Home | Metamath
Proof Explorer Theorem List (p. 421 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 | zrtermorngc 42001 | The zero ring is a terminal object in the category of nonunital rings. (Contributed by AV, 17-Apr-2020.) |
RngCat NzRing TermO | ||
Theorem | zrzeroorngc 42002 | The zero ring is a zero object in the category of non-unital rings. (Contributed by AV, 18-Apr-2020.) |
RngCat NzRing ZeroO | ||
The "category of unital rings" RingCat is the category of all (unital) rings in a universe and (unital) ring homomorphisms RingHom between these rings. This category is defined as "category restriction" of the category of extensible structures ExtStrCat, which restricts the objects to (unital) rings and the morphisms to the (unital) ring homomorphisms, while the composition of morphisms is preserved, see df-ringc 42005. Alternately, the category of unital rings could have been defined as extensible structure consisting of three components/slots for the objects, morphisms and composition, see dfringc2 42018. In the following, we omit the predicate "unital", so that "ring" and "ring homomorphism" (without predicate) always mean "unital ring" and "unital ring homomorphism". 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 a subset of the rings (relativized to a subset or "universe" ) , see ringcbas 42011, and the morphisms/arrows are the ring homomorphisms restricted to this subset of the rings RingHom , see ringchomfval 42012, whereas the composition is the ordinary composition of functions, see ringccofval 42016 and ringcco 42017. By showing that the ring homomorphisms between rings are a subcategory subset (cat) of the mappings between base sets of extensible structures, see rhmsscmap 42020, it can be shown that the ring homomorphisms between rings are a subcategory (Subcat) of the category of extensible structures, see rhmsubcsetc 42023. It follows that the category of rings RingCat is actually a category, see ringccat 42024 with the identity function as identity arrow, see ringcid 42025. Furthermore, it is shown that the ring homomorphisms between rings are a subcategory subset of the non-unital ring homomorphisms between non-unital rings, see rhmsscrnghm 42026, and that the ring homomorphisms between rings are a subcategory of the category of non-unital rings, see rhmsubcrngc 42029. By this, the restriction of the category of non-unital rings to the set of unital ring homomorphisms is the category of unital rings, see rngcresringcat 42030: RngCat cat RingHom RingCat. Finally, it is shown that the "natural forgetful functor" from the category of rings into the category of sets is the function which sends each ring to its underlying set (base set) and the morphisms (ring homomorphisms) to mappings of the corresponding base sets, see funcringcsetc 42035. | ||
Syntax | cringc 42003 | Extend class notation to include the category Ring. |
RingCat | ||
Syntax | cringcALTV 42004 | Extend class notation to include the category Ring. (New usage is discouraged.) |
RingCatALTV | ||
Definition | df-ringc 42005 | Definition of the category Ring, relativized to a subset . See also the note in [Lang] p. 91, and the item Rng in [Adamek] p. 478. This is the category of all unital rings in and homomorphisms between these rings. 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 AV, 13-Feb-2020.) (Revised by AV, 8-Mar-2020.) |
RingCat ExtStrCat cat RingHom | ||
Definition | df-ringcALTV 42006* | Definition of the category Ring, relativized to a subset . This is the category of all rings in and homomorphisms between these rings. 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 AV, 13-Feb-2020.) (New usage is discouraged.) |
RingCatALTV RingHom comp RingHom RingHom | ||
Theorem | ringcvalALTV 42007* | Value of the category of rings (in a universe). (Contributed by AV, 13-Feb-2020.) (New usage is discouraged.) |
RingCatALTV RingHom RingHom RingHom comp | ||
Theorem | ringcval 42008 | Value of the category of unital rings (in a universe). (Contributed by AV, 13-Feb-2020.) (Revised by AV, 8-Mar-2020.) |
RingCat RingHom ExtStrCat cat | ||
Theorem | rhmresfn 42009 | The class of unital ring homomorphisms restricted to subsets of unital rings is a function. (Contributed by AV, 10-Mar-2020.) |
RingHom | ||
Theorem | rhmresel 42010 | An element of the unital ring homomorphisms restricted to a subset of unital rings is a unital ring homomorphism. (Contributed by AV, 10-Mar-2020.) |
RingHom RingHom | ||
Theorem | ringcbas 42011 | Set of objects of the category of unital rings (in a universe). (Contributed by AV, 13-Feb-2020.) (Revised by AV, 8-Mar-2020.) |
RingCat | ||
Theorem | ringchomfval 42012 | Set of arrows of the category of unital rings (in a universe). (Contributed by AV, 14-Feb-2020.) (Revised by AV, 8-Mar-2020.) |
RingCat RingHom | ||
Theorem | ringchom 42013 | Set of arrows of the category of unital rings (in a universe). (Contributed by AV, 14-Feb-2020.) |
RingCat RingHom | ||
Theorem | elringchom 42014 | A morphism of unital rings is a function. (Contributed by AV, 14-Feb-2020.) |
RingCat | ||
Theorem | ringchomfeqhom 42015 | The functionalized Hom-set operation equals the Hom-set operation in the category of unital rings (in a universe). (Contributed by AV, 9-Mar-2020.) |
RingCat f | ||
Theorem | ringccofval 42016 | Composition in the category of unital rings. (Contributed by AV, 14-Feb-2020.) (Revised by AV, 8-Mar-2020.) |
RingCat comp compExtStrCat | ||
Theorem | ringcco 42017 | Composition in the category of unital rings. (Contributed by AV, 14-Feb-2020.) (Revised by AV, 8-Mar-2020.) |
RingCat comp | ||
Theorem | dfringc2 42018 | Alternate definition of the category of unital rings (in a universe). (Contributed by AV, 16-Mar-2020.) |
RingCat RingHom compExtStrCat comp | ||
Theorem | rhmsscmap2 42019* | The unital ring homomorphisms between unital rings (in a universe) are a subcategory subset of the mappings between base sets of unital rings (in the same universe). (Contributed by AV, 6-Mar-2020.) |
RingHom cat | ||
Theorem | rhmsscmap 42020* | The unital ring homomorphisms between unital rings (in a universe) are a subcategory subset of the mappings between base sets of extensible structures (in the same universe). (Contributed by AV, 9-Mar-2020.) |
RingHom cat | ||
Theorem | rhmsubcsetclem1 42021 | Lemma 1 for rhmsubcsetc 42023. (Contributed by AV, 9-Mar-2020.) |
ExtStrCat RingHom | ||
Theorem | rhmsubcsetclem2 42022* | Lemma 2 for rhmsubcsetc 42023. (Contributed by AV, 9-Mar-2020.) |
ExtStrCat RingHom comp | ||
Theorem | rhmsubcsetc 42023 | The unital ring homomorphisms between unital rings (in a universe) are a subcategory of the category of extensible structures. (Contributed by AV, 9-Mar-2020.) |
ExtStrCat RingHom Subcat | ||
Theorem | ringccat 42024 | The category of unital rings is a category. (Contributed by AV, 14-Feb-2020.) (Revised by AV, 9-Mar-2020.) |
RingCat | ||
Theorem | ringcid 42025 | The identity arrow in the category of unital rings is the identity function. (Contributed by AV, 14-Feb-2020.) (Revised by AV, 10-Mar-2020.) |
RingCat | ||
Theorem | rhmsscrnghm 42026 | The unital ring homomorphisms between unital rings (in a universe) are a subcategory subset of the non-unital ring homomorphisms between non-unital rings (in the same universe). (Contributed by AV, 1-Mar-2020.) |
Rng RingHom cat RngHomo | ||
Theorem | rhmsubcrngclem1 42027 | Lemma 1 for rhmsubcrngc 42029. (Contributed by AV, 9-Mar-2020.) |
RngCat RingHom | ||
Theorem | rhmsubcrngclem2 42028* | Lemma 2 for rhmsubcrngc 42029. (Contributed by AV, 12-Mar-2020.) |
RngCat RingHom comp | ||
Theorem | rhmsubcrngc 42029 | The unital ring homomorphisms between unital rings (in a universe) are a subcategory of the category of non-unital rings. (Contributed by AV, 12-Mar-2020.) |
RngCat RingHom Subcat | ||
Theorem | rngcresringcat 42030 | The restriction of the category of non-unital rings to the set of unital ring homomorphisms is the category of unital rings. (Contributed by AV, 16-Mar-2020.) |
RngCat RingHom cat RingCat | ||
Theorem | ringcsect 42031 | A section in the category of unital rings, written out. (Contributed by AV, 14-Feb-2020.) |
RingCat Sect RingHom RingHom | ||
Theorem | ringcinv 42032 | An inverse in the category of unital rings is the converse operation. (Contributed by AV, 14-Feb-2020.) |
RingCat Inv RingIso | ||
Theorem | ringciso 42033 | An isomorphism in the category of unital rings is a bijection. (Contributed by AV, 14-Feb-2020.) |
RingCat RingIso | ||
Theorem | ringcbasbas 42034 | An element of the base set of the base set of the category of unital rings (i.e. the base set of a ring) belongs to the considered weak universe. (Contributed by AV, 15-Feb-2020.) |
RingCat WUni | ||
Theorem | funcringcsetc 42035* | The "natural forgetful functor" from the category of unital rings into the category of sets which sends each ring to its underlying set (base set) and the morphisms (ring homomorphisms) to mappings of the corresponding base sets. (Contributed by AV, 26-Mar-2020.) |
RingCat WUni RingHom | ||
Theorem | funcringcsetcALTV2lem1 42036* | Lemma 1 for funcringcsetcALTV2 42045. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
RingCat WUni | ||
Theorem | funcringcsetcALTV2lem2 42037* | Lemma 2 for funcringcsetcALTV2 42045. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
RingCat WUni | ||
Theorem | funcringcsetcALTV2lem3 42038* | Lemma 3 for funcringcsetcALTV2 42045. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
RingCat WUni | ||
Theorem | funcringcsetcALTV2lem4 42039* | Lemma 4 for funcringcsetcALTV2 42045. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
RingCat WUni RingHom | ||
Theorem | funcringcsetcALTV2lem5 42040* | Lemma 5 for funcringcsetcALTV2 42045. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
RingCat WUni RingHom RingHom | ||
Theorem | funcringcsetcALTV2lem6 42041* | Lemma 6 for funcringcsetcALTV2 42045. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
RingCat WUni RingHom RingHom | ||
Theorem | funcringcsetcALTV2lem7 42042* | Lemma 7 for funcringcsetcALTV2 42045. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
RingCat WUni RingHom | ||
Theorem | funcringcsetcALTV2lem8 42043* | Lemma 8 for funcringcsetcALTV2 42045. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
RingCat WUni RingHom | ||
Theorem | funcringcsetcALTV2lem9 42044* | Lemma 9 for funcringcsetcALTV2 42045. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
RingCat WUni RingHom comp comp | ||
Theorem | funcringcsetcALTV2 42045* | The "natural forgetful functor" from the category of unital rings into the category of sets which sends each ring to its underlying set (base set) and the morphisms (ring homomorphisms) to mappings of the corresponding base sets. (Contributed by AV, 16-Feb-2020.) (New usage is discouraged.) |
RingCat WUni RingHom | ||
Theorem | ringcbasALTV 42046 | Set of objects of the category of rings (in a universe). (Contributed by AV, 13-Feb-2020.) (New usage is discouraged.) |
RingCatALTV | ||
Theorem | ringchomfvalALTV 42047* | Set of arrows of the category of rings (in a universe). (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
RingCatALTV RingHom | ||
Theorem | ringchomALTV 42048 | Set of arrows of the category of rings (in a universe). (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
RingCatALTV RingHom | ||
Theorem | elringchomALTV 42049 | A morphism of rings is a function. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
RingCatALTV | ||
Theorem | ringccofvalALTV 42050* | Composition in the category of rings. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
RingCatALTV comp RingHom RingHom | ||
Theorem | ringccoALTV 42051 | Composition in the category of rings. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
RingCatALTV comp RingHom RingHom | ||
Theorem | ringccatidALTV 42052* | Lemma for ringccatALTV 42053. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
RingCatALTV | ||
Theorem | ringccatALTV 42053 | The category of rings is a category. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
RingCatALTV | ||
Theorem | ringcidALTV 42054 | The identity arrow in the category of rings is the identity function. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
RingCatALTV | ||
Theorem | ringcsectALTV 42055 | A section in the category of rings, written out. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
RingCatALTV Sect RingHom RingHom | ||
Theorem | ringcinvALTV 42056 | An inverse in the category of rings is the converse operation. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
RingCatALTV Inv RingIso | ||
Theorem | ringcisoALTV 42057 | An isomorphism in the category of rings is a bijection. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
RingCatALTV RingIso | ||
Theorem | ringcbasbasALTV 42058 | An element of the base set of the base set of the category of rings (i.e. the base set of a ring) belongs to the considered weak universe. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
RingCatALTV WUni | ||
Theorem | funcringcsetclem1ALTV 42059* | Lemma 1 for funcringcsetcALTV 42068. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
RingCatALTV WUni | ||
Theorem | funcringcsetclem2ALTV 42060* | Lemma 2 for funcringcsetcALTV 42068. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
RingCatALTV WUni | ||
Theorem | funcringcsetclem3ALTV 42061* | Lemma 3 for funcringcsetcALTV 42068. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
RingCatALTV WUni | ||
Theorem | funcringcsetclem4ALTV 42062* | Lemma 4 for funcringcsetcALTV 42068. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
RingCatALTV WUni RingHom | ||
Theorem | funcringcsetclem5ALTV 42063* | Lemma 5 for funcringcsetcALTV 42068. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
RingCatALTV WUni RingHom RingHom | ||
Theorem | funcringcsetclem6ALTV 42064* | Lemma 6 for funcringcsetcALTV 42068. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
RingCatALTV WUni RingHom RingHom | ||
Theorem | funcringcsetclem7ALTV 42065* | Lemma 7 for funcringcsetcALTV 42068. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
RingCatALTV WUni RingHom | ||
Theorem | funcringcsetclem8ALTV 42066* | Lemma 8 for funcringcsetcALTV 42068. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
RingCatALTV WUni RingHom | ||
Theorem | funcringcsetclem9ALTV 42067* | Lemma 9 for funcringcsetcALTV 42068. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
RingCatALTV WUni RingHom comp comp | ||
Theorem | funcringcsetcALTV 42068* | The "natural forgetful functor" from the category of rings into the category of sets which sends each ring to its underlying set (base set) and the morphisms (ring homomorphisms) to mappings of the corresponding base sets. (Contributed by AV, 16-Feb-2020.) (New usage is discouraged.) |
RingCatALTV WUni RingHom | ||
Theorem | irinitoringc 42069 | The ring of integers is an initial object in the category of unital rings (within a universe containing the ring of integers). Example 7.2 (6) of [Adamek] p. 101 , and example in [Lang] p. 58. (Contributed by AV, 3-Apr-2020.) |
ℤring RingCat ℤring InitO | ||
Theorem | zrtermoringc 42070 | The zero ring is a terminal object in the category of unital rings. (Contributed by AV, 17-Apr-2020.) |
RingCat NzRing TermO | ||
Theorem | zrninitoringc 42071* | The zero ring is not an initial object in the category of unital rings (if the universe contains at least one unital ring different from the zero ring). (Contributed by AV, 18-Apr-2020.) |
RingCat NzRing NzRing InitO | ||
Theorem | nzerooringczr 42072 | There is no zero object in the category of unital rings (at least in a universe which contains the zero ring and the ring of integers). Example 7.9 (3) in [Adamek] p. 103. (Contributed by AV, 18-Apr-2020.) |
RingCat NzRing ℤring ZeroO | ||
Theorem | srhmsubclem1 42073* | Lemma 1 for srhmsubc 42076. (Contributed by AV, 19-Feb-2020.) |
Theorem | srhmsubclem2 42074* | Lemma 2 for srhmsubc 42076. (Contributed by AV, 19-Feb-2020.) |
RingCat | ||
Theorem | srhmsubclem3 42075* | Lemma 3 for srhmsubc 42076. (Contributed by AV, 19-Feb-2020.) |
RingHom RingCat | ||
Theorem | srhmsubc 42076* | According to df-subc 16472, the subcategories Subcat of a category are subsets of the homomorphisms of ( see subcssc 16500 and subcss2 16503). Therefore, the set of special ring homomorphisms (i.e. ring homomorphisms from a special ring to another ring of that kind) is a "subcategory" of the category of (unital) rings. (Contributed by AV, 19-Feb-2020.) |
RingHom SubcatRingCat | ||
Theorem | sringcat 42077* | The restriction of the category of (unital) rings to the set of special ring homomorphisms is a category. (Contributed by AV, 19-Feb-2020.) |
RingHom RingCat cat | ||
Theorem | crhmsubc 42078* | According to df-subc 16472, the subcategories Subcat of a category are subsets of the homomorphisms of ( see subcssc 16500 and subcss2 16503). Therefore, the set of commutative ring homomorphisms (i.e. ring homomorphisms from a commutative ring to a commutative ring) is a "subcategory" of the category of (unital) rings. (Contributed by AV, 19-Feb-2020.) |
RingHom SubcatRingCat | ||
Theorem | cringcat 42079* | The restriction of the category of (unital) rings to the set of commutative ring homomorphisms is a category, the "category of commutative rings". (Contributed by AV, 19-Feb-2020.) |
RingHom RingCat cat | ||
Theorem | drhmsubc 42080* | According to df-subc 16472, the subcategories Subcat of a category are subsets of the homomorphisms of ( see subcssc 16500 and subcss2 16503). Therefore, the set of division ring homomorphisms is a "subcategory" of the category of (unital) rings. (Contributed by AV, 20-Feb-2020.) |
RingHom SubcatRingCat | ||
Theorem | drngcat 42081* | The restriction of the category of (unital) rings to the set of division ring homomorphisms is a category, the "category of division rings". (Contributed by AV, 20-Feb-2020.) |
RingHom RingCat cat | ||
Theorem | fldcat 42082* | The restriction of the category of (unital) rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020.) |
RingHom Field RingHom RingCat cat | ||
Theorem | fldc 42083* | The restriction of the category of division rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020.) |
RingHom Field RingHom RingCat cat cat | ||
Theorem | fldhmsubc 42084* | According to df-subc 16472, the subcategories Subcat of a category are subsets of the homomorphisms of ( see subcssc 16500 and subcss2 16503). Therefore, the set of field homomorphisms is a "subcategory" of the category of division rings. (Contributed by AV, 20-Feb-2020.) |
RingHom Field RingHom SubcatRingCat cat | ||
Theorem | rngcrescrhm 42085 | The category of non-unital rings (in a universe) restricted to the ring homomorphisms between unital rings (in the same universe). (Contributed by AV, 1-Mar-2020.) |
RngCat RingHom cat ↾s sSet | ||
Theorem | rhmsubclem1 42086 | Lemma 1 for rhmsubc 42090. (Contributed by AV, 2-Mar-2020.) |
RngCat RingHom | ||
Theorem | rhmsubclem2 42087 | Lemma 2 for rhmsubc 42090. (Contributed by AV, 2-Mar-2020.) |
RngCat RingHom RingHom | ||
Theorem | rhmsubclem3 42088* | Lemma 3 for rhmsubc 42090. (Contributed by AV, 2-Mar-2020.) |
RngCat RingHom RngCat | ||
Theorem | rhmsubclem4 42089* | Lemma 4 for rhmsubc 42090. (Contributed by AV, 2-Mar-2020.) |
RngCat RingHom compRngCat | ||
Theorem | rhmsubc 42090 | According to df-subc 16472, the subcategories Subcat of a category are subsets of the homomorphisms of ( see subcssc 16500 and subcss2 16503). Therefore, the set of unital ring homomorphisms is a "subcategory" of the category of non-unital rings. (Contributed by AV, 2-Mar-2020.) |
RngCat RingHom SubcatRngCat | ||
Theorem | rhmsubccat 42091 | The restriction of the category of non-unital rings to the set of unital ring homomorphisms is a category. (Contributed by AV, 4-Mar-2020.) |
RngCat RingHom RngCat cat | ||
Theorem | srhmsubcALTVlem1 42092* | Lemma 1 for srhmsubcALTV 42094. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.) |
RingCatALTV | ||
Theorem | srhmsubcALTVlem2 42093* | Lemma 2 for srhmsubcALTV 42094. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.) |
RingHom RingCatALTV | ||
Theorem | srhmsubcALTV 42094* | According to df-subc 16472, the subcategories Subcat of a category are subsets of the homomorphisms of ( see subcssc 16500 and subcss2 16503). Therefore, the set of special ring homomorphisms (i.e. ring homomorphisms from a special ring to another ring of that kind) is a "subcategory" of the category of (unital) rings. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.) |
RingHom SubcatRingCatALTV | ||
Theorem | sringcatALTV 42095* | The restriction of the category of (unital) rings to the set of special ring homomorphisms is a category. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.) |
RingHom RingCatALTV cat | ||
Theorem | crhmsubcALTV 42096* | According to df-subc 16472, the subcategories Subcat of a category are subsets of the homomorphisms of ( see subcssc 16500 and subcss2 16503). Therefore, the set of commutative ring homomorphisms (i.e. ring homomorphisms from a commutative ring to a commutative ring) is a "subcategory" of the category of (unital) rings. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.) |
RingHom SubcatRingCatALTV | ||
Theorem | cringcatALTV 42097* | The restriction of the category of (unital) rings to the set of commutative ring homomorphisms is a category, the "category of commutative rings". (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.) |
RingHom RingCatALTV cat | ||
Theorem | drhmsubcALTV 42098* | According to df-subc 16472, the subcategories Subcat of a category are subsets of the homomorphisms of ( see subcssc 16500 and subcss2 16503). Therefore, the set of division ring homomorphisms is a "subcategory" of the category of (unital) rings. (Contributed by AV, 20-Feb-2020.) (New usage is discouraged.) |
RingHom SubcatRingCatALTV | ||
Theorem | drngcatALTV 42099* | The restriction of the category of (unital) rings to the set of division ring homomorphisms is a category, the "category of division rings". (Contributed by AV, 20-Feb-2020.) (New usage is discouraged.) |
RingHom RingCatALTV cat | ||
Theorem | fldcatALTV 42100* | The restriction of the category of (unital) rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020.) (New usage is discouraged.) |
RingHom Field RingHom RingCatALTV cat |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |