Theory SetsCat_Interps
chapter "Interpretations of ‹sets_cat›"
theory SetsCat_Interps
imports Category3.ConcreteCategory Category3.ZFC_SetCat Category3.Colimit
SetsCat Universe_Interps
begin
text‹
In this section we construct two interpretations of the @{locale sets_cat} locale:
one using ``finite'' as the notion of smallness and one that uses ‹small›
from the theory ‹ZFC_in_HOL›. These interpretations demonstrate
the consistency of the variants of the @{locale sets_cat} locale: the interpretation
using finiteness validates the @{locale sets_cat_with_tupling} locale in unextended HOL,
and the interpretation in terms of ‹ZFC_in_HOL› validates the
@{locale sets_cat_with_tupling_and_infinity} locale, assuming that the axiomatization
of ‹ZFC_in_HOL› is consistent with HOL.
›
section "Category of Finite Sets"
text‹
The ‹finite_sets_cat› locale defines a category having as objects the natural numbers
and as arrows from ‹m› to ‹n› the functions from ‹m›-element sets to ‹n›-element sets.
In view of ‹SetsCat.categoricity›, this is the unique interpretation (up to equivalence
of categories) of @{locale sets_cat} having a countably infinite collection of arrows.
›
locale finite_sets_cat
begin
abbreviation OBJ
where "OBJ ≡ UNIV :: nat set"
abbreviation HOM
where "HOM ≡ λm n. {1..m :: nat} →⇩E {1..n :: nat}"
abbreviation Id
where "Id n ≡ λx :: nat. if x ∈ {1..n} then x else undefined"
abbreviation Comp
where "Comp _ _ m ≡ compose {1..m}"
interpretation Fin: concrete_category OBJ HOM Id Comp
by unfold_locales fastforce+
abbreviation comp
where "comp ≡ Fin.COMP"
lemma terminal_MkIde_1:
shows "Fin.terminal (Fin.MkIde 1)"
proof
show 1: "Fin.ide (Fin.MkIde 1)"
using Fin.ide_MkIde by blast
show "⋀a. Fin.ide a ⟹ ∃!f. Fin.in_hom f a (Fin.MkIde 1)"
proof -
fix a
assume a: "Fin.ide a"
let ?Ta = "λx. if x ∈ {1..Fin.Dom a} then 1 else undefined"
have 2: "HOM (Fin.Dom a) 1 = {?Ta}"
by (cases "Fin.Dom a = 0") auto
have "Fin.hom a (Fin.MkIde 1) = {Fin.MkArr (Fin.Dom a) 1 ?Ta}"
proof
show "{Fin.MkArr (Fin.Dom a) 1 ?Ta} ⊆ Fin.hom a (Fin.MkIde 1)"
using a 1 2 Fin.bij_betw_hom_Hom [of a "Fin.MkIde 1"] by fastforce
show "Fin.hom a (Fin.MkIde 1) ⊆ {Fin.MkArr (Fin.Dom a) 1 ?Ta}"
using a 1 2 Fin.bij_betw_hom_Hom(1-4) [of a "Fin.MkIde 1"]
by auto[1] (simp add: Pi_iff)
qed
thus "∃!f. Fin.in_hom f a (Fin.MkIde 1)"
by (metis (no_types, lifting) mem_Collect_eq singleton_iff)
qed
qed
sublocale category_with_terminal_object comp
using terminal_MkIde_1
by unfold_locales auto
notation some_terminal ("𝟭⇧?")
sublocale sets_cat_base ‹finite :: nat set ⇒ bool› comp
by (unfold_locales) (meson finite_surj lepoll_iff)
sublocale small_finite ‹finite :: nat set ⇒ bool›
using Universe_Interps.small_finite_finset by blast
sublocale small_powerset ‹finite :: nat set ⇒ bool›
using small_powerset_finset by auto
lemma finite_HOM:
shows "finite (HOM m n)"
by (simp add: finite_PiE)
lemma card_HOM:
shows "card (HOM m n) = n ^ m"
by (simp add: card_funcsetE)
lemma terminal_char⇩F⇩S⇩C:
shows "Fin.terminal a ⟷ a = Fin.MkIde 1"
proof
show "a = Fin.MkIde 1 ⟹ Fin.terminal a"
using terminal_MkIde_1 by blast
assume a: "Fin.terminal a"
have "a = Fin.MkIde (Fin.Dom a)"
using a Fin.terminal_def Fin.MkIde_Dom' by auto
moreover have "Fin.Dom a = 1"
proof -
have "Fin.Dom a ≠ 1 ⟹ ¬ (∃!f. Fin.in_hom f a (Fin.MkIde 1))"
proof -
assume 1: "Fin.Dom a ≠ 1"
have "card (HOM 1 (Fin.Dom a)) ≠ 1"
using 1 card_HOM
by (metis power_one_right)
moreover have "card (HOM 1 (Fin.Dom a)) = card (Fin.hom (Fin.MkIde 1) a)"
by (metis (no_types, lifting) HOL.ext Fin.Dom.simps(1) a Fin.bij_betw_hom_Hom(5)
bij_betw_same_card terminal_MkIde_1 Fin.terminal_def)
moreover have "⋀A. (∃!x. x ∈ A) ⟷ card A = 1"
by (metis card_1_singletonE ex_in_conv insert_iff is_singletonI' is_singleton_altdef)
ultimately show "¬ (∃!f. Fin.in_hom f a (Fin.MkIde 1))"
by (metis (no_types, lifting) a mem_Collect_eq terminal_MkIde_1 Fin.terminal_def)
qed
thus ?thesis
using a Fin.terminal_def terminal_MkIde_1 by force
qed
ultimately show "a = Fin.MkIde 1" by auto
qed
lemma MkIde_1_eq:
shows "Fin.MkIde 1 = 𝟭⇧?"
using terminal_char⇩F⇩S⇩C terminal_some_terminal by presburger
lemma finite_Set:
assumes "Fin.ide a"
shows "finite (Set a)"
by (metis assms bij_betw_finite Fin.bij_betw_hom_Hom(5) finite_HOM ide_some_terminal)
lemma card_Set:
assumes "Fin.ide a"
shows "card (Set a) = Fin.Dom a"
proof -
have "Set a = Fin.hom (Fin.MkIde 1) a"
using assms MkIde_1_eq by presburger
moreover have "eqpoll (Fin.hom (Fin.MkIde 1) a) (HOM 1 (Fin.Dom a))"
using assms Fin.bij_betw_hom_Hom(5)[of "Fin.MkIde 1" a] eqpoll_def
MkIde_1_eq ide_some_terminal
by auto
moreover have "card (HOM 1 (Fin.Dom a)) = Fin.Dom a"
using card_HOM
by (metis power_one_right)
ultimately show ?thesis
by (metis (lifting) bij_betw_same_card eqpoll_def)
qed
abbreviation mkpoint
where "mkpoint n k ≡ Fin.MkArr 1 n (λx. if x = 1 then k :: nat else undefined)"
abbreviation valof
where "valof x ≡ Fin.Map x (1 :: nat)"
lemma mkpoint_in_hom [intro, simp]:
assumes "k ∈ {1..n}"
shows "Fin.in_hom (mkpoint n k) (Fin.MkIde 1) (Fin.MkIde n)"
using assms Fin.MkArr_in_hom [of 1 n _ "Fin.MkIde 1" "Fin.MkIde n"] by fastforce
lemma valof_in_range:
assumes "Fin.in_hom x 𝟭⇧? a"
shows "valof x ∈ {1..Fin.Dom a}"
using assms Fin.arr_char [of x] Fin.dom_char Fin.cod_char
by (metis (no_types, lifting) Fin.Dom.simps(1) MkIde_1_eq PiE_E atLeastAtMost_singleton'
Fin.in_hom_char singletonI)
lemma valof_mkpoint:
shows "valof (mkpoint n k) = k"
by force
lemma mkpoint_valof:
assumes "Fin.in_hom x 𝟭⇧? a"
shows "mkpoint (Fin.Dom a) (valof x) = x"
proof (intro Fin.arr_eqI)
show "Fin.arr (mkpoint (Fin.Dom a) (valof x))"
using assms mkpoint_in_hom valof_in_range by blast
show 1: "Fin.arr x"
using assms by blast
show 2: "Fin.Dom (mkpoint (Fin.Dom a) (valof x)) = Fin.Dom x"
by (metis (lifting) Fin.Dom.simps(1) MkIde_1_eq assms Fin.in_hom_char)
show "Fin.Cod (mkpoint (Fin.Dom a) (valof x)) = Fin.Cod x"
by (metis (lifting) Fin.Cod.simps(1) MkIde_1_eq assms Fin.in_hom_char)
show "Fin.Map (mkpoint (Fin.Dom a) (valof x)) = Fin.Map x"
proof -
have "Fin.Map (mkpoint (Fin.Dom a) (valof x)) =
(λk. if k = 1 then valof x else undefined)"
by simp
also have "... = Fin.Map x"
proof
fix k
show "(if k = 1 then valof x else undefined) = Fin.Map x k"
using "1" "2" Fin.arr_char by auto
qed
finally show ?thesis by blast
qed
qed
lemma Map_arr_eq:
assumes "Fin.in_hom f a b"
shows "Fin.Map f = (λk. if k ∈ {1..Fin.Dom a}
then Fin.Map (Fun f (mkpoint (Fin.Dom a) k)) 1
else undefined)"
(is "Fin.Map f = ?F")
proof
fix k
show "Fin.Map f k = ?F k"
proof (cases "k ∈ {1..Fin.Dom a}")
case False
show ?thesis using False
by (metis (no_types, lifting) Fin.Map_in_Hom PiE_arb assms Fin.in_hom_char)
next
case True
have "?F k = Fin.Map (Fun f (mkpoint (Fin.Dom a) k)) 1"
using True by simp
also have "... = Fin.Map (comp f (mkpoint (Fin.Dom a) k)) 1"
using assms True mkpoint_in_hom [of k "Fin.Dom a"] MkIde_1_eq Fin.in_homE
Fin.in_hom_char Fun_def
by auto
also have "... = Fin.Map f (Fin.Map (mkpoint (Fin.Dom a) k) (1 :: nat))"
using assms True mkpoint_in_hom Fin.in_hom_char Fin.Map_comp by auto
also have "... = Fin.Map f k"
by force
finally show ?thesis by simp
qed
qed
sublocale sets_cat ‹finite :: nat set ⇒ bool› comp
proof
show "⋀a. Fin.ide a ⟹ nat_tupling.small (Set a)"
using finite_Set finset_small_iff_finite by blast
show "⋀A. ⟦nat_tupling.small A; A ⊆ Collect Fin.arr⟧ ⟹ ∃a. Fin.ide a ∧ Set a ≈ A"
by (metis (no_types, lifting) Fin.Dom.simps(1) card_Set eqpoll_iff_card finite_Set
finset_small_iff_finite Fin.ide_MkIde iso_tuple_UNIV_I)
show "⋀a b. ⟦Fin.ide a; Fin.ide b⟧ ⟹ inj_on Fun (Fin.hom a b)"
using Map_arr_eq Fin.in_hom_char
by (intro inj_onI Fin.arr_eqI) auto
show "⋀a b. ⟦Fin.ide a; Fin.ide b⟧ ⟹ Hom a b ⊆ Fun ` Fin.hom a b"
proof
fix a b
assume a: "Fin.ide a" and b: "Fin.ide b"
fix F
assume F: "F ∈ Hom a b"
show "F ∈ Fun ` Fin.hom a b"
proof
let ?F' = "λk. if k ∈ {1..Fin.Dom a}
then valof (F (mkpoint (Fin.Dom a) k))
else undefined"
let ?f = "Fin.MkArr (Fin.Dom a) (Fin.Dom b) ?F'"
show f: "?f ∈ Fin.hom a b"
proof
show "Fin.in_hom ?f a b"
proof
show "Fin.Dom a ∈ UNIV" by auto
show "Fin.Dom b ∈ UNIV" by auto
show "a = Fin.MkIde (Fin.Dom a)"
using a Fin.MkIde_Dom' by presburger
show "b = Fin.MkIde (Fin.Dom b)"
using b Fin.MkIde_Dom' by presburger
show "?F' ∈ HOM (Fin.Dom a) (Fin.Dom b)"
proof
fix k
show "k ∉ {1..Fin.Dom a} ⟹ ?F' k = undefined" by auto
show "k ∈ {1..Fin.Dom a} ⟹ ?F' k ∈ {1..Fin.Dom b}"
proof -
assume k: "k ∈ {1..Fin.Dom a}"
have "?F' k = valof (F (mkpoint (Fin.Dom a) k))"
using k by simp
moreover have "... ∈ {1..Fin.Dom b}"
proof -
have "F (mkpoint (Fin.Dom a) k) ∈ Fin.hom 𝟭⇧? b"
using a k F mkpoint_in_hom MkIde_1_eq ‹a = Fin.MkIde (Fin.Dom a)›
by force
thus ?thesis
using valof_in_range by blast
qed
ultimately show ?thesis by auto
qed
qed
qed
qed
show "F = Fun ?f"
proof
fix x
show "F x = Fun ?f x"
proof (cases "x ∈ Fin.hom 𝟭⇧? a")
case False
show ?thesis
using False F f a Fin.dom_eqI Fin.ide_in_hom Fin.seqI' Fun_def by auto
next
case True
show ?thesis
proof (intro Fin.arr_eqI)
show 1: "Fin.arr (F x)"
using F True by blast
show 2: "Fin.arr (Fun ?f x)"
using f True a Fin.dom_eqI Fin.ide_in_hom Fin.seqI' Fun_def by auto
show "Fin.Dom (F x) = Fin.Dom (Fun ?f x)"
proof -
have "Fin.Dom (F x) = Fin.Dom 𝟭⇧?"
using F True
by (metis (no_types, lifting) Int_def Pi_iff Fin.in_hom_char mem_Collect_eq)
also have "... = Fin.Dom (Fun ?f x)"
using True f
by (metis (no_types, lifting) "2" Fin.Dom_comp Fun_def Fin.arrE
Fin.in_hom_char mem_Collect_eq Fin.null_char)
finally show ?thesis by blast
qed
show "Fin.Cod (F x) = Fin.Cod (Fun ?f x)"
proof -
have "Fin.Cod (F x) = Fin.Dom b"
using F True
by (metis (no_types, lifting) Int_def Pi_mem Fin.in_hom_char mem_Collect_eq)
also have "... = Fin.Cod (Fun ?f x)"
using True f 2
by (metis (no_types, lifting) Fin.Cod.simps(1) Fin.Cod_comp Fin.arrE
Fin.null_char Fin.seq_char Fun_def)
finally show ?thesis by blast
qed
show "Fin.Map (F x) = Fin.Map (Fun ?f x)"
proof
fix k
show "Fin.Map (F x) k = Fin.Map (Fun ?f x) k"
proof -
have "k ≠ 1 ⟹ ?thesis"
proof -
assume k: "k ≠ 1"
have 1: "Fin.Map (F x) k = undefined"
proof -
have "Fin.in_hom (F x) 𝟭⇧? b"
using F True by blast
thus ?thesis
using F True k Map_arr_eq [of "F x" "𝟭⇧?" "b"]
by (metis Fin.Dom.simps(1) MkIde_1_eq atLeastAtMost_iff le_antisym)
qed
also have "... = Fin.Map (Fun ?f x) k"
proof -
have "Fin.Map (Fun ?f x) k = Fin.Map (comp ?f x) k"
using f True Fun_def by fastforce
also have "... = compose {1..Fin.Dom x} (Fin.Map ?f) (Fin.Map x) k"
using f True Fin.Map_comp
by (metis (no_types, lifting) Fin.in_hom_char mem_Collect_eq)
also have "... = undefined"
proof -
have "k ∉ {1..Fin.Dom x}"
using True k
by (metis (no_types, lifting) Fin.Dom.simps(1) MkIde_1_eq
atLeastAtMost_singleton Fin.in_hom_char mem_Collect_eq
singleton_iff)
thus ?thesis by auto
qed
finally show ?thesis by simp
qed
finally show ?thesis by simp
qed
moreover have "k = 1 ⟹ ?thesis"
proof -
assume k: "k = 1"
have "Fin.Map (Fun ?f x) k = Fin.Map (comp ?f x) k"
using "2" Fun_def Fin.arrE Fin.null_char by fastforce
also have "... = compose {1..1} (Fin.Map ?f) (Fin.Map x) k"
using f True Fin.Map_comp
by (metis (lifting) Fin.Dom.simps(1) IntI Int_Collect MkIde_1_eq
Fin.in_hom_char)
also have "... = ?F' (Fin.Map x k)"
apply auto[1]
by (auto simp add: k)
also have "... = valof (F (mkpoint (Fin.Dom a) (Fin.Map x k)))"
using F True k a valof_in_range by auto
also have "... = valof (F x)"
using F True k mkpoint_valof by force
also have "... = Fin.Map (F x) k"
using F True k by argo
finally show ?thesis by simp
qed
ultimately show ?thesis by blast
qed
qed
qed
qed
qed
qed
qed
qed
lemma is_sets_cat:
shows "sets_cat (finite :: nat set ⇒ bool) comp"
..
sublocale small_product ‹finite :: nat set ⇒ bool›
using small_product_finset by blast
sublocale sets_cat_with_pairing ‹finite :: nat set ⇒ bool› comp
proof
show "∃ι. is_embedding_of ι (Collect Fin.arr × Collect Fin.arr)"
proof -
have "⋀A. ⟦countable A; infinite A⟧ ⟹ ∃ι. ι ` (A × A) ⊆ A ∧ inj_on ι (A × A)"
proof -
fix A :: "'a set"
assume countable: "countable A" and infinite: "infinite A"
obtain ρ where ρ: "bij_betw ρ (A × A) (UNIV :: nat set)"
using countable infinite countableE_infinite
by (metis countable_SIGMA infinite_cartesian_product)
obtain σ where σ: "bij_betw σ (UNIV :: nat set) A"
using countable infinite bij_betw_from_nat_into by blast
have "(σ ∘ ρ) ` (A × A) ⊆ A ∧ inj_on (σ ∘ ρ) (A × A)"
using ρ σ
by (metis bij_betw_def comp_inj_on_iff equalityD2 image_comp)
thus "∃ι. ι ` (A × A) ⊆ A ∧ inj_on ι (A × A)" by blast
qed
moreover have "countable (Collect Fin.arr) ∧ infinite (Collect Fin.arr)"
proof
show "countable (Collect Fin.arr)"
proof -
have "Collect Fin.arr =
(⋃ab∈Collect Fin.ide × Collect Fin.ide. Fin.hom (fst ab) (snd ab))"
proof
show "(⋃ab∈Collect Fin.ide × Collect Fin.ide. Fin.hom (fst ab) (snd ab)) ⊆
Collect Fin.arr"
by blast
show "Collect Fin.arr ⊆
(⋃ab∈Collect Fin.ide × Collect Fin.ide. Fin.hom (fst ab) (snd ab))"
proof
fix f
assume f: "f ∈ Collect Fin.arr"
have "Fin.ide (Fin.dom f) ∧ Fin.ide (Fin.cod f) ∧
f ∈ Fin.hom (Fin.dom f) (Fin.cod f)"
using f Fin.ide_dom Fin.ide_cod by blast
hence "(Fin.dom f, Fin.cod f) ∈ Collect Fin.ide × Collect Fin.ide ∧
f ∈ Fin.hom (fst (Fin.dom f, Fin.cod f)) (snd (Fin.dom f, Fin.cod f))"
by auto
thus "f ∈ (⋃ab∈Collect Fin.ide × Collect Fin.ide. Fin.hom (fst ab) (snd ab))"
by blast
qed
qed
moreover have "countable (Collect Fin.ide × Collect Fin.ide)"
using Fin.bij_betw_ide_Obj(5) by force
moreover have "⋀ab. ab ∈ Collect Fin.ide × Collect Fin.ide
⟹ finite (Fin.hom (fst ab) (snd ab)) ∧
card (Fin.hom (fst ab) (snd ab)) =
Fin.Dom (snd ab) ^ Fin.Dom (fst ab)"
by (metis bij_betw_finite Fin.bij_betw_hom_Hom(5) bij_betw_same_card card_HOM
finite_HOM mem_Collect_eq mem_Times_iff)
ultimately show ?thesis
using countable_UN countable_finite by (metis (lifting))
qed
show "infinite (Collect Fin.arr)"
proof -
have "⋀X. ∀n. (∃Y. Y ⊆ X ∧ card Y ≥ n) ⟹ infinite X"
by (metis card_mono not_less_eq_eq)
moreover have "∀n. (∃ab. ab ∈ Collect Fin.ide × Collect Fin.ide ∧
card (Fin.hom (fst ab) (snd ab)) ≥ n)"
by (metis (no_types, lifting) HOL.ext Fin.Dom.simps(1) SigmaI card_Set
fst_conv Fin.ide_MkIde ide_some_terminal iso_tuple_UNIV_I mem_Collect_eq
order_refl snd_conv)
ultimately show ?thesis
by (metis (no_types, lifting) Fin.in_homE mem_Collect_eq subsetI)
qed
qed
ultimately show ?thesis by blast
qed
qed
lemma is_sets_cat_with_pairing:
shows "sets_cat_with_pairing (finite :: nat set ⇒ bool) comp"
..
sublocale lifting ‹Collect Fin.arr›
proof
show "embeds ({None} ∪ Some ` Collect Fin.arr)"
proof -
have "⋀n :: nat. Set (Fin.MkIde n) ⊆ Collect Fin.arr ∧ card (Set (Fin.MkIde n)) = n"
using card_Set Fin.ide_MkIde by fastforce
hence 1: "infinite (Collect Fin.arr)"
by (metis (lifting) Suc_n_not_le_n card_mono)
obtain a where a: "a ∈ Collect Fin.arr"
using 1 not_finite_existsD by auto
have 2: "eqpoll (Collect Fin.arr) (Collect Fin.arr - {a})"
using 1 a
by (metis (lifting) infinite_insert_eqpoll infinite_remove insert_Diff)
obtain f where f: "f ` Collect Fin.arr ⊆ Collect Fin.arr - {a} ∧
inj_on f (Collect Fin.arr)"
using 2
by (metis (lifting) bij_betw_def eqpoll_def subset_refl)
let ?ι = "λNone ⇒ a | Some x ⇒ f x"
have "is_embedding_of ?ι ({None} ∪ Some ` Collect Fin.arr)"
using a f by (auto simp add: inj_on_def)
thus ?thesis by blast
qed
qed
sublocale sets_cat_with_powering ‹finite :: nat set ⇒ bool› comp
proof
show "embeds {X. X ⊆ Collect Fin.arr ∧ nat_tupling.small X}"
proof -
have "⋀X. infinite X ⟹ eqpoll (Fpow X) X"
using Fpow_infinite_bij_betw eqpoll_def by blast
hence "eqpoll {X. X ⊆ Collect Fin.arr ∧ nat_tupling.small X} (Collect Fin.arr)"
using infinite_univ finset_small_iff_finite Fpow_def
by (metis (mono_tags, lifting) Collect_cong)
thus ?thesis
by (metis (lifting) bij_betw_def eqpoll_def subset_refl)
qed
qed
lemma is_sets_cat_with_powering:
shows "sets_cat_with_powering (finite :: nat set ⇒ bool) comp"
..
sublocale small_sum ‹finite :: nat set ⇒ bool›
using small_sum_finset by blast
sublocale sets_cat_with_tupling ‹finite :: nat set ⇒ bool› comp
by unfold_locales
theorem is_sets_cat_with_tupling:
shows "sets_cat_with_tupling (finite :: nat set ⇒ bool) comp"
..
end
text‹
Here is the final top-level interpretation. Note that this is proved in
``vanilla HOL'' without any additional axioms.
›