Home | Metamath
Proof Explorer Theorem List (p. 461 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-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
The "category of unital rings" RingCat is the category of all (unital) rings Ring 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 46003. 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 46016. 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" π’) (π’ β© Ring), see ringcbas 46009, and the morphisms/arrows are the ring homomorphisms restricted to this subset of the rings ( RingHom βΎ (π΅ Γ π΅)), see ringchomfval 46010, whereas the composition is the ordinary composition of functions, see ringccofval 46014 and ringcco 46015. By showing that the ring homomorphisms between rings are a subcategory subset (βcat) of the mappings between base sets of extensible structures, see rhmsscmap 46018, it can be shown that the ring homomorphisms between rings are a subcategory (Subcat) of the category of extensible structures, see rhmsubcsetc 46021. It follows that the category of rings RingCat is actually a category, see ringccat 46022 with the identity function as identity arrow, see ringcid 46023. 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 46024, and that the ring homomorphisms between rings are a subcategory of the category of non-unital rings, see rhmsubcrngc 46027. 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 46028: ((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 46033. | ||
Syntax | cringc 46001 | Extend class notation to include the category Ring. |
class RingCat | ||
Syntax | cringcALTV 46002 | Extend class notation to include the category Ring. (New usage is discouraged.) |
class RingCatALTV | ||
Definition | df-ringc 46003 | 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 = (π’ β V β¦ ((ExtStrCatβπ’) βΎcat ( RingHom βΎ ((π’ β© Ring) Γ (π’ β© Ring))))) | ||
Definition | df-ringcALTV 46004* | 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 = (π’ β V β¦ β¦(π’ β© Ring) / πβ¦{β¨(Baseβndx), πβ©, β¨(Hom βndx), (π₯ β π, π¦ β π β¦ (π₯ RingHom π¦))β©, β¨(compβndx), (π£ β (π Γ π), π§ β π β¦ (π β ((2nd βπ£) RingHom π§), π β ((1st βπ£) RingHom (2nd βπ£)) β¦ (π β π)))β©}) | ||
Theorem | ringcvalALTV 46005* | Value of the category of rings (in a universe). (Contributed by AV, 13-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RingCatALTVβπ) & β’ (π β π β π) & β’ (π β π΅ = (π β© Ring)) & β’ (π β π» = (π₯ β π΅, π¦ β π΅ β¦ (π₯ RingHom π¦))) & β’ (π β Β· = (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) RingHom π§), π β ((1st βπ£) RingHom (2nd βπ£)) β¦ (π β π)))) β β’ (π β πΆ = {β¨(Baseβndx), π΅β©, β¨(Hom βndx), π»β©, β¨(compβndx), Β· β©}) | ||
Theorem | ringcval 46006 | Value of the category of unital rings (in a universe). (Contributed by AV, 13-Feb-2020.) (Revised by AV, 8-Mar-2020.) |
β’ πΆ = (RingCatβπ) & β’ (π β π β π) & β’ (π β π΅ = (π β© Ring)) & β’ (π β π» = ( RingHom βΎ (π΅ Γ π΅))) β β’ (π β πΆ = ((ExtStrCatβπ) βΎcat π»)) | ||
Theorem | rhmresfn 46007 | The class of unital ring homomorphisms restricted to subsets of unital rings is a function. (Contributed by AV, 10-Mar-2020.) |
β’ (π β π΅ = (π β© Ring)) & β’ (π β π» = ( RingHom βΎ (π΅ Γ π΅))) β β’ (π β π» Fn (π΅ Γ π΅)) | ||
Theorem | rhmresel 46008 | 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 46009 | 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βπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) β β’ (π β π΅ = (π β© Ring)) | ||
Theorem | ringchomfval 46010 | 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βπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ π» = (Hom βπΆ) β β’ (π β π» = ( RingHom βΎ (π΅ Γ π΅))) | ||
Theorem | ringchom 46011 | Set of arrows of the category of unital rings (in a universe). (Contributed by AV, 14-Feb-2020.) |
β’ πΆ = (RingCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ π» = (Hom βπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (ππ»π) = (π RingHom π)) | ||
Theorem | elringchom 46012 | A morphism of unital rings is a function. (Contributed by AV, 14-Feb-2020.) |
β’ πΆ = (RingCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ π» = (Hom βπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (πΉ β (ππ»π) β πΉ:(Baseβπ)βΆ(Baseβπ))) | ||
Theorem | ringchomfeqhom 46013 | 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βπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) β β’ (π β (Homf βπΆ) = (Hom βπΆ)) | ||
Theorem | ringccofval 46014 | Composition in the category of unital rings. (Contributed by AV, 14-Feb-2020.) (Revised by AV, 8-Mar-2020.) |
β’ πΆ = (RingCatβπ) & β’ (π β π β π) & β’ Β· = (compβπΆ) β β’ (π β Β· = (compβ(ExtStrCatβπ))) | ||
Theorem | ringcco 46015 | Composition in the category of unital rings. (Contributed by AV, 14-Feb-2020.) (Revised by AV, 8-Mar-2020.) |
β’ πΆ = (RingCatβπ) & β’ (π β π β π) & β’ Β· = (compβπΆ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β πΉ:(Baseβπ)βΆ(Baseβπ)) & β’ (π β πΊ:(Baseβπ)βΆ(Baseβπ)) β β’ (π β (πΊ(β¨π, πβ© Β· π)πΉ) = (πΊ β πΉ)) | ||
Theorem | dfringc2 46016 | Alternate definition of the category of unital rings (in a universe). (Contributed by AV, 16-Mar-2020.) |
β’ πΆ = (RingCatβπ) & β’ (π β π β π) & β’ (π β π΅ = (π β© Ring)) & β’ (π β π» = ( RingHom βΎ (π΅ Γ π΅))) & β’ (π β Β· = (compβ(ExtStrCatβπ))) β β’ (π β πΆ = {β¨(Baseβndx), π΅β©, β¨(Hom βndx), π»β©, β¨(compβndx), Β· β©}) | ||
Theorem | rhmsscmap2 46017* | 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.) |
β’ (π β π β π) & β’ (π β π = (Ring β© π)) β β’ (π β ( RingHom βΎ (π Γ π )) βcat (π₯ β π , π¦ β π β¦ ((Baseβπ¦) βm (Baseβπ₯)))) | ||
Theorem | rhmsscmap 46018* | 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.) |
β’ (π β π β π) & β’ (π β π = (Ring β© π)) β β’ (π β ( RingHom βΎ (π Γ π )) βcat (π₯ β π, π¦ β π β¦ ((Baseβπ¦) βm (Baseβπ₯)))) | ||
Theorem | rhmsubcsetclem1 46019 | Lemma 1 for rhmsubcsetc 46021. (Contributed by AV, 9-Mar-2020.) |
β’ πΆ = (ExtStrCatβπ) & β’ (π β π β π) & β’ (π β π΅ = (Ring β© π)) & β’ (π β π» = ( RingHom βΎ (π΅ Γ π΅))) β β’ ((π β§ π₯ β π΅) β ((IdβπΆ)βπ₯) β (π₯π»π₯)) | ||
Theorem | rhmsubcsetclem2 46020* | Lemma 2 for rhmsubcsetc 46021. (Contributed by AV, 9-Mar-2020.) |
β’ πΆ = (ExtStrCatβπ) & β’ (π β π β π) & β’ (π β π΅ = (Ring β© π)) & β’ (π β π» = ( RingHom βΎ (π΅ Γ π΅))) β β’ ((π β§ π₯ β π΅) β βπ¦ β π΅ βπ§ β π΅ βπ β (π₯π»π¦)βπ β (π¦π»π§)(π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯π»π§)) | ||
Theorem | rhmsubcsetc 46021 | 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βπ) & β’ (π β π β π) & β’ (π β π΅ = (Ring β© π)) & β’ (π β π» = ( RingHom βΎ (π΅ Γ π΅))) β β’ (π β π» β (SubcatβπΆ)) | ||
Theorem | ringccat 46022 | The category of unital rings is a category. (Contributed by AV, 14-Feb-2020.) (Revised by AV, 9-Mar-2020.) |
β’ πΆ = (RingCatβπ) β β’ (π β π β πΆ β Cat) | ||
Theorem | ringcid 46023 | 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βπ) & β’ π΅ = (BaseβπΆ) & β’ 1 = (IdβπΆ) & β’ (π β π β π) & β’ (π β π β π΅) & β’ π = (Baseβπ) β β’ (π β ( 1 βπ) = ( I βΎ π)) | ||
Theorem | rhmsscrnghm 46024 | 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.) |
β’ (π β π β π) & β’ (π β π = (Ring β© π)) & β’ (π β π = (Rng β© π)) β β’ (π β ( RingHom βΎ (π Γ π )) βcat ( RngHomo βΎ (π Γ π))) | ||
Theorem | rhmsubcrngclem1 46025 | Lemma 1 for rhmsubcrngc 46027. (Contributed by AV, 9-Mar-2020.) |
β’ πΆ = (RngCatβπ) & β’ (π β π β π) & β’ (π β π΅ = (Ring β© π)) & β’ (π β π» = ( RingHom βΎ (π΅ Γ π΅))) β β’ ((π β§ π₯ β π΅) β ((IdβπΆ)βπ₯) β (π₯π»π₯)) | ||
Theorem | rhmsubcrngclem2 46026* | Lemma 2 for rhmsubcrngc 46027. (Contributed by AV, 12-Mar-2020.) |
β’ πΆ = (RngCatβπ) & β’ (π β π β π) & β’ (π β π΅ = (Ring β© π)) & β’ (π β π» = ( RingHom βΎ (π΅ Γ π΅))) β β’ ((π β§ π₯ β π΅) β βπ¦ β π΅ βπ§ β π΅ βπ β (π₯π»π¦)βπ β (π¦π»π§)(π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯π»π§)) | ||
Theorem | rhmsubcrngc 46027 | 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βπ) & β’ (π β π β π) & β’ (π β π΅ = (Ring β© π)) & β’ (π β π» = ( RingHom βΎ (π΅ Γ π΅))) β β’ (π β π» β (SubcatβπΆ)) | ||
Theorem | rngcresringcat 46028 | 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βπ) & β’ (π β π β π) & β’ (π β π΅ = (Ring β© π)) & β’ (π β π» = ( RingHom βΎ (π΅ Γ π΅))) β β’ (π β (πΆ βΎcat π») = (RingCatβπ)) | ||
Theorem | ringcsect 46029 | A section in the category of unital rings, written out. (Contributed by AV, 14-Feb-2020.) |
β’ πΆ = (RingCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ πΈ = (Baseβπ) & β’ π = (SectβπΆ) β β’ (π β (πΉ(πππ)πΊ β (πΉ β (π RingHom π) β§ πΊ β (π RingHom π) β§ (πΊ β πΉ) = ( I βΎ πΈ)))) | ||
Theorem | ringcinv 46030 | An inverse in the category of unital rings is the converse operation. (Contributed by AV, 14-Feb-2020.) |
β’ πΆ = (RingCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ π = (InvβπΆ) β β’ (π β (πΉ(πππ)πΊ β (πΉ β (π RingIso π) β§ πΊ = β‘πΉ))) | ||
Theorem | ringciso 46031 | An isomorphism in the category of unital rings is a bijection. (Contributed by AV, 14-Feb-2020.) |
β’ πΆ = (RingCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ πΌ = (IsoβπΆ) β β’ (π β (πΉ β (ππΌπ) β πΉ β (π RingIso π))) | ||
Theorem | ringcbasbas 46032 | 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βπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β WUni) β β’ ((π β§ π β π΅) β (Baseβπ ) β π) | ||
Theorem | funcringcsetc 46033* | 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βπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ (π β πΉ(π Func π)πΊ) | ||
Theorem | funcringcsetcALTV2lem1 46034* | Lemma 1 for funcringcsetcALTV2 46043. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) β β’ ((π β§ π β π΅) β (πΉβπ) = (Baseβπ)) | ||
Theorem | funcringcsetcALTV2lem2 46035* | Lemma 2 for funcringcsetcALTV2 46043. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) β β’ ((π β§ π β π΅) β (πΉβπ) β π) | ||
Theorem | funcringcsetcALTV2lem3 46036* | Lemma 3 for funcringcsetcALTV2 46043. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) β β’ (π β πΉ:π΅βΆπΆ) | ||
Theorem | funcringcsetcALTV2lem4 46037* | Lemma 4 for funcringcsetcALTV2 46043. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ (π β πΊ Fn (π΅ Γ π΅)) | ||
Theorem | funcringcsetcALTV2lem5 46038* | Lemma 5 for funcringcsetcALTV2 46043. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΊπ) = ( I βΎ (π RingHom π))) | ||
Theorem | funcringcsetcALTV2lem6 46039* | Lemma 6 for funcringcsetcALTV2 46043. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ ((π β§ (π β π΅ β§ π β π΅) β§ π» β (π RingHom π)) β ((ππΊπ)βπ») = π») | ||
Theorem | funcringcsetcALTV2lem7 46040* | Lemma 7 for funcringcsetcALTV2 46043. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ ((π β§ π β π΅) β ((ππΊπ)β((Idβπ )βπ)) = ((Idβπ)β(πΉβπ))) | ||
Theorem | funcringcsetcALTV2lem8 46041* | Lemma 8 for funcringcsetcALTV2 46043. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΊπ):(π(Hom βπ )π)βΆ((πΉβπ)(Hom βπ)(πΉβπ))) | ||
Theorem | funcringcsetcALTV2lem9 46042* | Lemma 9 for funcringcsetcALTV2 46043. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ ((π β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π» β (π(Hom βπ )π) β§ πΎ β (π(Hom βπ )π))) β ((ππΊπ)β(πΎ(β¨π, πβ©(compβπ )π)π»)) = (((ππΊπ)βπΎ)(β¨(πΉβπ), (πΉβπ)β©(compβπ)(πΉβπ))((ππΊπ)βπ»))) | ||
Theorem | funcringcsetcALTV2 46043* | 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βπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ (π β πΉ(π Func π)πΊ) | ||
Theorem | ringcbasALTV 46044 | Set of objects of the category of rings (in a universe). (Contributed by AV, 13-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RingCatALTVβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) β β’ (π β π΅ = (π β© Ring)) | ||
Theorem | ringchomfvalALTV 46045* | Set of arrows of the category of rings (in a universe). (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RingCatALTVβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ π» = (Hom βπΆ) β β’ (π β π» = (π₯ β π΅, π¦ β π΅ β¦ (π₯ RingHom π¦))) | ||
Theorem | ringchomALTV 46046 | Set of arrows of the category of rings (in a universe). (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RingCatALTVβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ π» = (Hom βπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (ππ»π) = (π RingHom π)) | ||
Theorem | elringchomALTV 46047 | A morphism of rings is a function. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RingCatALTVβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ π» = (Hom βπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (πΉ β (ππ»π) β πΉ:(Baseβπ)βΆ(Baseβπ))) | ||
Theorem | ringccofvalALTV 46048* | Composition in the category of rings. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RingCatALTVβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ Β· = (compβπΆ) β β’ (π β Β· = (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) RingHom π§), π β ((1st βπ£) RingHom (2nd βπ£)) β¦ (π β π)))) | ||
Theorem | ringccoALTV 46049 | Composition in the category of rings. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RingCatALTVβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ Β· = (compβπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ β (π RingHom π)) & β’ (π β πΊ β (π RingHom π)) β β’ (π β (πΊ(β¨π, πβ© Β· π)πΉ) = (πΊ β πΉ)) | ||
Theorem | ringccatidALTV 46050* | Lemma for ringccatALTV 46051. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RingCatALTVβπ) & β’ π΅ = (BaseβπΆ) β β’ (π β π β (πΆ β Cat β§ (IdβπΆ) = (π₯ β π΅ β¦ ( I βΎ (Baseβπ₯))))) | ||
Theorem | ringccatALTV 46051 | The category of rings is a category. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RingCatALTVβπ) β β’ (π β π β πΆ β Cat) | ||
Theorem | ringcidALTV 46052 | The identity arrow in the category of rings is the identity function. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RingCatALTVβπ) & β’ π΅ = (BaseβπΆ) & β’ 1 = (IdβπΆ) & β’ (π β π β π) & β’ (π β π β π΅) & β’ π = (Baseβπ) β β’ (π β ( 1 βπ) = ( I βΎ π)) | ||
Theorem | ringcsectALTV 46053 | A section in the category of rings, written out. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RingCatALTVβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ πΈ = (Baseβπ) & β’ π = (SectβπΆ) β β’ (π β (πΉ(πππ)πΊ β (πΉ β (π RingHom π) β§ πΊ β (π RingHom π) β§ (πΊ β πΉ) = ( I βΎ πΈ)))) | ||
Theorem | ringcinvALTV 46054 | An inverse in the category of rings is the converse operation. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RingCatALTVβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ π = (InvβπΆ) β β’ (π β (πΉ(πππ)πΊ β (πΉ β (π RingIso π) β§ πΊ = β‘πΉ))) | ||
Theorem | ringcisoALTV 46055 | An isomorphism in the category of rings is a bijection. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RingCatALTVβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ πΌ = (IsoβπΆ) β β’ (π β (πΉ β (ππΌπ) β πΉ β (π RingIso π))) | ||
Theorem | ringcbasbasALTV 46056 | 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βπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β WUni) β β’ ((π β§ π β π΅) β (Baseβπ ) β π) | ||
Theorem | funcringcsetclem1ALTV 46057* | Lemma 1 for funcringcsetcALTV 46066. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatALTVβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) β β’ ((π β§ π β π΅) β (πΉβπ) = (Baseβπ)) | ||
Theorem | funcringcsetclem2ALTV 46058* | Lemma 2 for funcringcsetcALTV 46066. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatALTVβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) β β’ ((π β§ π β π΅) β (πΉβπ) β π) | ||
Theorem | funcringcsetclem3ALTV 46059* | Lemma 3 for funcringcsetcALTV 46066. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatALTVβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) β β’ (π β πΉ:π΅βΆπΆ) | ||
Theorem | funcringcsetclem4ALTV 46060* | Lemma 4 for funcringcsetcALTV 46066. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatALTVβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ (π β πΊ Fn (π΅ Γ π΅)) | ||
Theorem | funcringcsetclem5ALTV 46061* | Lemma 5 for funcringcsetcALTV 46066. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatALTVβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΊπ) = ( I βΎ (π RingHom π))) | ||
Theorem | funcringcsetclem6ALTV 46062* | Lemma 6 for funcringcsetcALTV 46066. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatALTVβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ ((π β§ (π β π΅ β§ π β π΅) β§ π» β (π RingHom π)) β ((ππΊπ)βπ») = π») | ||
Theorem | funcringcsetclem7ALTV 46063* | Lemma 7 for funcringcsetcALTV 46066. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatALTVβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ ((π β§ π β π΅) β ((ππΊπ)β((Idβπ )βπ)) = ((Idβπ)β(πΉβπ))) | ||
Theorem | funcringcsetclem8ALTV 46064* | Lemma 8 for funcringcsetcALTV 46066. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatALTVβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΊπ):(π(Hom βπ )π)βΆ((πΉβπ)(Hom βπ)(πΉβπ))) | ||
Theorem | funcringcsetclem9ALTV 46065* | Lemma 9 for funcringcsetcALTV 46066. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatALTVβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ ((π β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π» β (π(Hom βπ )π) β§ πΎ β (π(Hom βπ )π))) β ((ππΊπ)β(πΎ(β¨π, πβ©(compβπ )π)π»)) = (((ππΊπ)βπΎ)(β¨(πΉβπ), (πΉβπ)β©(compβπ)(πΉβπ))((ππΊπ)βπ»))) | ||
Theorem | funcringcsetcALTV 46066* | 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βπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ (π β πΉ(π Func π)πΊ) | ||
Theorem | irinitoringc 46067 | 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 46068 | The zero ring is a terminal object in the category of unital rings. (Contributed by AV, 17-Apr-2020.) |
β’ (π β π β π) & β’ πΆ = (RingCatβπ) & β’ (π β π β (Ring β NzRing)) & β’ (π β π β π) β β’ (π β π β (TermOβπΆ)) | ||
Theorem | zrninitoringc 46069* | 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βπ) & β’ (π β π β (Ring β NzRing)) & β’ (π β π β π) & β’ (π β βπ β (BaseβπΆ)π β NzRing) β β’ (π β π β (InitOβπΆ)) | ||
Theorem | nzerooringczr 46070 | 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βπ) & β’ (π β π β (Ring β NzRing)) & β’ (π β π β π) & β’ (π β β€ring β π) β β’ (π β (ZeroOβπΆ) = β ) | ||
Theorem | srhmsubclem1 46071* | Lemma 1 for srhmsubc 46074. (Contributed by AV, 19-Feb-2020.) |
β’ βπ β π π β Ring & β’ πΆ = (π β© π) β β’ (π β πΆ β π β (π β© Ring)) | ||
Theorem | srhmsubclem2 46072* | Lemma 2 for srhmsubc 46074. (Contributed by AV, 19-Feb-2020.) |
β’ βπ β π π β Ring & β’ πΆ = (π β© π) β β’ ((π β π β§ π β πΆ) β π β (Baseβ(RingCatβπ))) | ||
Theorem | srhmsubclem3 46073* | Lemma 3 for srhmsubc 46074. (Contributed by AV, 19-Feb-2020.) |
β’ βπ β π π β Ring & β’ πΆ = (π β© π) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ ((π β π β§ (π β πΆ β§ π β πΆ)) β (ππ½π) = (π(Hom β(RingCatβπ))π)) | ||
Theorem | srhmsubc 46074* | According to df-subc 17630, the subcategories (SubcatβπΆ) of a category πΆ are subsets of the homomorphisms of πΆ (see subcssc 17661 and subcss2 17664). 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.) |
β’ βπ β π π β Ring & β’ πΆ = (π β© π) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β π½ β (Subcatβ(RingCatβπ))) | ||
Theorem | sringcat 46075* | The restriction of the category of (unital) rings to the set of special ring homomorphisms is a category. (Contributed by AV, 19-Feb-2020.) |
β’ βπ β π π β Ring & β’ πΆ = (π β© π) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β ((RingCatβπ) βΎcat π½) β Cat) | ||
Theorem | crhmsubc 46076* | According to df-subc 17630, the subcategories (SubcatβπΆ) of a category πΆ are subsets of the homomorphisms of πΆ (see subcssc 17661 and subcss2 17664). 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.) |
β’ πΆ = (π β© CRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β π½ β (Subcatβ(RingCatβπ))) | ||
Theorem | cringcat 46077* | 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.) |
β’ πΆ = (π β© CRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β ((RingCatβπ) βΎcat π½) β Cat) | ||
Theorem | drhmsubc 46078* | According to df-subc 17630, the subcategories (SubcatβπΆ) of a category πΆ are subsets of the homomorphisms of πΆ (see subcssc 17661 and subcss2 17664). Therefore, the set of division ring homomorphisms is a "subcategory" of the category of (unital) rings. (Contributed by AV, 20-Feb-2020.) |
β’ πΆ = (π β© DivRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β π½ β (Subcatβ(RingCatβπ))) | ||
Theorem | drngcat 46079* | 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.) |
β’ πΆ = (π β© DivRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β ((RingCatβπ) βΎcat π½) β Cat) | ||
Theorem | fldcat 46080* | 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.) |
β’ πΆ = (π β© DivRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) & β’ π· = (π β© Field) & β’ πΉ = (π β π·, π β π· β¦ (π RingHom π )) β β’ (π β π β ((RingCatβπ) βΎcat πΉ) β Cat) | ||
Theorem | fldc 46081* | 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.) |
β’ πΆ = (π β© DivRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) & β’ π· = (π β© Field) & β’ πΉ = (π β π·, π β π· β¦ (π RingHom π )) β β’ (π β π β (((RingCatβπ) βΎcat π½) βΎcat πΉ) β Cat) | ||
Theorem | fldhmsubc 46082* | According to df-subc 17630, the subcategories (SubcatβπΆ) of a category πΆ are subsets of the homomorphisms of πΆ (see subcssc 17661 and subcss2 17664). Therefore, the set of field homomorphisms is a "subcategory" of the category of division rings. (Contributed by AV, 20-Feb-2020.) |
β’ πΆ = (π β© DivRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) & β’ π· = (π β© Field) & β’ πΉ = (π β π·, π β π· β¦ (π RingHom π )) β β’ (π β π β πΉ β (Subcatβ((RingCatβπ) βΎcat π½))) | ||
Theorem | rngcrescrhm 46083 | 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βπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ (π β (πΆ βΎcat π») = ((πΆ βΎs π ) sSet β¨(Hom βndx), π»β©)) | ||
Theorem | rhmsubclem1 46084 | Lemma 1 for rhmsubc 46088. (Contributed by AV, 2-Mar-2020.) |
β’ (π β π β π) & β’ πΆ = (RngCatβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ (π β π» Fn (π Γ π )) | ||
Theorem | rhmsubclem2 46085 | Lemma 2 for rhmsubc 46088. (Contributed by AV, 2-Mar-2020.) |
β’ (π β π β π) & β’ πΆ = (RngCatβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ ((π β§ π β π β§ π β π ) β (ππ»π) = (π RingHom π)) | ||
Theorem | rhmsubclem3 46086* | Lemma 3 for rhmsubc 46088. (Contributed by AV, 2-Mar-2020.) |
β’ (π β π β π) & β’ πΆ = (RngCatβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ ((π β§ π₯ β π ) β ((Idβ(RngCatβπ))βπ₯) β (π₯π»π₯)) | ||
Theorem | rhmsubclem4 46087* | Lemma 4 for rhmsubc 46088. (Contributed by AV, 2-Mar-2020.) |
β’ (π β π β π) & β’ πΆ = (RngCatβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ ((((π β§ π₯ β π ) β§ (π¦ β π β§ π§ β π )) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β (π(β¨π₯, π¦β©(compβ(RngCatβπ))π§)π) β (π₯π»π§)) | ||
Theorem | rhmsubc 46088 | According to df-subc 17630, the subcategories (SubcatβπΆ) of a category πΆ are subsets of the homomorphisms of πΆ (see subcssc 17661 and subcss2 17664). Therefore, the set of unital ring homomorphisms is a "subcategory" of the category of non-unital rings. (Contributed by AV, 2-Mar-2020.) |
β’ (π β π β π) & β’ πΆ = (RngCatβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ (π β π» β (Subcatβ(RngCatβπ))) | ||
Theorem | rhmsubccat 46089 | 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βπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ (π β ((RngCatβπ) βΎcat π») β Cat) | ||
Theorem | srhmsubcALTVlem1 46090* | Lemma 1 for srhmsubcALTV 46092. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.) |
β’ βπ β π π β Ring & β’ πΆ = (π β© π) β β’ ((π β π β§ π β πΆ) β π β (Baseβ(RingCatALTVβπ))) | ||
Theorem | srhmsubcALTVlem2 46091* | Lemma 2 for srhmsubcALTV 46092. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.) |
β’ βπ β π π β Ring & β’ πΆ = (π β© π) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ ((π β π β§ (π β πΆ β§ π β πΆ)) β (ππ½π) = (π(Hom β(RingCatALTVβπ))π)) | ||
Theorem | srhmsubcALTV 46092* | According to df-subc 17630, the subcategories (SubcatβπΆ) of a category πΆ are subsets of the homomorphisms of πΆ (see subcssc 17661 and subcss2 17664). 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.) |
β’ βπ β π π β Ring & β’ πΆ = (π β© π) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β π½ β (Subcatβ(RingCatALTVβπ))) | ||
Theorem | sringcatALTV 46093* | 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.) |
β’ βπ β π π β Ring & β’ πΆ = (π β© π) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β ((RingCatALTVβπ) βΎcat π½) β Cat) | ||
Theorem | crhmsubcALTV 46094* | According to df-subc 17630, the subcategories (SubcatβπΆ) of a category πΆ are subsets of the homomorphisms of πΆ (see subcssc 17661 and subcss2 17664). 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.) |
β’ πΆ = (π β© CRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β π½ β (Subcatβ(RingCatALTVβπ))) | ||
Theorem | cringcatALTV 46095* | 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.) |
β’ πΆ = (π β© CRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β ((RingCatALTVβπ) βΎcat π½) β Cat) | ||
Theorem | drhmsubcALTV 46096* | According to df-subc 17630, the subcategories (SubcatβπΆ) of a category πΆ are subsets of the homomorphisms of πΆ (see subcssc 17661 and subcss2 17664). 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.) |
β’ πΆ = (π β© DivRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β π½ β (Subcatβ(RingCatALTVβπ))) | ||
Theorem | drngcatALTV 46097* | 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.) |
β’ πΆ = (π β© DivRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β ((RingCatALTVβπ) βΎcat π½) β Cat) | ||
Theorem | fldcatALTV 46098* | 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.) |
β’ πΆ = (π β© DivRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) & β’ π· = (π β© Field) & β’ πΉ = (π β π·, π β π· β¦ (π RingHom π )) β β’ (π β π β ((RingCatALTVβπ) βΎcat πΉ) β Cat) | ||
Theorem | fldcALTV 46099* | 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.) (New usage is discouraged.) |
β’ πΆ = (π β© DivRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) & β’ π· = (π β© Field) & β’ πΉ = (π β π·, π β π· β¦ (π RingHom π )) β β’ (π β π β (((RingCatALTVβπ) βΎcat π½) βΎcat πΉ) β Cat) | ||
Theorem | fldhmsubcALTV 46100* | According to df-subc 17630, the subcategories (SubcatβπΆ) of a category πΆ are subsets of the homomorphisms of πΆ (see subcssc 17661 and subcss2 17664). Therefore, the set of field homomorphisms is a "subcategory" of the category of division rings. (Contributed by AV, 20-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (π β© DivRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) & β’ π· = (π β© Field) & β’ πΉ = (π β π·, π β π· β¦ (π RingHom π )) β β’ (π β π β πΉ β (Subcatβ((RingCatALTVβπ) βΎcat π½))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |