Home | Metamath
Proof Explorer Theorem List (p. 180 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | setchom 17901 | Set of arrows of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ πΆ = (SetCatβπ) & β’ (π β π β π) & β’ π» = (Hom βπΆ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (ππ»π) = (π βm π)) | ||
Theorem | elsetchom 17902 | A morphism of sets is a function. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ πΆ = (SetCatβπ) & β’ (π β π β π) & β’ π» = (Hom βπΆ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πΉ β (ππ»π) β πΉ:πβΆπ)) | ||
Theorem | setccofval 17903* | Composition in the category of sets. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ πΆ = (SetCatβπ) & β’ (π β π β π) & β’ Β· = (compβπΆ) β β’ (π β Β· = (π£ β (π Γ π), π§ β π β¦ (π β (π§ βm (2nd βπ£)), π β ((2nd βπ£) βm (1st βπ£)) β¦ (π β π)))) | ||
Theorem | setcco 17904 | Composition in the category of sets. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ πΆ = (SetCatβπ) & β’ (π β π β π) & β’ Β· = (compβπΆ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β πΉ:πβΆπ) & β’ (π β πΊ:πβΆπ) β β’ (π β (πΊ(β¨π, πβ© Β· π)πΉ) = (πΊ β πΉ)) | ||
Theorem | setccatid 17905* | Lemma for setccat 17906. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ πΆ = (SetCatβπ) β β’ (π β π β (πΆ β Cat β§ (IdβπΆ) = (π₯ β π β¦ ( I βΎ π₯)))) | ||
Theorem | setccat 17906 | The category of sets is a category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ πΆ = (SetCatβπ) β β’ (π β π β πΆ β Cat) | ||
Theorem | setcid 17907 | The identity arrow in the category of sets is the identity function. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ πΆ = (SetCatβπ) & β’ 1 = (IdβπΆ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ( 1 βπ) = ( I βΎ π)) | ||
Theorem | setcmon 17908 | A monomorphism of sets is an injection. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ πΆ = (SetCatβπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ π = (MonoβπΆ) β β’ (π β (πΉ β (πππ) β πΉ:πβ1-1βπ)) | ||
Theorem | setcepi 17909 | An epimorphism of sets is a surjection. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ πΆ = (SetCatβπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ πΈ = (EpiβπΆ) & β’ (π β 2o β π) β β’ (π β (πΉ β (ππΈπ) β πΉ:πβontoβπ)) | ||
Theorem | setcsect 17910 | A section in the category of sets, written out. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ πΆ = (SetCatβπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ π = (SectβπΆ) β β’ (π β (πΉ(πππ)πΊ β (πΉ:πβΆπ β§ πΊ:πβΆπ β§ (πΊ β πΉ) = ( I βΎ π)))) | ||
Theorem | setcinv 17911 | An inverse in the category of sets is the converse operation. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ πΆ = (SetCatβπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ π = (InvβπΆ) β β’ (π β (πΉ(πππ)πΊ β (πΉ:πβ1-1-ontoβπ β§ πΊ = β‘πΉ))) | ||
Theorem | setciso 17912 | An isomorphism in the category of sets is a bijection. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ πΆ = (SetCatβπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ πΌ = (IsoβπΆ) β β’ (π β (πΉ β (ππΌπ) β πΉ:πβ1-1-ontoβπ)) | ||
Theorem | resssetc 17913 | The restriction of the category of sets to a subset is the category of sets in the subset. Thus, the SetCatβπ categories for different π are full subcategories of each other. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ πΆ = (SetCatβπ) & β’ π· = (SetCatβπ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ((Homf β(πΆ βΎs π)) = (Homf βπ·) β§ (compfβ(πΆ βΎs π)) = (compfβπ·))) | ||
Theorem | funcsetcres2 17914 | A functor into a smaller category of sets is a functor into the larger category. (Contributed by Mario Carneiro, 28-Jan-2017.) |
β’ πΆ = (SetCatβπ) & β’ π· = (SetCatβπ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πΈ Func π·) β (πΈ Func πΆ)) | ||
Theorem | setc2obas 17915 | β and 1o are distinct objects in (SetCatβ2o). This combined with setc2ohom 17916 demonstrates that the category does not have pairwise disjoint hom-sets. See also df-cat 17483 and cat1 17918. (Contributed by Zhi Wang, 24-Sep-2024.) |
β’ πΆ = (SetCatβ2o) & β’ π΅ = (BaseβπΆ) β β’ (β β π΅ β§ 1o β π΅ β§ 1o β β ) | ||
Theorem | setc2ohom 17916 | (SetCatβ2o) is a category (provable from setccat 17906 and 2oex 8391) that does not have pairwise disjoint hom-sets, proved by this theorem combined with setc2obas 17915. Notably, the empty set β is simultaneously an object (setc2obas 17915) , an identity morphism from β to β (setcid 17907 or thincid 46771) , and a non-identity morphism from β to 1o. See cat1lem 17917 and cat1 17918 for a more general statement. This category is also thin (setc2othin 46794), and therefore is "equivalent" to a preorder (actually a partial order). See prsthinc 46792 for more details on the "equivalence". (Contributed by Zhi Wang, 24-Sep-2024.) |
β’ πΆ = (SetCatβ2o) & β’ π» = (Hom βπΆ) β β’ β β ((β π»β ) β© (β π»1o)) | ||
Theorem | cat1lem 17917* | The category of sets in a "universe" containing the empty set and another set does not have pairwise disjoint hom-sets as required in Axiom CAT 1 in [Lang] p. 53. Lemma for cat1 17918. (Contributed by Zhi Wang, 15-Sep-2024.) |
β’ πΆ = (SetCatβπ) & β’ (π β π β π) & β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ (π β β β π) & β’ (π β π β π) & β’ (π β β β π) β β’ (π β βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ βπ€ β π΅ (((π₯π»π¦) β© (π§π»π€)) β β β§ Β¬ (π₯ = π§ β§ π¦ = π€))) | ||
Theorem | cat1 17918* | The definition of category df-cat 17483 does not impose pairwise disjoint hom-sets as required in Axiom CAT 1 in [Lang] p. 53. See setc2obas 17915 and setc2ohom 17916 for a counterexample. For a version with pairwise disjoint hom-sets, see df-homa 17847 and its subsection. (Contributed by Zhi Wang, 15-Sep-2024.) |
β’ βπ β Cat [(Baseβπ) / π][(Hom βπ) / β] Β¬ βπ₯ β π βπ¦ β π βπ§ β π βπ€ β π (((π₯βπ¦) β© (π§βπ€)) β β β (π₯ = π§ β§ π¦ = π€)) | ||
Syntax | ccatc 17919 | Extend class notation to include the category Cat. |
class CatCat | ||
Definition | df-catc 17920* | Definition of the category Cat, which consists of all categories in the universe π’ (i.e., "π’-small categories", see Definition 3.44. of [Adamek] p. 39), with functors as the morphisms. Definition 3.47 of [Adamek] p. 40. We do not introduce a specific definition for "π’ -large categories", which can be expressed as (Cat β π’). (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ CatCat = (π’ β V β¦ β¦(π’ β© Cat) / πβ¦{β¨(Baseβndx), πβ©, β¨(Hom βndx), (π₯ β π, π¦ β π β¦ (π₯ Func π¦))β©, β¨(compβndx), (π£ β (π Γ π), π§ β π β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π)))β©}) | ||
Theorem | catcval 17921* | Value of the category of categories (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ πΆ = (CatCatβπ) & β’ (π β π β π) & β’ (π β π΅ = (π β© Cat)) & β’ (π β π» = (π₯ β π΅, π¦ β π΅ β¦ (π₯ Func π¦))) & β’ (π β Β· = (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π)))) β β’ (π β πΆ = {β¨(Baseβndx), π΅β©, β¨(Hom βndx), π»β©, β¨(compβndx), Β· β©}) | ||
Theorem | catcbas 17922 | Set of objects of the category of categories. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ πΆ = (CatCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) β β’ (π β π΅ = (π β© Cat)) | ||
Theorem | catchomfval 17923* | Set of arrows of the category of categories (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ πΆ = (CatCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ π» = (Hom βπΆ) β β’ (π β π» = (π₯ β π΅, π¦ β π΅ β¦ (π₯ Func π¦))) | ||
Theorem | catchom 17924 | Set of arrows of the category of categories (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ πΆ = (CatCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ π» = (Hom βπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (ππ»π) = (π Func π)) | ||
Theorem | catccofval 17925* | Composition in the category of categories. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ πΆ = (CatCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ Β· = (compβπΆ) β β’ (π β Β· = (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) Func π§), π β ( Func βπ£) β¦ (π βfunc π)))) | ||
Theorem | catcco 17926 | Composition in the category of categories. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ πΆ = (CatCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ Β· = (compβπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ β (π Func π)) & β’ (π β πΊ β (π Func π)) β β’ (π β (πΊ(β¨π, πβ© Β· π)πΉ) = (πΊ βfunc πΉ)) | ||
Theorem | catccatid 17927* | Lemma for catccat 17929. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ πΆ = (CatCatβπ) & β’ π΅ = (BaseβπΆ) β β’ (π β π β (πΆ β Cat β§ (IdβπΆ) = (π₯ β π΅ β¦ (idfuncβπ₯)))) | ||
Theorem | catcid 17928 | The identity arrow in the category of categories is the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ πΆ = (CatCatβπ) & β’ π΅ = (BaseβπΆ) & β’ 1 = (IdβπΆ) & β’ πΌ = (idfuncβπ) & β’ (π β π β π) & β’ (π β π β π΅) β β’ (π β ( 1 βπ) = πΌ) | ||
Theorem | catccat 17929 | The category of categories is a category, see remark 3.48 in [Adamek] p. 40. (Clearly it cannot be an element of itself, hence it is "π -large".) (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ πΆ = (CatCatβπ) β β’ (π β π β πΆ β Cat) | ||
Theorem | resscatc 17930 | The restriction of the category of categories to a subset is the category of categories in the subset. Thus, the CatCatβπ categories for different π are full subcategories of each other. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ πΆ = (CatCatβπ) & β’ π· = (CatCatβπ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ((Homf β(πΆ βΎs π)) = (Homf βπ·) β§ (compfβ(πΆ βΎs π)) = (compfβπ·))) | ||
Theorem | catcisolem 17931* | Lemma for catciso 17932. (Contributed by Mario Carneiro, 29-Jan-2017.) |
β’ πΆ = (CatCatβπ) & β’ π΅ = (BaseβπΆ) & β’ π = (Baseβπ) & β’ π = (Baseβπ) & β’ (π β π β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ πΌ = (InvβπΆ) & β’ π» = (π₯ β π, π¦ β π β¦ β‘((β‘πΉβπ₯)πΊ(β‘πΉβπ¦))) & β’ (π β πΉ((π Full π) β© (π Faith π))πΊ) & β’ (π β πΉ:π β1-1-ontoβπ) β β’ (π β β¨πΉ, πΊβ©(ππΌπ)β¨β‘πΉ, π»β©) | ||
Theorem | catciso 17932 | A functor is an isomorphism of categories if and only if it is full and faithful, and is a bijection on the objects. Remark 3.28(2) in [Adamek] p. 34. (Contributed by Mario Carneiro, 29-Jan-2017.) |
β’ πΆ = (CatCatβπ) & β’ π΅ = (BaseβπΆ) & β’ π = (Baseβπ) & β’ π = (Baseβπ) & β’ (π β π β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ πΌ = (IsoβπΆ) β β’ (π β (πΉ β (ππΌπ) β (πΉ β ((π Full π) β© (π Faith π)) β§ (1st βπΉ):π β1-1-ontoβπ))) | ||
Theorem | catcbascl 17933 | An element of the base set of the category of categories for a weak universe belongs to the weak universe. Formerly part of the proof for catcoppccl 17938. (Contributed by AV, 14-Oct-2024.) |
β’ πΆ = (CatCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β WUni) & β’ (π β π β π΅) β β’ (π β π β π) | ||
Theorem | catcslotelcl 17934 | A slot entry of an element of the base set of the category of categories for a weak universe belongs to the weak universe. Formerly part of the proof for catcoppccl 17938. (Contributed by AV, 14-Oct-2024.) |
β’ πΆ = (CatCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β WUni) & β’ (π β π β π΅) & β’ πΈ = Slot (πΈβndx) β β’ (π β (πΈβπ) β π) | ||
Theorem | catcbaselcl 17935 | The base set of an element of the base set of the category of categories for a weak universe belongs to the weak universe. Formerly part of the proof for catcoppccl 17938. (Contributed by AV, 14-Oct-2024.) |
β’ πΆ = (CatCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β WUni) & β’ (π β π β π΅) β β’ (π β (Baseβπ) β π) | ||
Theorem | catchomcl 17936 | The Hom-set of an element of the base set of the category of categories for a weak universe belongs to the weak universe. Formerly part of the proof for catcoppccl 17938. (Contributed by AV, 14-Oct-2024.) |
β’ πΆ = (CatCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β WUni) & β’ (π β π β π΅) β β’ (π β (Hom βπ) β π) | ||
Theorem | catcccocl 17937 | The composition operation of an element of the base set of the category of categories for a weak universe belongs to the weak universe. Formerly part of the proof for catcoppccl 17938. (Contributed by AV, 14-Oct-2024.) |
β’ πΆ = (CatCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β WUni) & β’ (π β π β π΅) β β’ (π β (compβπ) β π) | ||
Theorem | catcoppccl 17938 | The category of categories for a weak universe is closed under taking opposites. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof shortened by AV, 13-Oct-2024.) |
β’ πΆ = (CatCatβπ) & β’ π΅ = (BaseβπΆ) & β’ π = (oppCatβπ) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β π β π΅) β β’ (π β π β π΅) | ||
Theorem | catcoppcclOLD 17939 | Obsolete proof of catcoppccl 17938 as of 13-Oct-2024. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ πΆ = (CatCatβπ) & β’ π΅ = (BaseβπΆ) & β’ π = (oppCatβπ) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β π β π΅) β β’ (π β π β π΅) | ||
Theorem | catcfuccl 17940 | The category of categories for a weak universe is closed under the functor category operation. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof shortened by AV, 14-Oct-2024.) |
β’ πΆ = (CatCatβπ) & β’ π΅ = (BaseβπΆ) & β’ π = (π FuncCat π) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β π β π΅) | ||
Theorem | catcfucclOLD 17941 | Obsolete proof of catcfuccl 17940 as of 14-Oct-2024. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ πΆ = (CatCatβπ) & β’ π΅ = (BaseβπΆ) & β’ π = (π FuncCat π) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β π β π΅) | ||
The "category of extensible structures" ExtStrCat is the category of all sets in a universe regarded as extensible structures and the functions between their base sets, see df-estrc 17945. Since we consider only "small categories" (i.e. categories whose objects and morphisms are actually sets and not proper classes), the objects of the category (i.e. the base set of the category regarded as extensible structure) are all sets in a universe π’, which can be an arbitrary set, see estrcbas 17947. Generally, we will take π’ to be a weak universe or Grothendieck universe, because these sets have closure properties as good as the real thing. If a set is not a real extensible structure, it is regarded as extensible structure with an empty base set. Because of bascnvimaeqv 17943 we do not need to restrict the universe to sets which "have a base". The morphisms (or arrows) between two objects, i.e. sets from the universe, are the mappings between their base sets, see estrchomfval 17948, whereas the composition is the ordinary composition of functions, see estrccofval 17951 and estrcco 17952. It is shown that the category of extensible structures ExtStrCat is actually a category, see estrccat 17955 with the identity function as identity arrow, see estrcid 17956. In the following, some background information about the category of extensible structures is given, taken from the discussion in Github issue #1507 (see https://github.com/metamath/set.mm/issues/1507 17956): At the beginning, the categories of non-unital rings RngCat and unital rings RingCat were defined separately (as unordered triples of ordereds pairs, see dfrngc2 45988 and dfringc2 46034, but with special compositions). With this definitions, however, Theorem rngcresringcat 46046 could not be proven, because the compositions were not compatible. Unfortunately, no precise definition of the composition within the category of rings could be found in the literature. In section 3.3 EXAMPLES, paragraph (2) of [Adamek] p. 22, however, a definition is given for "Grp", the category of groups: "The following constructs; i.e., categories of structured sets and structure-preserving functions between them (o will always be the composition of functions and idA will always be the identity function on A): ... (b) Grp with objects all groups and morphisms all homomorphisms between them." Therefore, the compositions should have been harmonized by using the composition of the category of sets SetCat, see df-setc 17897, which is the ordinary composition of functions. Analogously, categories of Rngs (and Rings) could have been shown to be restrictions resp. subcategories of the category of sets. BJ and MC observed, however, that "... βΎcat [cannot be used] to restrict the category Set to Ring, because the homs are different. Although Ring is a concrete category, a hom between rings R and S is a function (Base`R) --> (Base`S) with certain properties, unlike in Set where it is a function R --> S.". Therefore, MC suggested that "we could have an alternative version of the Set category consisting of extensible structures (in U) together with (A Hom B) := (Base`A) --> (Base`B). This category is not isomorphic to Set because different extensible structures can have the same base set, but it is equivalent to Set; the relevant functors are (U`A) = (Base`A), the forgetful functor, and (F`A) = { <. (Base`ndx), A >. }". This led to the current definition of ExtStrCat, see df-estrc 17945. The claimed equivalence is proven by equivestrcsetc 17975. Having a definition of a category of extensible structures, the categories of non-unital and unital rings can be defined as appropriate restrictions of the category of extensible structures, see df-rngc 45975 and df-ringc 46021. In the same way, more subcategories could be provided, resulting in the following "inclusion chain" by proving theorems like rngcresringcat 46046, although the morphisms of the shown categories are different ( "->" means "is subcategory of"): RingCat-> RngCat-> GrpCat -> MndCat -> MgmCat -> ExtStrCat According to MC, "If we generalize from subcategories to embeddings, then we can even fit SetCat into the chain, equivalent to ExtStrCat at the end." As mentioned before, the equivalence of SetCat and ExtStrCat is proven by equivestrcsetc 17975. Furthermore, it can be shown that SetCat is embedded into ExtStrCat, see embedsetcestrc 17990. Remark: equivestrcsetc 17975 as well as embedsetcestrc 17990 require that the index of the base set extractor is contained within the considered universe. This is ensured by assuming that the natural numbers are contained within the considered universe: Ο β π (see wunndx 17002), but it would be currently sufficient to assume that 1 β π, because the index value of the base set extractor is hard-coded as 1, see basendx 17027. Some people, however, feel uncomfortable to say that a ring "is a" group (without mentioning the restriction to the addition, which is usually found in the literature, e.g., the definition of a ring in [Herstein] p. 126: "... Note that so far all we have said is that R is an abelian group under +.". The main argument against a ring being a group is the number of components/slots: usually, a group consists of (exactly!) two components (a base set and an operation), whereas a ring consists of (exactly!) three components (a base set and two operations). According to this "definition", a ring cannot be a group. This is also an (unfortunately informal) argument for the category of rings not being a subcategory of the category of abelian groups in "Categories and Functors", Bodo Pareigis, Academic Press, New York, London, 1970: "A category A is called a subcategory of a category B if Ob(A) β Ob(B) and MorA(X,Y) β MorB(X,Y) for all X,Y e. Ob(A), if the composition of morphisms in A coincides with the composition of the same morphisms in B and if the identity of an object in A is also the identity of the same object viewed as an object in B. Then there is a forgetful functor from A to B. We note that Ri [the category of rings] is not a subcategory of Ab [the category of abelian groups]. In fact, Ob(Ri) β Ob(Ab) is not true, although every ring can also be regarded as an abelian group. The corresponding abelian groups of two rings may coincide even if the rings do not coincide. The multiplication may be defined differently.". As long as we define Rings, Groups, etc. in a way that π΄ β Ring β π΄ β Grp is valid (see ringgrp 19893) the corresponding categories are in a subcategory relation. If we do not want Rings to be Groups (then the category of rings would not be a subcategory of the category of groups, as observed by Pareigis), we would have to change the definitions of Magmas, Monoids, Groups, Rings etc. to restrict them to have exactly the required number of slots, so that the following holds π β Grp β π Struct β¨(Baseβndx), (+gβndx)β© π β Ring β π Struct β¨(Baseβndx), (+gβndx), (.rβndx)β© | ||
Theorem | fncnvimaeqv 17942 | The inverse images of the universal class V under functions on the universal class V are the universal class V itself. (Proposed by Mario Carneiro, 7-Mar-2020.) (Contributed by AV, 7-Mar-2020.) |
β’ (πΉ Fn V β (β‘πΉ β V) = V) | ||
Theorem | bascnvimaeqv 17943 | The inverse image of the universal class V under the base function is the universal class V itself. (Proposed by Mario Carneiro, 7-Mar-2020.) (Contributed by AV, 7-Mar-2020.) |
β’ (β‘Base β V) = V | ||
Syntax | cestrc 17944 | Extend class notation to include the category ExtStr. |
class ExtStrCat | ||
Definition | df-estrc 17945* | Definition of the category ExtStr of extensible structures. This is the category whose objects are all sets in a universe π’ regarded as extensible structures and whose morphisms are the functions between their base sets. If a set is not a real extensible structure, it is regarded as extensible structure with an empty base set. Because of bascnvimaeqv 17943 we do not need to restrict the universe to sets which "have a base". Generally, we will take π’ to be a weak universe or Grothendieck universe, because these sets have closure properties as good as the real thing. (Proposed by Mario Carneiro, 5-Mar-2020.) (Contributed by AV, 7-Mar-2020.) |
β’ ExtStrCat = (π’ β V β¦ {β¨(Baseβndx), π’β©, β¨(Hom βndx), (π₯ β π’, π¦ β π’ β¦ ((Baseβπ¦) βm (Baseβπ₯)))β©, β¨(compβndx), (π£ β (π’ Γ π’), π§ β π’ β¦ (π β ((Baseβπ§) βm (Baseβ(2nd βπ£))), π β ((Baseβ(2nd βπ£)) βm (Baseβ(1st βπ£))) β¦ (π β π)))β©}) | ||
Theorem | estrcval 17946* | Value of the category of extensible structures (in a universe). (Contributed by AV, 7-Mar-2020.) |
β’ πΆ = (ExtStrCatβπ) & β’ (π β π β π) & β’ (π β π» = (π₯ β π, π¦ β π β¦ ((Baseβπ¦) βm (Baseβπ₯)))) & β’ (π β Β· = (π£ β (π Γ π), π§ β π β¦ (π β ((Baseβπ§) βm (Baseβ(2nd βπ£))), π β ((Baseβ(2nd βπ£)) βm (Baseβ(1st βπ£))) β¦ (π β π)))) β β’ (π β πΆ = {β¨(Baseβndx), πβ©, β¨(Hom βndx), π»β©, β¨(compβndx), Β· β©}) | ||
Theorem | estrcbas 17947 | Set of objects of the category of extensible structures (in a universe). (Contributed by AV, 7-Mar-2020.) |
β’ πΆ = (ExtStrCatβπ) & β’ (π β π β π) β β’ (π β π = (BaseβπΆ)) | ||
Theorem | estrchomfval 17948* | Set of morphisms ("arrows") of the category of extensible structures (in a universe). (Contributed by AV, 7-Mar-2020.) |
β’ πΆ = (ExtStrCatβπ) & β’ (π β π β π) & β’ π» = (Hom βπΆ) β β’ (π β π» = (π₯ β π, π¦ β π β¦ ((Baseβπ¦) βm (Baseβπ₯)))) | ||
Theorem | estrchom 17949 | The morphisms between extensible structures are mappings between their base sets. (Contributed by AV, 7-Mar-2020.) |
β’ πΆ = (ExtStrCatβπ) & β’ (π β π β π) & β’ π» = (Hom βπΆ) & β’ (π β π β π) & β’ (π β π β π) & β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) β β’ (π β (ππ»π) = (π΅ βm π΄)) | ||
Theorem | elestrchom 17950 | A morphism between extensible structures is a function between their base sets. (Contributed by AV, 7-Mar-2020.) |
β’ πΆ = (ExtStrCatβπ) & β’ (π β π β π) & β’ π» = (Hom βπΆ) & β’ (π β π β π) & β’ (π β π β π) & β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) β β’ (π β (πΉ β (ππ»π) β πΉ:π΄βΆπ΅)) | ||
Theorem | estrccofval 17951* | Composition in the category of extensible structures. (Contributed by AV, 7-Mar-2020.) |
β’ πΆ = (ExtStrCatβπ) & β’ (π β π β π) & β’ Β· = (compβπΆ) β β’ (π β Β· = (π£ β (π Γ π), π§ β π β¦ (π β ((Baseβπ§) βm (Baseβ(2nd βπ£))), π β ((Baseβ(2nd βπ£)) βm (Baseβ(1st βπ£))) β¦ (π β π)))) | ||
Theorem | estrcco 17952 | Composition in the category of extensible structures. (Contributed by AV, 7-Mar-2020.) |
β’ πΆ = (ExtStrCatβπ) & β’ (π β π β π) & β’ Β· = (compβπΆ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ π· = (Baseβπ) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β πΊ:π΅βΆπ·) β β’ (π β (πΊ(β¨π, πβ© Β· π)πΉ) = (πΊ β πΉ)) | ||
Theorem | estrcbasbas 17953 | An element of the base set of the base set of the category of extensible structures (i.e. the base set of an extensible structure) belongs to the considered weak universe. (Contributed by AV, 22-Mar-2020.) |
β’ πΆ = (ExtStrCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β WUni) β β’ ((π β§ πΈ β π΅) β (BaseβπΈ) β π) | ||
Theorem | estrccatid 17954* | Lemma for estrccat 17955. (Contributed by AV, 8-Mar-2020.) |
β’ πΆ = (ExtStrCatβπ) β β’ (π β π β (πΆ β Cat β§ (IdβπΆ) = (π₯ β π β¦ ( I βΎ (Baseβπ₯))))) | ||
Theorem | estrccat 17955 | The category of extensible structures is a category. (Contributed by AV, 8-Mar-2020.) |
β’ πΆ = (ExtStrCatβπ) β β’ (π β π β πΆ β Cat) | ||
Theorem | estrcid 17956 | The identity arrow in the category of extensible structures is the identity function of base sets. (Contributed by AV, 8-Mar-2020.) |
β’ πΆ = (ExtStrCatβπ) & β’ 1 = (IdβπΆ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ( 1 βπ) = ( I βΎ (Baseβπ))) | ||
Theorem | estrchomfn 17957 | The Hom-set operation in the category of extensible structures (in a universe) is a function. (Contributed by AV, 8-Mar-2020.) |
β’ πΆ = (ExtStrCatβπ) & β’ (π β π β π) & β’ π» = (Hom βπΆ) β β’ (π β π» Fn (π Γ π)) | ||
Theorem | estrchomfeqhom 17958 | The functionalized Hom-set operation equals the Hom-set operation in the category of extensible structures (in a universe). (Contributed by AV, 8-Mar-2020.) |
β’ πΆ = (ExtStrCatβπ) & β’ (π β π β π) & β’ π» = (Hom βπΆ) β β’ (π β (Homf βπΆ) = π») | ||
Theorem | estrreslem1 17959 | Lemma 1 for estrres 17962. (Contributed by AV, 14-Mar-2020.) (Proof shortened by AV, 28-Oct-2024.) |
β’ (π β πΆ = {β¨(Baseβndx), π΅β©, β¨(Hom βndx), π»β©, β¨(compβndx), Β· β©}) & β’ (π β π΅ β π) β β’ (π β π΅ = (BaseβπΆ)) | ||
Theorem | estrreslem1OLD 17960 | Obsolete version of estrreslem1 17959 as of 28-Oct-2024. Lemma 1 for estrres 17962. (Contributed by AV, 14-Mar-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β πΆ = {β¨(Baseβndx), π΅β©, β¨(Hom βndx), π»β©, β¨(compβndx), Β· β©}) & β’ (π β π΅ β π) β β’ (π β π΅ = (BaseβπΆ)) | ||
Theorem | estrreslem2 17961 | Lemma 2 for estrres 17962. (Contributed by AV, 14-Mar-2020.) |
β’ (π β πΆ = {β¨(Baseβndx), π΅β©, β¨(Hom βndx), π»β©, β¨(compβndx), Β· β©}) & β’ (π β π΅ β π) & β’ (π β π» β π) & β’ (π β Β· β π) β β’ (π β (Baseβndx) β dom πΆ) | ||
Theorem | estrres 17962 | Any restriction of a category (as an extensible structure which is an unordered triple of ordered pairs) is an unordered triple of ordered pairs. (Contributed by AV, 15-Mar-2020.) (Revised by AV, 3-Jul-2022.) |
β’ (π β πΆ = {β¨(Baseβndx), π΅β©, β¨(Hom βndx), π»β©, β¨(compβndx), Β· β©}) & β’ (π β π΅ β π) & β’ (π β π» β π) & β’ (π β Β· β π) & β’ (π β πΊ β π) & β’ (π β π΄ β π΅) β β’ (π β ((πΆ βΎs π΄) sSet β¨(Hom βndx), πΊβ©) = {β¨(Baseβndx), π΄β©, β¨(Hom βndx), πΊβ©, β¨(compβndx), Β· β©}) | ||
Theorem | funcestrcsetclem1 17963* | Lemma 1 for funcestrcsetc 17972. (Contributed by AV, 22-Mar-2020.) |
β’ πΈ = (ExtStrCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (BaseβπΈ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) β β’ ((π β§ π β π΅) β (πΉβπ) = (Baseβπ)) | ||
Theorem | funcestrcsetclem2 17964* | Lemma 2 for funcestrcsetc 17972. (Contributed by AV, 22-Mar-2020.) |
β’ πΈ = (ExtStrCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (BaseβπΈ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) β β’ ((π β§ π β π΅) β (πΉβπ) β π) | ||
Theorem | funcestrcsetclem3 17965* | Lemma 3 for funcestrcsetc 17972. (Contributed by AV, 22-Mar-2020.) |
β’ πΈ = (ExtStrCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (BaseβπΈ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) β β’ (π β πΉ:π΅βΆπΆ) | ||
Theorem | funcestrcsetclem4 17966* | Lemma 4 for funcestrcsetc 17972. (Contributed by AV, 22-Mar-2020.) |
β’ πΈ = (ExtStrCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (BaseβπΈ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ ((Baseβπ¦) βm (Baseβπ₯))))) β β’ (π β πΊ Fn (π΅ Γ π΅)) | ||
Theorem | funcestrcsetclem5 17967* | Lemma 5 for funcestrcsetc 17972. (Contributed by AV, 23-Mar-2020.) |
β’ πΈ = (ExtStrCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (BaseβπΈ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ ((Baseβπ¦) βm (Baseβπ₯))))) & β’ π = (Baseβπ) & β’ π = (Baseβπ) β β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΊπ) = ( I βΎ (π βm π))) | ||
Theorem | funcestrcsetclem6 17968* | Lemma 6 for funcestrcsetc 17972. (Contributed by AV, 23-Mar-2020.) |
β’ πΈ = (ExtStrCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (BaseβπΈ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ ((Baseβπ¦) βm (Baseβπ₯))))) & β’ π = (Baseβπ) & β’ π = (Baseβπ) β β’ ((π β§ (π β π΅ β§ π β π΅) β§ π» β (π βm π)) β ((ππΊπ)βπ») = π») | ||
Theorem | funcestrcsetclem7 17969* | Lemma 7 for funcestrcsetc 17972. (Contributed by AV, 23-Mar-2020.) |
β’ πΈ = (ExtStrCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (BaseβπΈ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ ((Baseβπ¦) βm (Baseβπ₯))))) β β’ ((π β§ π β π΅) β ((ππΊπ)β((IdβπΈ)βπ)) = ((Idβπ)β(πΉβπ))) | ||
Theorem | funcestrcsetclem8 17970* | Lemma 8 for funcestrcsetc 17972. (Contributed by AV, 15-Feb-2020.) |
β’ πΈ = (ExtStrCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (BaseβπΈ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ ((Baseβπ¦) βm (Baseβπ₯))))) β β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΊπ):(π(Hom βπΈ)π)βΆ((πΉβπ)(Hom βπ)(πΉβπ))) | ||
Theorem | funcestrcsetclem9 17971* | Lemma 9 for funcestrcsetc 17972. (Contributed by AV, 23-Mar-2020.) |
β’ πΈ = (ExtStrCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (BaseβπΈ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ ((Baseβπ¦) βm (Baseβπ₯))))) β β’ ((π β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π» β (π(Hom βπΈ)π) β§ πΎ β (π(Hom βπΈ)π))) β ((ππΊπ)β(πΎ(β¨π, πβ©(compβπΈ)π)π»)) = (((ππΊπ)βπΎ)(β¨(πΉβπ), (πΉβπ)β©(compβπ)(πΉβπ))((ππΊπ)βπ»))) | ||
Theorem | funcestrcsetc 17972* | The "natural forgetful functor" from the category of extensible structures into the category of sets which sends each extensible structure to its base set, preserving the morphisms as mappings between the corresponding base sets. (Contributed by AV, 23-Mar-2020.) |
β’ πΈ = (ExtStrCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (BaseβπΈ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ ((Baseβπ¦) βm (Baseβπ₯))))) β β’ (π β πΉ(πΈ Func π)πΊ) | ||
Theorem | fthestrcsetc 17973* | The "natural forgetful functor" from the category of extensible structures into the category of sets which sends each extensible structure to its base set is faithful. (Contributed by AV, 2-Apr-2020.) |
β’ πΈ = (ExtStrCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (BaseβπΈ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ ((Baseβπ¦) βm (Baseβπ₯))))) β β’ (π β πΉ(πΈ Faith π)πΊ) | ||
Theorem | fullestrcsetc 17974* | The "natural forgetful functor" from the category of extensible structures into the category of sets which sends each extensible structure to its base set is full. (Contributed by AV, 2-Apr-2020.) |
β’ πΈ = (ExtStrCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (BaseβπΈ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ ((Baseβπ¦) βm (Baseβπ₯))))) β β’ (π β πΉ(πΈ Full π)πΊ) | ||
Theorem | equivestrcsetc 17975* | The "natural forgetful functor" from the category of extensible structures into the category of sets which sends each extensible structure to its base set is an equivalence. According to definition 3.33 (1) of [Adamek] p. 36, "A functor F : A -> B is called an equivalence provided that it is full, faithful, and isomorphism-dense in the sense that for any B-object B' there exists some A-object A' such that F(A') is isomorphic to B'.". Therefore, the category of sets and the category of extensible structures are equivalent, according to definition 3.33 (2) of [Adamek] p. 36, "Categories A and B are called equivalent provided that there is an equivalence from A to B.". (Contributed by AV, 2-Apr-2020.) |
β’ πΈ = (ExtStrCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (BaseβπΈ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ ((Baseβπ¦) βm (Baseβπ₯))))) & β’ (π β (Baseβndx) β π) β β’ (π β (πΉ(πΈ Faith π)πΊ β§ πΉ(πΈ Full π)πΊ β§ βπ β πΆ βπ β π΅ βπ π:πβ1-1-ontoβ(πΉβπ))) | ||
Theorem | setc1strwun 17976 | A constructed one-slot structure with the objects of the category of sets as base set in a weak universe. (Contributed by AV, 27-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β Ο β π) β β’ ((π β§ π β πΆ) β {β¨(Baseβndx), πβ©} β π) | ||
Theorem | funcsetcestrclem1 17977* | Lemma 1 for funcsetcestrc 17987. (Contributed by AV, 27-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) β β’ ((π β§ π β πΆ) β (πΉβπ) = {β¨(Baseβndx), πβ©}) | ||
Theorem | funcsetcestrclem2 17978* | Lemma 2 for funcsetcestrc 17987. (Contributed by AV, 27-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) β β’ ((π β§ π β πΆ) β (πΉβπ) β π) | ||
Theorem | funcsetcestrclem3 17979* | Lemma 3 for funcsetcestrc 17987. (Contributed by AV, 27-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ πΈ = (ExtStrCatβπ) & β’ π΅ = (BaseβπΈ) β β’ (π β πΉ:πΆβΆπ΅) | ||
Theorem | embedsetcestrclem 17980* | Lemma for embedsetcestrc 17990. (Contributed by AV, 31-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ πΈ = (ExtStrCatβπ) & β’ π΅ = (BaseβπΈ) β β’ (π β πΉ:πΆβ1-1βπ΅) | ||
Theorem | funcsetcestrclem4 17981* | Lemma 4 for funcsetcestrc 17987. (Contributed by AV, 27-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β πΊ = (π₯ β πΆ, π¦ β πΆ β¦ ( I βΎ (π¦ βm π₯)))) β β’ (π β πΊ Fn (πΆ Γ πΆ)) | ||
Theorem | funcsetcestrclem5 17982* | Lemma 5 for funcsetcestrc 17987. (Contributed by AV, 27-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β πΊ = (π₯ β πΆ, π¦ β πΆ β¦ ( I βΎ (π¦ βm π₯)))) β β’ ((π β§ (π β πΆ β§ π β πΆ)) β (ππΊπ) = ( I βΎ (π βm π))) | ||
Theorem | funcsetcestrclem6 17983* | Lemma 6 for funcsetcestrc 17987. (Contributed by AV, 27-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β πΊ = (π₯ β πΆ, π¦ β πΆ β¦ ( I βΎ (π¦ βm π₯)))) β β’ ((π β§ (π β πΆ β§ π β πΆ) β§ π» β (π βm π)) β ((ππΊπ)βπ») = π») | ||
Theorem | funcsetcestrclem7 17984* | Lemma 7 for funcsetcestrc 17987. (Contributed by AV, 27-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β πΊ = (π₯ β πΆ, π¦ β πΆ β¦ ( I βΎ (π¦ βm π₯)))) & β’ πΈ = (ExtStrCatβπ) β β’ ((π β§ π β πΆ) β ((ππΊπ)β((Idβπ)βπ)) = ((IdβπΈ)β(πΉβπ))) | ||
Theorem | funcsetcestrclem8 17985* | Lemma 8 for funcsetcestrc 17987. (Contributed by AV, 28-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β πΊ = (π₯ β πΆ, π¦ β πΆ β¦ ( I βΎ (π¦ βm π₯)))) & β’ πΈ = (ExtStrCatβπ) β β’ ((π β§ (π β πΆ β§ π β πΆ)) β (ππΊπ):(π(Hom βπ)π)βΆ((πΉβπ)(Hom βπΈ)(πΉβπ))) | ||
Theorem | funcsetcestrclem9 17986* | Lemma 9 for funcsetcestrc 17987. (Contributed by AV, 28-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β πΊ = (π₯ β πΆ, π¦ β πΆ β¦ ( I βΎ (π¦ βm π₯)))) & β’ πΈ = (ExtStrCatβπ) β β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ) β§ (π» β (π(Hom βπ)π) β§ πΎ β (π(Hom βπ)π))) β ((ππΊπ)β(πΎ(β¨π, πβ©(compβπ)π)π»)) = (((ππΊπ)βπΎ)(β¨(πΉβπ), (πΉβπ)β©(compβπΈ)(πΉβπ))((ππΊπ)βπ»))) | ||
Theorem | funcsetcestrc 17987* | The "embedding functor" from the category of sets into the category of extensible structures which sends each set to an extensible structure consisting of the base set slot only, preserving the morphisms as mappings between the corresponding base sets. (Contributed by AV, 28-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β πΊ = (π₯ β πΆ, π¦ β πΆ β¦ ( I βΎ (π¦ βm π₯)))) & β’ πΈ = (ExtStrCatβπ) β β’ (π β πΉ(π Func πΈ)πΊ) | ||
Theorem | fthsetcestrc 17988* | The "embedding functor" from the category of sets into the category of extensible structures which sends each set to an extensible structure consisting of the base set slot only is faithful. (Contributed by AV, 31-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β πΊ = (π₯ β πΆ, π¦ β πΆ β¦ ( I βΎ (π¦ βm π₯)))) & β’ πΈ = (ExtStrCatβπ) β β’ (π β πΉ(π Faith πΈ)πΊ) | ||
Theorem | fullsetcestrc 17989* | The "embedding functor" from the category of sets into the category of extensible structures which sends each set to an extensible structure consisting of the base set slot only is full. (Contributed by AV, 1-Apr-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β πΊ = (π₯ β πΆ, π¦ β πΆ β¦ ( I βΎ (π¦ βm π₯)))) & β’ πΈ = (ExtStrCatβπ) β β’ (π β πΉ(π Full πΈ)πΊ) | ||
Theorem | embedsetcestrc 17990* | The "embedding functor" from the category of sets into the category of extensible structures which sends each set to an extensible structure consisting of the base set slot only is an embedding. According to definition 3.27 (1) of [Adamek] p. 34, a functor "F is called an embedding provided that F is injective on morphisms", or according to remark 3.28 (1) in [Adamek] p. 34, "a functor is an embedding if and only if it is faithful and injective on objects". (Contributed by AV, 31-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β πΊ = (π₯ β πΆ, π¦ β πΆ β¦ ( I βΎ (π¦ βm π₯)))) & β’ πΈ = (ExtStrCatβπ) & β’ π΅ = (BaseβπΈ) β β’ (π β (πΉ(π Faith πΈ)πΊ β§ πΉ:πΆβ1-1βπ΅)) | ||
Syntax | cxpc 17991 | Extend class notation with the product of two categories. |
class Γc | ||
Syntax | c1stf 17992 | Extend class notation with the first projection functor. |
class 1stF | ||
Syntax | c2ndf 17993 | Extend class notation with the second projection functor. |
class 2ndF | ||
Syntax | cprf 17994 | Extend class notation with the functor pairing operation. |
class β¨,β©F | ||
Definition | df-xpc 17995* | Define the binary product of categories, which has objects for each pair of objects of the factors, and morphisms for each pair of morphisms of the factors. Composition is componentwise. (Contributed by Mario Carneiro, 10-Jan-2017.) |
β’ Γc = (π β V, π β V β¦ β¦((Baseβπ) Γ (Baseβπ )) / πβ¦β¦(π’ β π, π£ β π β¦ (((1st βπ’)(Hom βπ)(1st βπ£)) Γ ((2nd βπ’)(Hom βπ )(2nd βπ£)))) / ββ¦{β¨(Baseβndx), πβ©, β¨(Hom βndx), ββ©, β¨(compβndx), (π₯ β (π Γ π), π¦ β π β¦ (π β ((2nd βπ₯)βπ¦), π β (ββπ₯) β¦ β¨((1st βπ)(β¨(1st β(1st βπ₯)), (1st β(2nd βπ₯))β©(compβπ)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd β(1st βπ₯)), (2nd β(2nd βπ₯))β©(compβπ )(2nd βπ¦))(2nd βπ))β©))β©}) | ||
Definition | df-1stf 17996* | Define the first projection functor out of the product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ 1stF = (π β Cat, π β Cat β¦ β¦((Baseβπ) Γ (Baseβπ )) / πβ¦β¨(1st βΎ π), (π₯ β π, π¦ β π β¦ (1st βΎ (π₯(Hom β(π Γc π ))π¦)))β©) | ||
Definition | df-2ndf 17997* | Define the second projection functor out of the product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ 2ndF = (π β Cat, π β Cat β¦ β¦((Baseβπ) Γ (Baseβπ )) / πβ¦β¨(2nd βΎ π), (π₯ β π, π¦ β π β¦ (2nd βΎ (π₯(Hom β(π Γc π ))π¦)))β©) | ||
Definition | df-prf 17998* | Define the pairing operation for functors (which takes two functors πΉ:πΆβΆπ· and πΊ:πΆβΆπΈ and produces (πΉ β¨,β©F πΊ):πΆβΆ(π· Γc πΈ)). (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ β¨,β©F = (π β V, π β V β¦ β¦dom (1st βπ) / πβ¦β¨(π₯ β π β¦ β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©), (π₯ β π, π¦ β π β¦ (β β dom (π₯(2nd βπ)π¦) β¦ β¨((π₯(2nd βπ)π¦)ββ), ((π₯(2nd βπ)π¦)ββ)β©))β©) | ||
Theorem | fnxpc 17999 | The binary product of categories is a two-argument function. (Contributed by Mario Carneiro, 10-Jan-2017.) |
β’ Γc Fn (V Γ V) | ||
Theorem | xpcval 18000* | Value of the binary product of categories. (Contributed by Mario Carneiro, 10-Jan-2017.) |
β’ π = (πΆ Γc π·) & β’ π = (BaseβπΆ) & β’ π = (Baseβπ·) & β’ π» = (Hom βπΆ) & β’ π½ = (Hom βπ·) & β’ Β· = (compβπΆ) & β’ β = (compβπ·) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β π΅ = (π Γ π)) & β’ (π β πΎ = (π’ β π΅, π£ β π΅ β¦ (((1st βπ’)π»(1st βπ£)) Γ ((2nd βπ’)π½(2nd βπ£))))) & β’ (π β π = (π₯ β (π΅ Γ π΅), π¦ β π΅ β¦ (π β ((2nd βπ₯)πΎπ¦), π β (πΎβπ₯) β¦ β¨((1st βπ)(β¨(1st β(1st βπ₯)), (1st β(2nd βπ₯))β© Β· (1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd β(1st βπ₯)), (2nd β(2nd βπ₯))β© β (2nd βπ¦))(2nd βπ))β©))) β β’ (π β π = {β¨(Baseβndx), π΅β©, β¨(Hom βndx), πΎβ©, β¨(compβndx), πβ©}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |