(* Title: ZFC_SetCat Author: Eugene W. Stark <stark@cs.stonybrook.edu>, 2022 Maintainer: Eugene W. Stark <stark@cs.stonybrook.edu> *) chapter "ZFC SetCat" text‹ In the statement and proof of the Yoneda Lemma given in theory ‹Yoneda›, we sidestepped the issue, of not having a category of ``all'' sets, by axiomatizing the notion of a ``set category'', showing that for every category we could obtain a hom-functor into a set category at a higher type, and then proving the Yoneda lemma for that particular hom-functor. This is perhaps the best we can do within HOL, because HOL does not provide any type that contains a universe of sets with the closure properties usually associated with a category ‹Set› of sets and functions between them. However, a significant aspect of category theory involves considering ``all'' algebraic structures of a particular kind as the objects of a ``large'' category having nice closure or completeness properties. Being able to consider a category of sets that is ``small-complete'', or a cartesian closed category of sets and functions that includes some infinite sets as objects, are basic examples of this kind of situation. The purpose of this section is to demonstrate that, although it cannot be done in pure HOL, if we are willing to accept the existence of a type ‹V› whose inhabitants correspond to sets satisfying the axioms of ZFC, then it is possible to construct, for example, the ``large'' category of sets and functions as it is usually understood in category theory. Moreover, assuming the existence of such a type is essentially all we have to do; all the category theory we have developed so far still applies. Specifically, what we do in this section is to use theory ‹ZFC_in_HOL›, which provides an axiomatization of a set-theoretic universe ‹V›, to construct a ``set category'' ‹ZFC_SetCat›, whose objects correspond to ‹V›-sets, whose arrows correspond to functions between ‹V›-sets, and which has the small-completeness property traditionally ascribed to the category of all small sets and functions between them. › theory ZFC_SetCat imports ZFC_in_HOL.ZFC_Cardinals Limit begin text‹ The following locale constructs the category of classes and functions between them and shows that it is small complete. The category is obtained simply as the replete set category at type ‹V›. This is not yet the category of sets we want, because it contains objects corresponding to ``large'' ‹V›-sets. › locale ZFC_class_cat begin sublocale replete_setcat ‹TYPE(V)› . lemma admits_small_V_tupling: assumes "small (I :: V set)" shows "admits_tupling I" proof (unfold admits_tupling_def) let ?π = "λf. UP (VLambda (ZFC_in_HOL.set I) (DN o f))" have "?π ∈ (I → Univ) ∩ extensional' I → Univ" using UP_mapsto by force moreover have "inj_on ?π ((I → Univ) ∩ extensional' I)" proof fix f g assume f: "f ∈ (I → Univ) ∩ extensional' I" assume g: "g ∈ (I → Univ) ∩ extensional' I" assume eq: "UP (VLambda (ZFC_in_HOL.set I) (DN ∘ f)) = UP (VLambda (ZFC_in_HOL.set I) (DN ∘ g))" have 1: "VLambda (ZFC_in_HOL.set I) (DN ∘ f) = VLambda (ZFC_in_HOL.set I) (DN ∘ g)" using f g eq by (meson injD inj_UP) show "f = g" proof fix x have "x ∉ I ⟹ f x = g x" using f g extensional'_def [of I] by auto moreover have "x ∈ I ⟹ f x = g x" proof - assume x: "x ∈ I" hence "(DN o f) x = (DN o g) x" using assms 1 x elts_of_set VLambda_eq_D2 by fastforce thus "f x = g x" using f g x comp_apply UP_DN by (metis IntD1 PiE bij_arr_of bij_betw_imp_surj_on) qed ultimately show "f x = g x" by blast qed qed ultimately show "∃π. π ∈ (I → Univ) ∩ extensional' I → Univ ∧ inj_on π ((I → Univ) ∩ extensional' I)" by blast qed corollary admits_small_tupling: assumes "small I" shows "admits_tupling I" proof - obtain φ where φ: "inj_on φ I ∧ φ ` I ∈ range elts" using assms small_def by metis have "admits_tupling (φ ` I)" using φ admits_small_V_tupling by fastforce moreover have inv: "bij_betw (inv_into I φ) (φ ` I) I" by (simp add: φ bij_betw_inv_into inj_on_imp_bij_betw) ultimately show ?thesis using admits_tupling_respects_bij by blast qed lemma has_small_products: assumes "small (I :: 'i set)" and "I ≠ UNIV" shows "has_products I" proof - have 1: "⋀I :: V set. small I ⟹ has_products I" using big_UNIV by (metis admits_small_tupling has_products_iff_admits_tupling) obtain V_of where V_of: "inj_on V_of I ∧ V_of ` I ∈ range elts" using assms small_def by metis have "bij_betw (inv_into I V_of) (V_of ` I) I" using V_of bij_betw_inv_into bij_betw_imageI by metis moreover have "small (V_of ` I)" using assms by auto ultimately show ?thesis using assms 1 has_products_preserved_by_bijection by blast qed theorem has_small_limits: assumes "small (UNIV :: 'i set)" shows "has_limits (undefined :: 'i)" proof - have "∀I :: 'i set. I ≠ UNIV ⟶ admits_tupling I" using assms smaller_than_small subset_UNIV admits_small_tupling by auto thus ?thesis using assms has_limits_iff_admits_tupling by blast qed end text‹ We now construct the desired category of small sets and functions between them, as a full subcategory of the category of classes and functions. To show that this subcategory is small complete, we show that the inclusion creates small products; that is, a small product of objects corresponding to small sets itself corresponds to a small set. › locale ZFC_set_cat begin interpretation Cls: ZFC_class_cat . definition setp where "setp A ≡ A ⊆ Cls.Univ ∧ small A" sublocale sub_set_category Cls.comp ‹λA. A ⊆ Cls.Univ› setp using small_Un smaller_than_small setp_def apply unfold_locales apply simp_all apply force by auto lemma is_sub_set_category: shows "sub_set_category Cls.comp (λA. A ⊆ Cls.Univ) setp" using sub_set_category_axioms by blast interpretation incl: full_inclusion_functor Cls.comp ‹λa. Cls.ide a ∧ setp (Cls.set a)› .. text‹ The following functions establish a bijection between the identities of the category and the elements of type ‹V›; which in turn are in bijective correspondence with small ‹V›-sets. › definition V_of_ide :: "V setcat.arr ⇒ V" where "V_of_ide a ≡ ZFC_in_HOL.set (Cls.DN ` Cls.set a)" definition ide_of_V :: "V ⇒ V setcat.arr" where "ide_of_V A ≡ Cls.mkIde (Cls.UP ` elts A)" lemma bij_betw_ide_V: shows "V_of_ide ∈ Collect ide → UNIV" and "ide_of_V ∈ UNIV → Collect ide" and [simp]: "ide a ⟹ ide_of_V (V_of_ide a) = a" and [simp]: "V_of_ide (ide_of_V A) = A" and "bij_betw V_of_ide (Collect ide) UNIV" and "bij_betw ide_of_V UNIV (Collect ide)" proof - have "Univ = Cls.Univ" using terminal_char by presburger show 1: "V_of_ide ∈ Collect ide → UNIV" by blast show 2: "ide_of_V ∈ UNIV → Collect ide" proof fix A :: V have "small (elts A)" by blast have "Cls.UP ` elts A ⊆ Univ ∧ small (Cls.UP ` elts A)" using Cls.UP_mapsto terminal_char by blast hence "ide (mkIde (Cls.UP ` elts A))" using ide_mkIde ‹Univ = Cls.Univ› setp_def by auto thus "ide_of_V A ∈ Collect ide" using ide_of_V_def ide_char⇩_{S}⇩_{S}⇩_{C}setp_def by (metis (no_types, lifting) Cls.ide_mkIde Cls.set_mkIde arr_mkIde ide_char' mem_Collect_eq) qed show 3: "⋀a. ide a ⟹ ide_of_V (V_of_ide a) = a" proof - fix a assume a: "ide a" have "ide_of_V (V_of_ide a) = Cls.mkIde (Cls.UP ` elts (ZFC_in_HOL.set (Cls.DN ` Cls.set a)))" unfolding ide_of_V_def V_of_ide_def by simp also have "... = Cls.mkIde (Cls.UP ` Cls.DN ` Cls.set a)" using setp_set_ide a ide_char⇩_{S}⇩_{S}⇩_{C}setp_def by force also have "... = Cls.mkIde (Cls.set a)" proof - have "Cls.set a ⊆ Cls.Univ" using a ide_char⇩_{S}⇩_{S}⇩_{C}setp_def by blast hence "Cls.UP ` Cls.DN ` Cls.set a = Cls.set a" proof - have "⋀x. x ∈ Cls.set a ⟹ x ∈ Cls.UP ` Cls.DN ` Cls.set a" using Cls.UP_DN ‹Cls.set a ⊆ Cls.Univ› by (metis Cls.bij_arr_of bij_betw_def image_inv_into_cancel) moreover have "⋀x. x ∈ Cls.UP ` Cls.DN ` Cls.set a ⟹ x ∈ Cls.set a" using ‹Cls.set a ⊆ Cls.Univ› by (metis Cls.bij_arr_of bij_betw_def image_inv_into_cancel) ultimately show ?thesis by blast qed thus ?thesis by argo qed also have "... = a" using a Cls.mkIde_set ide_char⇩_{S}⇩_{b}⇩_{C}by blast finally show "ide_of_V (V_of_ide a) = a" by simp qed show 4: "⋀A. V_of_ide (ide_of_V A) = A" proof - fix A have "V_of_ide (ide_of_V A) = ZFC_in_HOL.set (Cls.DN ` Cls.set (Cls.mkIde (Cls.UP ` elts A)))" unfolding V_of_ide_def ide_of_V_def by simp also have "... = ZFC_in_HOL.set (Cls.DN ` Cls.UP ` elts A)" using Cls.set_mkIde [of "Cls.UP ` elts A"] Cls.UP_mapsto by fastforce also have "... = ZFC_in_HOL.set (elts A)" using Cls.DN_UP by force also have "... = A" by simp finally show "V_of_ide (ide_of_V A) = A" by blast qed show "bij_betw V_of_ide (Collect ide) UNIV" using 1 2 3 4 by (intro bij_betwI) auto show "bij_betw ide_of_V UNIV (Collect ide)" using 1 2 3 4 by (intro bij_betwI) blast+ qed text‹ Next, we establish bijections between the hom-sets of the category and certain subsets of ‹V› whose elements represent functions. › definition V_of_arr :: "V setcat.arr ⇒ V" where "V_of_arr f ≡ VLambda (V_of_ide (dom f)) (Cls.DN o Cls.Fun f o Cls.UP)" definition arr_of_V :: "V setcat.arr ⇒ V setcat.arr ⇒ V ⇒ V setcat.arr" where "arr_of_V a b F ≡ Cls.mkArr (Cls.set a) (Cls.set b) (Cls.UP o app F o Cls.DN)" definition vfun where "vfun A B f ≡ f ∈ elts (VPow (vtimes A B)) ∧ elts A = Domain (pairs f) ∧ single_valued (pairs f)" lemma small_Collect_vfun: shows "small (Collect (vfun A B))" unfolding vfun_def by (metis (full_types) small_Collect small_elts) lemma vfunI: assumes "f ∈ elts A → elts B" shows "vfun A B (VLambda A f)" proof (unfold vfun_def, intro conjI) show "VLambda A f ∈ elts (VPow (vtimes A B))" using assms VLambda_def by auto show "elts A = Domain (pairs (VLambda A f))" using assms VLambda_def [of A f] by (metis Domain_fst fst_pairs_VLambda) show "single_valued (pairs (VLambda A f))" using assms VLambda_def single_valued_def pairs_iff_elts by fastforce qed lemma app_vfun_mapsto: assumes "vfun A B F" shows "app F ∈ elts A → elts B" proof have "F ∈ elts (VPow (vtimes A B)) ∧ elts A = Domain (pairs F) ∧ single_valued (pairs F)" using assms vfun_def by simp hence 1: "F ∈ elts (VPi A (λ_. B)) ∧ elts A = Domain (pairs F) ∧ single_valued (pairs F)" unfolding VPi_def by (metis (no_types, lifting) down elts_of_set mem_Collect_eq subsetI) fix x assume x: "x ∈ elts A" have "x ∈ Domain (pairs F)" using assms x vfun_def by blast thus "app F x ∈ elts B" using x 1 VPi_D [of F A "λ_. B" x] by blast qed lemma bij_betw_hom_vfun: shows "V_of_arr ∈ hom a b → Collect (vfun (V_of_ide a) (V_of_ide b))" and "⟦ide a; ide b⟧ ⟹ arr_of_V a b ∈ Collect (vfun (V_of_ide a) (V_of_ide b)) → hom a b" and "f ∈ hom a b ⟹ arr_of_V a b (V_of_arr f) = f" and "⟦ide a; ide b; F ∈ Collect (vfun (V_of_ide a) (V_of_ide b))⟧ ⟹ V_of_arr (arr_of_V a b F) = F" and "⟦ide a; ide b⟧ ⟹ bij_betw V_of_arr (hom a b) (Collect (vfun (V_of_ide a) (V_of_ide b)))" and "⟦ide a; ide b⟧ ⟹ bij_betw (arr_of_V a b) (Collect (vfun (V_of_ide a) (V_of_ide b))) (hom a b)" proof - show 1: "⋀a b. V_of_arr ∈ hom a b → Collect (vfun (V_of_ide a) (V_of_ide b))" proof fix a b f assume f: "f ∈ hom a b" have "V_of_arr f = VLambda (V_of_ide (dom f)) (Cls.DN ∘ Cls.Fun f ∘ Cls.UP)" unfolding V_of_arr_def by simp moreover have "vfun (V_of_ide a) (V_of_ide b) ..." proof - have "Cls.DN ∘ Cls.Fun f ∘ Cls.UP ∈ elts (V_of_ide a) → elts (V_of_ide b)" proof fix x assume x: "x ∈ elts (V_of_ide a)" have "(Cls.DN ∘ Cls.Fun f ∘ Cls.UP) x = Cls.DN (Cls.Fun f (Cls.UP x))" by simp moreover have "... ∈ elts (V_of_ide b)" proof - have "Cls.UP x ∈ Cls.Dom f" by (metis (no_types, lifting) Cls.arr_dom_iff_arr Cls.arr_mkIde Cls.set_mkIde bij_betw_ide_V(3) arr_char⇩_{S}⇩_{b}⇩_{C}dom_simp f ide_char⇩_{S}⇩_{S}⇩_{C}ide_of_V_def image_eqI in_homE mem_Collect_eq x) hence "Cls.DN (Cls.Fun f (Cls.UP x)) ∈ Cls.DN ` Cls.Cod f" using f in_hom_char⇩_{F}⇩_{S}⇩_{b}⇩_{C}arr_char⇩_{S}⇩_{b}⇩_{C}Cls.Fun_mapsto [of f] by blast thus "Cls.DN (Cls.Fun f (Cls.UP x)) ∈ elts (V_of_ide b)" by (metis (no_types, lifting) V_of_ide_def arrE cod_char⇩_{S}⇩_{b}⇩_{C}elts_of_set f in_homE mem_Collect_eq replacement setp_def) qed ultimately show "(Cls.DN ∘ Cls.Fun f ∘ Cls.UP) x ∈ elts (V_of_ide b)" by argo qed thus ?thesis using f vfunI by blast qed ultimately show "V_of_arr f ∈ Collect (vfun (V_of_ide a) (V_of_ide b))" by simp qed show 2: "⋀a b. ⟦ide a; ide b⟧ ⟹ arr_of_V a b ∈ Collect (vfun (V_of_ide a) (V_of_ide b)) → hom a b" proof - fix a b assume a: "ide a" and b: "ide b" show "arr_of_V a b ∈ Collect (vfun (V_of_ide a) (V_of_ide b)) → hom a b" proof fix F assume F: "F ∈ Collect (vfun (V_of_ide a) (V_of_ide b))" have 3: "app F ∈ elts (V_of_ide a) → elts (V_of_ide b)" using F app_vfun_mapsto [of "V_of_ide a" "V_of_ide b" F] by blast have 4: "app F ∈ Cls.DN ` (Cls.set a) → Cls.DN ` (Cls.set b)" using 3 V_of_ide_def a b ide_char⇩_{S}⇩_{S}⇩_{C}setp_def by auto have "arr_of_V a b F = Cls.mkArr (Cls.set a) (Cls.set b) (Cls.UP ∘ app F ∘ Cls.DN)" unfolding arr_of_V_def by simp moreover have "... ∈ hom a b" proof show "«Cls.mkArr (Cls.set a) (Cls.set b) (Cls.UP ∘ app F ∘ Cls.DN) : a → b»" proof have 4: "Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.UP ∘ app F ∘ Cls.DN))" proof - have "Cls.set a ⊆ Cls.Univ ∧ Cls.set b ⊆ Cls.Univ" using a b ide_char⇩_{S}⇩_{S}⇩_{C}setp_def by blast moreover have "Cls.UP ∘ app F ∘ Cls.DN ∈ Cls.set a → Cls.set b" proof fix x assume x: "x ∈ Cls.set a" have "(Cls.UP ∘ app F ∘ Cls.DN) x = Cls.UP (app F (Cls.DN x))" by simp moreover have "... ∈ Cls.set b" by (metis (no_types, lifting) 4 Cls.arr_mkIde Cls.ide_char' Cls.set_mkIde PiE V_of_ide_def bij_betw_ide_V(3) b elts_of_set ide_char⇩_{S}⇩_{S}⇩_{C}ide_of_V_def replacement rev_image_eqI x setp_def) ultimately show "(Cls.UP ∘ app F ∘ Cls.DN) x ∈ Cls.set b" by auto qed ultimately show ?thesis by blast qed show 5: "arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.UP ∘ app F ∘ Cls.DN))" using a b 4 arr_char⇩_{S}⇩_{b}⇩_{C}ide_char⇩_{S}⇩_{b}⇩_{C}by auto show "dom (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.UP ∘ app F ∘ Cls.DN)) = a" using a 4 5 dom_char⇩_{S}⇩_{b}⇩_{C}ide_char⇩_{S}⇩_{b}⇩_{C}by auto show "cod (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.UP ∘ app F ∘ Cls.DN)) = b" using b 4 5 cod_char⇩_{S}⇩_{b}⇩_{C}ide_char⇩_{S}⇩_{b}⇩_{C}by auto qed qed ultimately show "arr_of_V a b F ∈ hom a b" by auto qed qed show 3: "⋀a b f. f ∈ hom a b ⟹ arr_of_V a b (V_of_arr f) = f" proof - fix a b f assume f: "f ∈ hom a b" have 4: "⋀x. x ∈ Cls.set a ⟹ (Cls.UP ∘ (Cls.DN ∘ Cls.Fun f ∘ Cls.UP) ∘ Cls.DN) x = Cls.Fun f x" proof - fix x assume x: "x ∈ Cls.set a" have "(Cls.UP ∘ (Cls.DN ∘ Cls.Fun f ∘ Cls.UP) ∘ Cls.DN) x = Cls.UP (Cls.DN (Cls.Fun f (Cls.UP (Cls.DN x))))" by simp also have "... = Cls.UP (Cls.DN (Cls.Fun f x))" using x Cls.UP_DN by (metis (no_types, lifting) Cls.elem_set_implies_incl_in Cls.incl_in_def Cls.setp_set_ide bij_betw_def replete_setcat.bij_arr_of subset_eq) also have "... = Cls.Fun f x" proof - have "x ∈ Cls.Dom f" using x f dom_char⇩_{S}⇩_{b}⇩_{C}by fastforce hence "Cls.Fun f x ∈ Cls.Cod f" using x f Cls.Fun_mapsto in_hom_char⇩_{F}⇩_{S}⇩_{b}⇩_{C}by blast hence "Cls.Fun f x ∈ Cls.Univ" using f cod_char⇩_{S}⇩_{b}⇩_{C}in_hom_char⇩_{F}⇩_{S}⇩_{b}⇩_{C}by (metis (no_types, lifting) Cls.elem_set_implies_incl_in Cls.incl_in_def Cls.setp_set_ide subsetD) thus ?thesis by (meson bij_betw_inv_into_right replete_setcat.bij_arr_of) qed finally show "(Cls.UP ∘ (Cls.DN ∘ Cls.Fun f ∘ Cls.UP) ∘ Cls.DN) x = Cls.Fun f x" by blast qed have 5: "Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.UP ∘ (Cls.DN ∘ Cls.Fun f ∘ Cls.UP) ∘ Cls.DN))" proof - have "Cls.set a ⊆ Cls.Univ ∧ Cls.set b ⊆ Cls.Univ" using f ide_char⇩_{S}⇩_{b}⇩_{C}codomains_def domains_def in_hom_def by force moreover have "Cls.UP ∘ (Cls.DN ∘ Cls.Fun f ∘ Cls.UP) ∘ Cls.DN ∈ Cls.set a → Cls.set b" proof fix x assume x: "x ∈ Cls.set a" hence 6: "x ∈ Cls.Dom f" using f by (metis (no_types, lifting) dom_char⇩_{S}⇩_{b}⇩_{C}in_homE mem_Collect_eq) have "(Cls.UP ∘ (Cls.DN ∘ Cls.Fun f ∘ Cls.UP) ∘ Cls.DN) x = Cls.Fun f x" using 4 f x by blast moreover have "... ∈ Cls.Cod f" using 4 6 f Cls.Fun_mapsto by (metis (no_types, lifting) Cls.arr_dom_iff_arr Cls.elem_set_implies_incl_in Cls.ideD(1) Cls.incl_in_def IntE PiE) moreover have "... = Cls.set b" using f by (metis (no_types, lifting) cod_char⇩_{S}⇩_{b}⇩_{C}in_homE mem_Collect_eq) ultimately show "(Cls.UP ∘ (Cls.DN ∘ Cls.Fun f ∘ Cls.UP) ∘ Cls.DN) x ∈ Cls.set b" by auto qed ultimately show ?thesis by blast qed have "arr_of_V a b (V_of_arr f) = Cls.mkArr (Cls.set a) (Cls.set b) (Cls.UP ∘ app (VLambda (V_of_ide (dom f)) (Cls.DN ∘ Cls.Fun f ∘ Cls.UP)) ∘ Cls.DN)" unfolding arr_of_V_def V_of_arr_def by simp also have "... = Cls.mkArr (Cls.set a) (Cls.set b) (Cls.UP ∘ (Cls.DN ∘ Cls.Fun f ∘ Cls.UP) ∘ Cls.DN)" proof (intro Cls.mkArr_eqI') show 6: "⋀x. x ∈ Cls.set a ⟹ (Cls.UP ∘ app (VLambda (V_of_ide (dom f)) (Cls.DN ∘ Cls.Fun f ∘ Cls.UP)) ∘ Cls.DN) x = (Cls.UP ∘ (Cls.DN ∘ Cls.Fun f ∘ Cls.UP) ∘ Cls.DN) x" proof - fix x assume x: "x ∈ Cls.set a" have "(Cls.UP ∘ app (VLambda (V_of_ide (dom f)) (Cls.DN ∘ Cls.Fun f ∘ Cls.UP)) ∘ Cls.DN) x = Cls.UP (app (VLambda (V_of_ide (dom f)) (Cls.DN ∘ Cls.Fun f ∘ Cls.UP)) (Cls.DN x))" by simp also have "... = (Cls.UP ∘ (Cls.DN ∘ Cls.Fun f ∘ Cls.UP) ∘ Cls.DN) x" proof - have "Cls.DN x ∈ elts (V_of_ide (dom f))" using f by (metis (no_types, lifting) V_of_ide_def elts_of_set ide_char⇩_{S}⇩_{S}⇩_{C}ide_dom image_eqI in_homE mem_Collect_eq replacement x setp_def) thus ?thesis using beta by auto qed ultimately show "(Cls.UP ∘ app (VLambda (V_of_ide (dom f)) (Cls.DN ∘ Cls.Fun f ∘ Cls.UP)) ∘ Cls.DN) x = (Cls.UP ∘ (Cls.DN ∘ Cls.Fun f ∘ Cls.UP) ∘ Cls.DN) x" by argo qed show "Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.UP ∘ app (VLambda (V_of_ide (local.dom f)) (Cls.DN ∘ Cls.Fun f ∘ Cls.UP)) ∘ Cls.DN))" using 5 6 Cls.mkArr_eqI by auto qed also have "... = Cls.mkArr (Cls.set a) (Cls.set b) (Cls.Fun f)" using 4 5 by force also have "... = f" using f Cls.mkArr_Fun by (metis (no_types, lifting) arr_char⇩_{S}⇩_{b}⇩_{C}cod_simp dom_char⇩_{S}⇩_{b}⇩_{C}in_homE mem_Collect_eq) finally show "arr_of_V a b (V_of_arr f) = f" by blast qed show 4: "⋀a b F. ⟦ide a; ide b; F ∈ Collect (vfun (V_of_ide a) (V_of_ide b))⟧ ⟹ V_of_arr (arr_of_V a b F) = F" proof - fix a b F assume a: "ide a" and b: "ide b" assume F: "F ∈ Collect (vfun (V_of_ide a) (V_of_ide b))" have "F ∈ elts (VPow (vtimes (V_of_ide a) (V_of_ide b))) ∧ elts (V_of_ide a) = Domain (pairs F) ∧ single_valued (pairs F)" using F vfun_def by simp hence 5: "F ∈ elts (VPi (V_of_ide a) (λ_. V_of_ide b))" unfolding VPi_def by (metis (no_types, lifting) down elts_of_set mem_Collect_eq subsetI) let ?f = "Cls.mkArr (Cls.set a) (Cls.set b) (Cls.UP ∘ app F ∘ Cls.DN)" have 6: "Cls.arr ?f" proof - have "Cls.set a ⊆ Cls.Univ ∧ Cls.set b ⊆ Cls.Univ" using a b ide_char⇩_{S}⇩_{S}⇩_{C}setp_def by blast moreover have "Cls.UP ∘ app F ∘ Cls.DN ∈ Cls.set a → Cls.set b" proof fix x assume x: "x ∈ Cls.set a" have "(Cls.UP ∘ app F ∘ Cls.DN) x = Cls.UP (app F (Cls.DN x))" by simp moreover have "... ∈ Cls.set b" proof - have "app F (Cls.DN x) ∈ Cls.DN ` Cls.set b" using a b ide_char⇩_{S}⇩_{S}⇩_{C}x F app_vfun_mapsto [of "V_of_ide a" "V_of_ide b" F] V_of_ide_def setp_def by auto thus ?thesis using ‹Cls.set a ⊆ Cls.Univ ∧ Cls.set b ⊆ Cls.Univ› by (metis Cls.bij_arr_of bij_betw_def imageI image_inv_into_cancel) qed ultimately show "(Cls.UP ∘ app F ∘ Cls.DN) x ∈ Cls.set b" by auto qed ultimately show ?thesis by blast qed have "V_of_arr (arr_of_V a b F) = VLambda (V_of_ide (dom ?f)) (Cls.DN ∘ Cls.Fun ?f ∘ Cls.UP)" unfolding V_of_arr_def arr_of_V_def by simp also have "... = VLambda (V_of_ide a) (Cls.DN ∘ Cls.Fun ?f ∘ Cls.UP)" unfolding V_of_ide_def using a b 6 ide_char⇩_{S}⇩_{S}⇩_{C}V_of_ide_def dom_char⇩_{S}⇩_{b}⇩_{C}Cls.dom_mkArr arrI⇩_{S}⇩_{b}⇩_{C}by auto also have "... = VLambda (V_of_ide a) (Cls.DN ∘ restrict (Cls.UP ∘ app F ∘ Cls.DN) (Cls.set a) ∘ Cls.UP)" using 6 Cls.Fun_mkArr by simp also have "... = VLambda (V_of_ide a) (app F)" proof - have 7: "⋀x. x ∈ elts (V_of_ide a) ⟹ (Cls.DN ∘ restrict (Cls.UP ∘ app F ∘ Cls.DN) (Cls.set a) ∘ Cls.UP) x = app F x" unfolding V_of_ide_def using a apply simp by (metis (no_types, lifting) Cls.bij_arr_of a bij_betw_def empty_iff ide_char⇩_{S}⇩_{S}⇩_{C}image_eqI image_inv_into_cancel setp_def) have 8: "⋀x. x ∈ elts (V_of_ide a) ⟹ (Cls.DN ∘ restrict (Cls.UP ∘ app F ∘ Cls.DN) (Cls.set a) ∘ Cls.UP) x ∈ elts (V_of_ide b)" using 5 7 VPi_D by fastforce have "VLambda (V_of_ide a) (app F) ∈ elts (VPi (V_of_ide a) (λ_. V_of_ide b))" using 5 VPi_I VPi_D by auto moreover have "VLambda (V_of_ide a) (Cls.DN ∘ restrict (Cls.UP ∘ app F ∘ Cls.DN) (Cls.set a) ∘ Cls.UP) ∈ elts (VPi (V_of_ide a) (λ_. V_of_ide b))" using 8 VPi_I by auto moreover have "⋀x. x ∈ elts (V_of_ide a) ⟹ app (VLambda (V_of_ide a) (Cls.DN ∘ restrict (Cls.UP ∘ app F ∘ Cls.DN) (Cls.set a) ∘ Cls.UP)) x = app F x" using 7 beta by auto ultimately show ?thesis using fun_ext by simp qed also have "... = F" using 5 eta [of F "V_of_ide a" "λ_. V_of_ide b"] by auto finally show "V_of_arr (arr_of_V a b F) = F" by blast qed show "⟦ide a; ide b⟧ ⟹ bij_betw V_of_arr (hom a b) (Collect (vfun (V_of_ide a) (V_of_ide b)))" using 1 2 3 4 apply (intro bij_betwI) apply blast apply blast by auto show "⟦ide a; ide b⟧ ⟹ bij_betw (arr_of_V a b) (Collect (vfun (V_of_ide a) (V_of_ide b))) (hom a b)" using 1 2 3 4 apply (intro bij_betwI) apply blast apply blast by auto qed lemma small_hom: shows "small (hom a b)" proof (cases "ide a ∧ ide b") assume 1: "¬ (ide a ∧ ide b)" have "⋀f. ¬ «f : a → b»" using 1 in_hom_def ide_cod ide_dom by blast hence "hom a b = {}" by blast thus ?thesis by simp next assume 1: "ide a ∧ ide b" show ?thesis using 1 bij_betw_hom_vfun(5) small_Collect_vfun small_def by (metis (no_types, lifting) bij_betw_def small_iff_range) qed text‹ We can now show that the inclusion of the subcategory into the ambient category ‹Cls› creates small products. To do this, we consider a product in ‹Cls› of objects of the subcategory indexed by a small set ‹I›. Since ‹Cls› is a replete set category, by a previous result we know that the elements of a product object ‹p› in ‹Cls› correspond to its points; that is, to the elements of ‹hom unity p›. The elements of ‹hom unity p› in turn correspond to ‹I›-tuples. By carrying out the construction of the set of ‹I›-tuples in ‹V› and exploiting the bijections between homs of the subcatgory and ‹V›-sets, we can obtain an injection of ‹hom unity p› to the extension of a ‹V›-set, thus showing ‹hom unity p› is small. Since ‹hom unity p› is small, it determines an object of the subcategory, which must then be a product in the subcategory, in view of the fact that the subcategory is full. › lemma has_small_V_products: assumes "small (I :: V set)" shows "has_products I" proof (unfold has_products_def, intro conjI impI allI) show "I ≠ UNIV" using assms big_UNIV by blast fix J D assume D: "discrete_diagram J comp D ∧ Collect (partial_composition.arr J) = I" interpret J: category J using D discrete_diagram_def by blast interpret D: discrete_diagram J comp D using D by blast interpret incloD: composite_functor J comp Cls.comp D map .. interpret incloD: discrete_diagram J Cls.comp incloD.map using D.is_discrete by unfold_locales auto interpret incloD: diagram_in_set_category J Cls.comp ‹λA. A ⊆ Cls.Univ› incloD.map .. have 1: "small (Collect J.ide)" using assms D D.is_discrete by argo show "∃a. has_as_product J D a" proof - have 2: "∃a. Cls.has_as_product J incloD.map a" proof - have "Collect J.ide ≠ UNIV" using J.ide_def by blast thus ?thesis using 1 D.is_discrete Cls.has_small_products [of "Collect J.ide"] Cls.has_products_def [of "Collect J.ide"] incloD.discrete_diagram_axioms by presburger qed obtain ΠD where ΠD: "Cls.has_as_product J incloD.map ΠD" using 2 by blast interpret ΠD: constant_functor J Cls.comp ΠD using ΠD Cls.product_is_ide by unfold_locales auto obtain π where π: "product_cone J Cls.comp incloD.map ΠD π" using ΠD Cls.has_as_product_def by blast interpret π: product_cone J Cls.comp incloD.map ΠD π using π by blast have "small (Cls.hom Cls.unity ΠD)" proof - obtain φ where φ: "bij_betw φ (Cls.hom Cls.unity ΠD) (incloD.cones Cls.unity)" using incloD.limits_are_sets_of_cones π.limit_cone_axioms by blast let ?J = "ZFC_in_HOL.set (Collect J.arr)" let ?V_of_point = "λx. VLambda ?J (λj. V_of_arr (φ x j))" let ?Tuples = "VPi ?J (λj. ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j)))" have V_of_point: "?V_of_point ∈ Cls.hom Cls.unity ΠD → elts ?Tuples" proof fix x assume x: "x ∈ Cls.hom Cls.unity ΠD" have φx: "φ x ∈ incloD.cones Cls.unity" using φ x unfolding bij_betw_def by blast interpret φx: cone J Cls.comp incloD.map Cls.unity ‹φ x› using φx by blast have "⋀j. J.arr j ⟹ V_of_arr (φ x j) ∈ elts (ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j)))" proof - fix j assume j: "J.arr j" have "φ x j ∈ hom Cls.unity (D j)" by (metis (mono_tags, lifting) D.preserves_ide φx.component_in_hom cod_simp ideD(1,3) in_hom_char⇩_{F}⇩_{S}⇩_{b}⇩_{C}incloD.is_discrete incloD.preserves_cod j map_simp mem_Collect_eq o_apply terminal_char2 terminal_unity⇩_{S}⇩_{S}⇩_{C}) moreover have "V_of_arr ` hom Cls.unity (D j) = elts (ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j)))" using small_hom replacement by simp ultimately show "V_of_arr (φ x j) ∈ elts (ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j)))" using j φx bij_betw_hom_vfun(1) by blast qed thus "?V_of_point x ∈ elts ?Tuples" using VPi_I by fastforce qed have "?V_of_point ` Cls.hom Cls.unity ΠD ∈ range elts" proof - have "?V_of_point ` Cls.hom Cls.unity ΠD ⊆ elts ?Tuples" using V_of_point by blast thus ?thesis using smaller_than_small down_raw by auto qed moreover have "inj_on ?V_of_point (Cls.hom Cls.unity ΠD)" proof fix x y assume x: "x ∈ Cls.hom Cls.unity ΠD" and y: "y ∈ Cls.hom Cls.unity ΠD" and eq: "?V_of_point x = ?V_of_point y" have φx: "φ x ∈ incloD.cones Cls.unity" using φ x unfolding bij_betw_def by blast have φy: "φ y ∈ incloD.cones Cls.unity" using φ y unfolding bij_betw_def by blast interpret φx: cone J Cls.comp incloD.map Cls.unity ‹φ x› using φx by blast interpret φy: cone J Cls.comp incloD.map Cls.unity ‹φ y› using φy by blast have "φ x = φ y" proof - have "⋀j. j ∈ elts ?J ⟹ φ x j = φ y j" proof - fix j assume j: "j ∈ elts ?J" hence 3: "J.arr j" by (simp add: 1 incloD.is_discrete) have 4: "ide (D j)" using 3 incloD.is_discrete D.preserves_ide by force have 5:"ide Cls.unity" using Cls.terminal_unity⇩_{S}⇩_{C}terminal_char terminal_def by auto have φxj: "φ x j ∈ hom Cls.unity (D j)" using 3 4 5 incloD.is_discrete φx.preserves_hom φx.A.map_simp in_hom_char⇩_{F}⇩_{S}⇩_{b}⇩_{C}by (metis (no_types, lifting) J.ide_char φx.component_in_hom ideD(1) map_simp mem_Collect_eq o_apply) have φyj: "φ y j ∈ hom Cls.unity (D j)" using 3 4 5 incloD.is_discrete φy.preserves_hom φx.A.map_simp in_hom_char⇩_{F}⇩_{S}⇩_{b}⇩_{C}by (metis (no_types, lifting) J.ide_char φy.component_in_hom ideD(1) map_simp mem_Collect_eq o_apply) show "φ x j = φ y j" proof - have "⋀j. j ∈ elts ?J ⟹ V_of_arr (φ x j) = V_of_arr (φ y j)" using x eq VLambda_eq_D2 by blast thus ?thesis using V_of_arr_def by (metis (mono_tags, lifting) j φxj φyj bij_betw_hom_vfun(3) mem_Collect_eq) qed qed moreover have "elts ?J = Collect J.arr" by (simp add: 1 incloD.is_discrete) ultimately show ?thesis using φx.is_extensional φy.is_extensional by (metis HOL.ext mem_Collect_eq) qed thus "x = y" using x y φ bij_betw_imp_inj_on inj_on_def by (metis (no_types, lifting)) qed ultimately show "small (Cls.hom Cls.unity ΠD)" using small_def by blast qed hence "small (Cls.set ΠD)" by (simp add: Cls.set_def) hence 2: "ide ΠD" using ide_char⇩_{S}⇩_{S}⇩_{C}Cls.setp_set_ide Cls.product_is_ide ΠD unfolding setp_def by blast interpret ΠD': constant_functor J comp ΠD using 2 by unfold_locales interpret π': cone J comp D ΠD π proof - have "⋀j. J.arr j ⟹ «π j : ΠD → D j»" proof fix j assume j: "J.arr j" show 3: "arr (π j)" by (metis (mono_tags, lifting) 2 D.as_nat_trans.preserves_cod D.is_discrete D.preserves_ide π.component_in_hom ideD(1) ideD(3) in_homE in_hom_char⇩_{F}⇩_{S}⇩_{b}⇩_{C}j map_simp o_apply) show "dom (π j) = ΠD" using 3 arr_char⇩_{S}⇩_{b}⇩_{C}dom_char⇩_{S}⇩_{b}⇩_{C}π.preserves_dom by auto show "cod (π j) = D j" using 3 arr_char⇩_{S}⇩_{b}⇩_{C}cod_char⇩_{S}⇩_{b}⇩_{C}π.preserves_cod by (metis (no_types, lifting) Cls.ideD(3) D.preserves_arr functor.preserves_ide incloD.is_discrete incloD.is_functor incloD.preserves_cod j map_simp o_apply) qed moreover have "D.mkCone π = π" using π.is_extensional null_char by auto ultimately show "cone J comp D ΠD π" using 2 D.cone_mkCone [of ΠD π] by simp qed interpret π': product_cone J comp D ΠD π proof fix a χ' assume χ': "D.cone a χ'" interpret χ': cone J comp D a χ' using χ' by blast have a: "Cls.ide a" using ide_char⇩_{S}⇩_{b}⇩_{C}χ'.A.value_is_ide by blast moreover have "⋀j. J.arr j ⟹ Cls.in_hom (χ' j) a (incloD.map j)" proof - fix j assume j: "J.arr j" have "«χ' j : a → D j»" using j D.is_discrete χ'.component_in_hom by force thus "Cls.in_hom (χ' j) a (incloD.map j)" using a j D.is_discrete in_hom_char⇩_{F}⇩_{S}⇩_{b}⇩_{C}map_simp by auto qed ultimately have 3: "incloD.cone a (incloD.mkCone χ')" using incloD.cone_mkCone [of a χ'] by blast interpret χ: cone J Cls.comp incloD.map a ‹incloD.mkCone χ'› using 3 by blast have univ: "∃!f. Cls.in_hom f a ΠD ∧ incloD.cones_map f π = incloD.mkCone χ'" using χ.cone_axioms π.is_universal [of a "incloD.mkCone χ'"] by blast have 4: "incloD.mkCone χ' = χ'" using D.as_nat_trans.preserves_reflects_arr D.preserves_arr Limit.cone_def χ' χ'.is_extensional identity_functor.intro identity_functor.map_def incloD.as_nat_trans.is_extensional o_apply by fastforce have 5: "D.mkCone π = π" using π.is_extensional null_char by auto have 6: "⋀f. Cls.in_hom f a ΠD ⟹ incloD.cones_map f π = D.cones_map f π" proof - fix f assume f: "Cls.in_hom f a ΠD" have "incloD.cones_map f π = (λj. if J.arr j then Cls.comp (π j) f else Cls.null)" using f π.cone_axioms by auto also have "... = (λj. if J.arr j then comp (π j) f else null)" proof - have "⋀j. J.arr j ⟹ Cls.comp (π j) f = comp (π j) f" using f 2 comp_char in_hom_char⇩_{F}⇩_{S}⇩_{b}⇩_{C}seq_char⇩_{S}⇩_{b}⇩_{C}by (metis (no_types, lifting) Cls.ext Cls.in_homE χ'.ide_apex π'.preserves_reflects_arr arr_char⇩_{S}⇩_{b}⇩_{C}ide_char⇩_{S}⇩_{S}⇩_{C}) thus ?thesis using null_char by auto qed also have "... = D.cones_map f π" proof - have "π ∈ D.cones (cod f)" proof - have "«f : a → ΠD»" using f 2 in_hom_char⇩_{F}⇩_{S}⇩_{b}⇩_{C}χ'.ide_apex ideD(1) by presburger thus ?thesis using f π'.cone_axioms by blast qed thus ?thesis using ‹π ∈ D.cones (cod f)› by simp qed finally show "incloD.cones_map f π = D.cones_map f π" by blast qed moreover have "⋀f. «f : a → ΠD» ⟹ Cls.in_hom f a ΠD" using in_hom_char⇩_{F}⇩_{S}⇩_{b}⇩_{C}by blast show "∃!f. «f : a → ΠD» ∧ D.cones_map f π = χ'" proof - have "∃f. «f : a → ΠD» ∧ D.cones_map f π = χ'" using 2 4 5 6 univ χ'.ide_apex ideD(1) in_hom_char⇩_{F}⇩_{S}⇩_{b}⇩_{C}by (metis (no_types, lifting)) moreover have "⋀f g. ⟦«f : a → ΠD» ∧ D.cones_map f π = χ'; «g : a → ΠD» ∧ D.cones_map g π = χ'⟧ ⟹ f = g" using 2 4 5 6 univ χ'.ide_apex ideD(1) in_hom_char⇩_{F}⇩_{S}⇩_{b}⇩_{C}by auto ultimately show ?thesis by blast qed qed show ?thesis using π'.product_cone_axioms has_as_product_def by blast qed qed corollary has_small_products: assumes "small I" and "I ≠ UNIV" shows "has_products I" proof - have 1: "⋀I :: V set. small I ⟹ has_products I" using has_small_V_products by blast obtain φ where φ: "inj_on φ I ∧ φ ` I ∈ range elts" using assms small_def by metis have "bij_betw (inv_into I φ) (φ ` I) I" using φ bij_betw_inv_into bij_betw_imageI by metis moreover have "small (φ ` I)" using assms by auto ultimately show ?thesis using assms 1 has_products_preserved_by_bijection by blast qed theorem has_small_limits: assumes "category (J :: 'j comp)" and "small (Collect (partial_composition.arr J))" shows "has_limits_of_shape J" proof - interpret J: category J using assms by blast have "small (Collect J.ide)" using assms smaller_than_small [of "Collect J.arr" "Collect J.ide"] by fastforce moreover have "Collect J.ide ≠ UNIV" using J.ide_def by blast moreover have "Collect J.arr ≠ UNIV" using J.not_arr_null by blast ultimately show "has_limits_of_shape J" using assms has_small_products has_limits_if_has_products [of J] by blast qed sublocale concrete_set_category comp setp UNIV Cls.UP proof show "Cls.UP ∈ UNIV → Univ" using Cls.UP_mapsto terminal_char by presburger show "inj Cls.UP" using Cls.inj_UP by blast qed lemma is_concrete_set_category: shows "concrete_set_category comp setp UNIV Cls.UP" .. end text‹ In pure HOL (without ZFC), we were able to show that every category ‹C› has a ``hom functor'', but there was necessarily a dependence of the target set category of the hom functor on the arrow type of ‹C›. Using the construction of the present theory, we can now show that every ``locally small'' category ‹C› has a hom functor, whose target is the same set category for all such ‹C›. To obtain such a hom functor requires a choice, for each hom-set ‹hom a b› of ‹C›, of an injection of ‹hom a b› to the extension of a ‹V›-set. › locale locally_small_category = category + assumes locally_small: "⟦ide a; ide b⟧ ⟹ small (hom b a)" begin interpretation Cop: dual_category C .. interpretation CopxC: product_category Cop.comp C .. interpretation S: ZFC_set_cat . definition Hom where "Hom ≡ λ(b, a). S.UP o (SOME φ. φ ` hom b a ∈ range elts ∧ inj_on φ (hom b a))" interpretation Hom: hom_functor C S.comp S.setp Hom proof have 1: "⋀a b. Hom (b, a) ∈ hom b a → S.Univ ∧ inj_on (Hom (b, a)) (hom b a)" proof - fix a b show "Hom (b, a) ∈ hom b a → S.Univ ∧ inj_on (Hom (b, a)) (hom b a)" proof (cases "ide a ∧ ide b") show "¬ (ide a ∧ ide b) ⟹ ?thesis" using inj_on_def by fastforce assume ab: "ide a ∧ ide b" show ?thesis proof have 1: "∃φ. φ ` hom b a ∈ range elts ∧ inj_on φ (hom b a)" using ab locally_small [of a b] small_def [of "hom b a"] by blast let ?φ = "SOME φ. φ ` hom b a ∈ range elts ∧ inj_on φ (hom b a)" have φ: "?φ ` hom b a ∈ range elts ∧ inj_on ?φ (hom b a)" using 1 someI_ex [of "λφ. φ ` hom b a ∈ range elts ∧ inj_on φ (hom b a)"] by blast show "Hom (b, a) ∈ hom b a → S.Univ" unfolding Hom_def using φ S.UP_mapsto by auto show "inj_on (Hom (b, a)) (hom b a)" unfolding Hom_def apply simp using ab φ S.inj_UP comp_inj_on injD inj_on_def by (metis (no_types, lifting)) qed qed qed show "⋀f. arr f ⟹ Hom (dom f, cod f) f ∈ S.Univ" using 1 by blast show "⋀b a. ⟦ide b; ide a⟧ ⟹ inj_on (Hom (b, a)) (hom b a)" using 1 by blast show "⋀b a. ⟦ide b; ide a⟧ ⟹ S.setp (Hom (b, a) ` hom b a)" unfolding S.setp_def using 1 locally_small S.terminal_char by force qed lemma has_ZFC_hom_functor: shows "hom_functor C S.comp S.setp Hom" .. text‹ Using this result, we can now state a more traditional version of the Yoneda Lemma in which the target category of the Yoneda functor is the same for all locally small categories. › interpretation Y: yoneda_functor C S.comp S.setp Hom .. theorem ZFC_yoneda_lemma: assumes "ide a" and "functor Cop.comp S.comp F" shows "∃φ. bij_betw φ (S.set (F a)) {τ. natural_transformation Cop.comp S.comp (Y.Y a) F τ}" proof - interpret F: "functor" Cop.comp S.comp F using assms(2) by blast interpret F: set_valued_functor Cop.comp S.comp S.setp F .. interpret Ya: yoneda_functor_fixed_object C S.comp S.setp Hom a using assms(1) by unfold_locales blast interpret Ya: yoneda_lemma C S.comp S.setp Hom F a .. show ?thesis using Ya.yoneda_lemma by blast qed end end