Home | Metamath
Proof Explorer Theorem List (p. 168 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | arwhom 16701 | The second component of an arrow is the corresponding morphism (without the domain/codomain tag). (Contributed by Mario Carneiro, 11-Jan-2017.) |
Nat coda | ||
Theorem | arwdmcd 16702 | Decompose an arrow into domain, codomain, and morphism. (Contributed by Mario Carneiro, 11-Jan-2017.) |
Nat coda | ||
Syntax | cida 16703 | Extend class notation to include identity for arrows. |
Ida | ||
Syntax | ccoa 16704 | Extend class notation to include composition for arrows. |
compa | ||
Definition | df-ida 16705* | Definition of the identity arrow, which is just the identity morphism tagged with its domain and codomain. (Contributed by FL, 26-Oct-2007.) (Revised by Mario Carneiro, 11-Jan-2017.) |
Ida | ||
Definition | df-coa 16706* | Definition of the composition of arrows. Since arrows are tagged with domain and codomain, this does not need to be a quinary operation like the regular composition in a category comp. Instead, it is a partial binary operation on arrows, which is defined when the domain of the first arrow matches the codomain of the second. (Contributed by Mario Carneiro, 11-Jan-2017.) |
compa Nat Nat coda coda compcoda | ||
Theorem | idafval 16707* | Value of the identity arrow function. (Contributed by Mario Carneiro, 11-Jan-2017.) |
Ida | ||
Theorem | idaval 16708 | Value of the identity arrow function. (Contributed by Mario Carneiro, 11-Jan-2017.) |
Ida | ||
Theorem | ida2 16709 | Morphism part of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.) |
Ida | ||
Theorem | idahom 16710 | Domain and codomain of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.) |
Ida Homa | ||
Theorem | idadm 16711 | Domain of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.) |
Ida | ||
Theorem | idacd 16712 | Codomain of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.) |
Ida coda | ||
Theorem | idaf 16713 | The identity arrow function is a function from objects to arrows. (Contributed by Mario Carneiro, 11-Jan-2017.) |
Ida Nat | ||
Theorem | coafval 16714* | The value of the composition of arrows. (Contributed by Mario Carneiro, 11-Jan-2017.) |
compa Nat comp coda coda coda | ||
Theorem | eldmcoa 16715 | A pair is in the domain of the arrow composition, if the domain of equals the codomain of . (In this case we say and are composable.) (Contributed by Mario Carneiro, 11-Jan-2017.) |
compa Nat coda | ||
Theorem | dmcoass 16716 | The domain of composition is a collection of pairs of arrows. (Contributed by Mario Carneiro, 11-Jan-2017.) |
compa Nat | ||
Theorem | homdmcoa 16717 | If and , then and are composable. (Contributed by Mario Carneiro, 11-Jan-2017.) |
compa Homa | ||
Theorem | coaval 16718 | Value of composition for composable arrows. (Contributed by Mario Carneiro, 11-Jan-2017.) |
compa Homa comp | ||
Theorem | coa2 16719 | The morphism part of arrow composition. (Contributed by Mario Carneiro, 11-Jan-2017.) |
compa Homa comp | ||
Theorem | coahom 16720 | The composition of two composable arrows is an arrow. (Contributed by Mario Carneiro, 11-Jan-2017.) |
compa Homa | ||
Theorem | coapm 16721 | Composition of arrows is a partial binary operation on arrows. (Contributed by Mario Carneiro, 11-Jan-2017.) |
compa Nat | ||
Theorem | arwlid 16722 | Left identity of a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017.) |
Homa compa Ida | ||
Theorem | arwrid 16723 | Right identity of a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017.) |
Homa compa Ida | ||
Theorem | arwass 16724 | Associativity of composition in a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017.) |
Homa compa Ida | ||
Syntax | csetc 16725 | Extend class notation to include the category Set. |
Definition | df-setc 16726* | Definition of the category Set, relativized to a subset . Example 3.3(1) of [Adamek] p. 22. This is the category of all sets in and functions between these sets. Generally, we will take to be a weak universe or Grothendieck universe, because these sets have closure properties as good as the real thing. (Contributed by FL, 8-Nov-2013.) (Revised by Mario Carneiro, 3-Jan-2017.) |
comp | ||
Theorem | setcval 16727* | Value of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.) |
comp | ||
Theorem | setcbas 16728 | Set of objects of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.) |
Theorem | setchomfval 16729* | Set of arrows of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.) |
Theorem | setchom 16730 | Set of arrows of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.) |
Theorem | elsetchom 16731 | A morphism of sets is a function. (Contributed by Mario Carneiro, 3-Jan-2017.) |
Theorem | setccofval 16732* | Composition in the category of sets. (Contributed by Mario Carneiro, 3-Jan-2017.) |
comp | ||
Theorem | setcco 16733 | Composition in the category of sets. (Contributed by Mario Carneiro, 3-Jan-2017.) |
comp | ||
Theorem | setccatid 16734* | Lemma for setccat 16735. (Contributed by Mario Carneiro, 3-Jan-2017.) |
Theorem | setccat 16735 | The category of sets is a category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
Theorem | setcid 16736 | The identity arrow in the category of sets is the identity function. (Contributed by Mario Carneiro, 3-Jan-2017.) |
Theorem | setcmon 16737 | A monomorphism of sets is an injection. (Contributed by Mario Carneiro, 3-Jan-2017.) |
Mono | ||
Theorem | setcepi 16738 | An epimorphism of sets is a surjection. (Contributed by Mario Carneiro, 3-Jan-2017.) |
Epi | ||
Theorem | setcsect 16739 | A section in the category of sets, written out. (Contributed by Mario Carneiro, 3-Jan-2017.) |
Sect | ||
Theorem | setcinv 16740 | An inverse in the category of sets is the converse operation. (Contributed by Mario Carneiro, 3-Jan-2017.) |
Inv | ||
Theorem | setciso 16741 | An isomorphism in the category of sets is a bijection. (Contributed by Mario Carneiro, 3-Jan-2017.) |
Theorem | resssetc 16742 | The restriction of the category of sets to a subset is the category of sets in the subset. Thus, the categories for different are full subcategories of each other. (Contributed by Mario Carneiro, 6-Jan-2017.) |
f ↾s f compf ↾s compf | ||
Theorem | funcsetcres2 16743 | A functor into a smaller category of sets is a functor into the larger category. (Contributed by Mario Carneiro, 28-Jan-2017.) |
Syntax | ccatc 16744 | Extend class notation to include the category Cat. |
CatCat | ||
Definition | df-catc 16745* | 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. (Contributed by Mario Carneiro, 3-Jan-2017.) |
CatCat comp func | ||
Theorem | catcval 16746* | Value of the category of categories (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.) |
CatCat func comp | ||
Theorem | catcbas 16747 | Set of objects of the category of categories. (Contributed by Mario Carneiro, 3-Jan-2017.) |
CatCat | ||
Theorem | catchomfval 16748* | Set of arrows of the category of categories (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.) |
CatCat | ||
Theorem | catchom 16749 | Set of arrows of the category of categories (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.) |
CatCat | ||
Theorem | catccofval 16750* | Composition in the category of categories. (Contributed by Mario Carneiro, 3-Jan-2017.) |
CatCat comp func | ||
Theorem | catcco 16751 | Composition in the category of categories. (Contributed by Mario Carneiro, 3-Jan-2017.) |
CatCat comp func | ||
Theorem | catccatid 16752* | Lemma for catccat 16754. (Contributed by Mario Carneiro, 3-Jan-2017.) |
CatCat idfunc | ||
Theorem | catcid 16753 | The identity arrow in the category of categories is the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.) |
CatCat idfunc | ||
Theorem | catccat 16754 | 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" with respect to .) (Contributed by Mario Carneiro, 3-Jan-2017.) |
CatCat | ||
Theorem | resscatc 16755 | 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 f ↾s f compf ↾s compf | ||
Theorem | catcisolem 16756* | Lemma for catciso 16757. (Contributed by Mario Carneiro, 29-Jan-2017.) |
CatCat Inv Full Faith | ||
Theorem | catciso 16757 | 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 Full Faith | ||
Theorem | catcoppccl 16758 | The category of categories for a weak universe is closed under taking opposites. (Contributed by Mario Carneiro, 12-Jan-2017.) |
CatCat oppCat WUni | ||
Theorem | catcfuccl 16759 | The category of categories for a weak universe is closed under the functor category operation. (Contributed by Mario Carneiro, 12-Jan-2017.) |
CatCat 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 16763. 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 16765. 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 16761 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 16766, whereas the composition is the ordinary composition of functions, see estrccofval 16769 and estrcco 16770. It is shown that the category of extensible structures ExtStrCat is actually a category, see estrccat 16773 with the identity function as identity arrow, see estrcid 16774. 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): 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 41972 and dfringc2 42018, but with special compositions). With this definitions, however, theorem rngcresringcat 42030 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 , see df-setc 16726, 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 16763. The claimed equivalence is proven by equivestrcsetc 16792. 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 41959 and df-ringc 42005. In the same way, more subcategories could be provided, resulting in the following "inclusion chain" by proving theorems like rngcresringcat 42030, 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 into the chain, equivalent to ExtStrCat at the end." As mentioned before, the equivalence of and ExtStrCat is proven by equivestrcsetc 16792. Furthermore, it can be shown that is embedded into ExtStrCat, see embedsetcestrc 16807. Remark: equivestrcsetc 16792 as well as embedsetcestrc 16807 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 15878), but it would be currently sufficient to assume that , because the index value of the base set extractor is hard-coded as , see basendx 15923. 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) C_ Ob(B) and MorA(X,Y) C_ 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) C_ 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 is valid (see ringgrp 18552) 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 Struct Struct | ||
Theorem | fncnvimaeqv 16760 | The inverse images of the universal class under functions on the universal class are the universal class itself. (Proposed by Mario Carneiro, 7-Mar-2020.) (Contributed by AV, 7-Mar-2020.) |
Theorem | bascnvimaeqv 16761 | The inverse image of the universal class under the base function is the universal class itself. (Proposed by Mario Carneiro, 7-Mar-2020.) (Contributed by AV, 7-Mar-2020.) |
Syntax | cestrc 16762 | Extend class notation to include the category ExtStr. |
ExtStrCat | ||
Definition | df-estrc 16763* | 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 16761 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 comp | ||
Theorem | estrcval 16764* | Value of the category of extensible structures (in a universe). (Contributed by AV, 7-Mar-2020.) |
ExtStrCat comp | ||
Theorem | estrcbas 16765 | Set of objects of the category of extensible structures (in a universe). (Contributed by AV, 7-Mar-2020.) |
ExtStrCat | ||
Theorem | estrchomfval 16766* | Set of morphisms ("arrows") of the category of extensible structures (in a universe). (Contributed by AV, 7-Mar-2020.) |
ExtStrCat | ||
Theorem | estrchom 16767 | The morphisms between extensible structures are mappings between their base sets. (Contributed by AV, 7-Mar-2020.) |
ExtStrCat | ||
Theorem | elestrchom 16768 | A morphism between extensible structures is a function between their base sets. (Contributed by AV, 7-Mar-2020.) |
ExtStrCat | ||
Theorem | estrccofval 16769* | Composition in the category of extensible structures. (Contributed by AV, 7-Mar-2020.) |
ExtStrCat comp | ||
Theorem | estrcco 16770 | Composition in the category of extensible structures. (Contributed by AV, 7-Mar-2020.) |
ExtStrCat comp | ||
Theorem | estrcbasbas 16771 | 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 WUni | ||
Theorem | estrccatid 16772* | Lemma for estrccat 16773. (Contributed by AV, 8-Mar-2020.) |
ExtStrCat | ||
Theorem | estrccat 16773 | The category of extensible structures is a category. (Contributed by AV, 8-Mar-2020.) |
ExtStrCat | ||
Theorem | estrcid 16774 | The identity arrow in the category of extensible structures is the identity function of base sets. (Contributed by AV, 8-Mar-2020.) |
ExtStrCat | ||
Theorem | estrchomfn 16775 | The Hom-set operation in the category of extensible structures (in a universe) is a function. (Contributed by AV, 8-Mar-2020.) |
ExtStrCat | ||
Theorem | estrchomfeqhom 16776 | 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 f | ||
Theorem | estrreslem1 16777 | Lemma 1 for estrres 16779. (Contributed by AV, 14-Mar-2020.) |
comp | ||
Theorem | estrreslem2 16778 | Lemma 2 for estrres 16779. (Contributed by AV, 14-Mar-2020.) |
comp | ||
Theorem | estrres 16779 | 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.) |
comp ↾s sSet comp | ||
Theorem | funcestrcsetclem1 16780* | Lemma 1 for funcestrcsetc 16789. (Contributed by AV, 22-Mar-2020.) |
ExtStrCat WUni | ||
Theorem | funcestrcsetclem2 16781* | Lemma 2 for funcestrcsetc 16789. (Contributed by AV, 22-Mar-2020.) |
ExtStrCat WUni | ||
Theorem | funcestrcsetclem3 16782* | Lemma 3 for funcestrcsetc 16789. (Contributed by AV, 22-Mar-2020.) |
ExtStrCat WUni | ||
Theorem | funcestrcsetclem4 16783* | Lemma 4 for funcestrcsetc 16789. (Contributed by AV, 22-Mar-2020.) |
ExtStrCat WUni | ||
Theorem | funcestrcsetclem5 16784* | Lemma 5 for funcestrcsetc 16789. (Contributed by AV, 23-Mar-2020.) |
ExtStrCat WUni | ||
Theorem | funcestrcsetclem6 16785* | Lemma 6 for funcestrcsetc 16789. (Contributed by AV, 23-Mar-2020.) |
ExtStrCat WUni | ||
Theorem | funcestrcsetclem7 16786* | Lemma 7 for funcestrcsetc 16789. (Contributed by AV, 23-Mar-2020.) |
ExtStrCat WUni | ||
Theorem | funcestrcsetclem8 16787* | Lemma 8 for funcestrcsetc 16789. (Contributed by AV, 15-Feb-2020.) |
ExtStrCat WUni | ||
Theorem | funcestrcsetclem9 16788* | Lemma 9 for funcestrcsetc 16789. (Contributed by AV, 23-Mar-2020.) |
ExtStrCat WUni comp comp | ||
Theorem | funcestrcsetc 16789* | 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 WUni | ||
Theorem | fthestrcsetc 16790* | 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 WUni Faith | ||
Theorem | fullestrcsetc 16791* | 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 WUni Full | ||
Theorem | equivestrcsetc 16792* | 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 WUni Faith Full | ||
Theorem | setc1strwun 16793 | 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.) |
WUni | ||
Theorem | funcsetcestrclem1 16794* | Lemma 1 for funcsetcestrc 16804. (Contributed by AV, 27-Mar-2020.) |
Theorem | funcsetcestrclem2 16795* | Lemma 2 for funcsetcestrc 16804. (Contributed by AV, 27-Mar-2020.) |
WUni | ||
Theorem | funcsetcestrclem3 16796* | Lemma 3 for funcsetcestrc 16804. (Contributed by AV, 27-Mar-2020.) |
WUni ExtStrCat | ||
Theorem | embedsetcestrclem 16797* | Lemma for embedsetcestrc 16807. (Contributed by AV, 31-Mar-2020.) |
WUni ExtStrCat | ||
Theorem | funcsetcestrclem4 16798* | Lemma 4 for funcsetcestrc 16804. (Contributed by AV, 27-Mar-2020.) |
WUni | ||
Theorem | funcsetcestrclem5 16799* | Lemma 5 for funcsetcestrc 16804. (Contributed by AV, 27-Mar-2020.) |
WUni | ||
Theorem | funcsetcestrclem6 16800* | Lemma 6 for funcsetcestrc 16804. (Contributed by AV, 27-Mar-2020.) |
WUni |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |