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-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rngchomALTV 46001 | Set of arrows of the category of non-unital rings (in a universe). (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.) |
β’ πΆ = (RngCatALTVβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ π» = (Hom βπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (ππ»π) = (π RngHomo π)) | ||
Theorem | elrngchomALTV 46002 | A morphism of non-unital rings is a function. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.) |
β’ πΆ = (RngCatALTVβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ π» = (Hom βπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (πΉ β (ππ»π) β πΉ:(Baseβπ)βΆ(Baseβπ))) | ||
Theorem | rngccofvalALTV 46003* | Composition in the category of non-unital rings. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.) |
β’ πΆ = (RngCatALTVβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ Β· = (compβπΆ) β β’ (π β Β· = (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) RngHomo π§), π β ((1st βπ£) RngHomo (2nd βπ£)) β¦ (π β π)))) | ||
Theorem | rngccoALTV 46004 | Composition in the category of non-unital rings. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.) |
β’ πΆ = (RngCatALTVβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ Β· = (compβπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ β (π RngHomo π)) & β’ (π β πΊ β (π RngHomo π)) β β’ (π β (πΊ(β¨π, πβ© Β· π)πΉ) = (πΊ β πΉ)) | ||
Theorem | rngccatidALTV 46005* | Lemma for rngccatALTV 46006. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.) |
β’ πΆ = (RngCatALTVβπ) & β’ π΅ = (BaseβπΆ) β β’ (π β π β (πΆ β Cat β§ (IdβπΆ) = (π₯ β π΅ β¦ ( I βΎ (Baseβπ₯))))) | ||
Theorem | rngccatALTV 46006 | The category of non-unital rings is a category. (Contributed by AV, 27-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RngCatALTVβπ) β β’ (π β π β πΆ β Cat) | ||
Theorem | rngcidALTV 46007 | The identity arrow in the category of non-unital rings is the identity function. (Contributed by AV, 27-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RngCatALTVβπ) & β’ π΅ = (BaseβπΆ) & β’ 1 = (IdβπΆ) & β’ (π β π β π) & β’ (π β π β π΅) & β’ π = (Baseβπ) β β’ (π β ( 1 βπ) = ( I βΎ π)) | ||
Theorem | rngcsectALTV 46008 | A section in the category of non-unital rings, written out. (Contributed by AV, 28-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RngCatALTVβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ πΈ = (Baseβπ) & β’ π = (SectβπΆ) β β’ (π β (πΉ(πππ)πΊ β (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π) β§ (πΊ β πΉ) = ( I βΎ πΈ)))) | ||
Theorem | rngcinvALTV 46009 | An inverse in the category of non-unital rings is the converse operation. (Contributed by AV, 28-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RngCatALTVβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ π = (InvβπΆ) β β’ (π β (πΉ(πππ)πΊ β (πΉ β (π RngIsom π) β§ πΊ = β‘πΉ))) | ||
Theorem | rngcisoALTV 46010 | An isomorphism in the category of non-unital rings is a bijection. (Contributed by AV, 28-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RngCatALTVβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ πΌ = (IsoβπΆ) β β’ (π β (πΉ β (ππΌπ) β πΉ β (π RngIsom π))) | ||
Theorem | rngchomffvalALTV 46011* | The value of the functionalized Hom-set operation in the category of non-unital rings (in a universe) in maps-to notation for an operation. (Contributed by AV, 1-Mar-2020.) (New usage is discouraged.) |
β’ πΆ = (RngCatALTVβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ πΉ = (Homf βπΆ) β β’ (π β πΉ = (π₯ β π΅, π¦ β π΅ β¦ (π₯ RngHomo π¦))) | ||
Theorem | rngchomrnghmresALTV 46012 | The value of the functionalized Hom-set operation in the category of non-unital rings (in a universe) as restriction of the non-unital ring homomorphisms. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.) |
β’ πΆ = (RngCatALTVβπ) & β’ π΅ = (Rng β© π) & β’ (π β π β π) & β’ πΉ = (Homf βπΆ) β β’ (π β πΉ = ( RngHomo βΎ (π΅ Γ π΅))) | ||
Theorem | rngcifuestrc 46013* | The "inclusion functor" from the category of non-unital rings into the category of extensible structures. (Contributed by AV, 30-Mar-2020.) |
β’ π = (RngCatβπ) & β’ πΈ = (ExtStrCatβπ) & β’ π΅ = (Baseβπ ) & β’ (π β π β π) & β’ (π β πΉ = ( I βΎ π΅)) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RngHomo π¦)))) β β’ (π β πΉ(π Func πΈ)πΊ) | ||
Theorem | funcrngcsetc 46014* | The "natural forgetful functor" from the category of non-unital rings into the category of sets which sends each non-unital ring to its underlying set (base set) and the morphisms (non-unital ring homomorphisms) to mappings of the corresponding base sets. An alternate proof is provided in funcrngcsetcALT 46015, using cofuval2 17708 to construct the "natural forgetful functor" from the category of non-unital rings into the category of sets by composing the "inclusion functor" from the category of non-unital rings into the category of extensible structures, see rngcifuestrc 46013, and the "natural forgetful functor" from the category of extensible structures into the category of sets, see funcestrcsetc 17972. (Contributed by AV, 26-Mar-2020.) |
β’ π = (RngCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RngHomo π¦)))) β β’ (π β πΉ(π Func π)πΊ) | ||
Theorem | funcrngcsetcALT 46015* | Alternate proof of funcrngcsetc 46014, using cofuval2 17708 to construct the "natural forgetful functor" from the category of non-unital rings into the category of sets by composing the "inclusion functor" from the category of non-unital rings into the category of extensible structures, see rngcifuestrc 46013, and the "natural forgetful functor" from the category of extensible structures into the category of sets, see funcestrcsetc 17972. Surprisingly, this proof is longer than the direct proof given in funcrngcsetc 46014. (Contributed by AV, 30-Mar-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π = (RngCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RngHomo π¦)))) β β’ (π β πΉ(π Func π)πΊ) | ||
Theorem | zrinitorngc 46016 | The zero ring is an initial object in the category of non-unital rings. (Contributed by AV, 18-Apr-2020.) |
β’ (π β π β π) & β’ πΆ = (RngCatβπ) & β’ (π β π β (Ring β NzRing)) & β’ (π β π β π) β β’ (π β π β (InitOβπΆ)) | ||
Theorem | zrtermorngc 46017 | The zero ring is a terminal object in the category of non-unital rings. (Contributed by AV, 17-Apr-2020.) |
β’ (π β π β π) & β’ πΆ = (RngCatβπ) & β’ (π β π β (Ring β NzRing)) & β’ (π β π β π) β β’ (π β π β (TermOβπΆ)) | ||
Theorem | zrzeroorngc 46018 | The zero ring is a zero object in the category of non-unital rings. (Contributed by AV, 18-Apr-2020.) |
β’ (π β π β π) & β’ πΆ = (RngCatβπ) & β’ (π β π β (Ring β NzRing)) & β’ (π β π β π) β β’ (π β π β (ZeroOβπΆ)) | ||
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 46021. 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 46034. 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 46027, and the morphisms/arrows are the ring homomorphisms restricted to this subset of the rings ( RingHom βΎ (π΅ Γ π΅)), see ringchomfval 46028, whereas the composition is the ordinary composition of functions, see ringccofval 46032 and ringcco 46033. By showing that the ring homomorphisms between rings are a subcategory subset (βcat) of the mappings between base sets of extensible structures, see rhmsscmap 46036, it can be shown that the ring homomorphisms between rings are a subcategory (Subcat) of the category of extensible structures, see rhmsubcsetc 46039. It follows that the category of rings RingCat is actually a category, see ringccat 46040 with the identity function as identity arrow, see ringcid 46041. 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 46042, and that the ring homomorphisms between rings are a subcategory of the category of non-unital rings, see rhmsubcrngc 46045. 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 46046: ((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 46051. | ||
Syntax | cringc 46019 | Extend class notation to include the category Ring. |
class RingCat | ||
Syntax | cringcALTV 46020 | Extend class notation to include the category Ring. (New usage is discouraged.) |
class RingCatALTV | ||
Definition | df-ringc 46021 | 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 46022* | 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 46023* | 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 46024 | 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 46025 | 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 46026 | 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 46027 | 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 46028 | 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 46029 | Set of arrows of the category of unital rings (in a universe). (Contributed by AV, 14-Feb-2020.) |
β’ πΆ = (RingCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ π» = (Hom βπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (ππ»π) = (π RingHom π)) | ||
Theorem | elringchom 46030 | A morphism of unital rings is a function. (Contributed by AV, 14-Feb-2020.) |
β’ πΆ = (RingCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ π» = (Hom βπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (πΉ β (ππ»π) β πΉ:(Baseβπ)βΆ(Baseβπ))) | ||
Theorem | ringchomfeqhom 46031 | 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 46032 | 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 46033 | 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 46034 | 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 46035* | 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 46036* | 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 46037 | Lemma 1 for rhmsubcsetc 46039. (Contributed by AV, 9-Mar-2020.) |
β’ πΆ = (ExtStrCatβπ) & β’ (π β π β π) & β’ (π β π΅ = (Ring β© π)) & β’ (π β π» = ( RingHom βΎ (π΅ Γ π΅))) β β’ ((π β§ π₯ β π΅) β ((IdβπΆ)βπ₯) β (π₯π»π₯)) | ||
Theorem | rhmsubcsetclem2 46038* | Lemma 2 for rhmsubcsetc 46039. (Contributed by AV, 9-Mar-2020.) |
β’ πΆ = (ExtStrCatβπ) & β’ (π β π β π) & β’ (π β π΅ = (Ring β© π)) & β’ (π β π» = ( RingHom βΎ (π΅ Γ π΅))) β β’ ((π β§ π₯ β π΅) β βπ¦ β π΅ βπ§ β π΅ βπ β (π₯π»π¦)βπ β (π¦π»π§)(π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯π»π§)) | ||
Theorem | rhmsubcsetc 46039 | 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 46040 | The category of unital rings is a category. (Contributed by AV, 14-Feb-2020.) (Revised by AV, 9-Mar-2020.) |
β’ πΆ = (RingCatβπ) β β’ (π β π β πΆ β Cat) | ||
Theorem | ringcid 46041 | 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 46042 | 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 46043 | Lemma 1 for rhmsubcrngc 46045. (Contributed by AV, 9-Mar-2020.) |
β’ πΆ = (RngCatβπ) & β’ (π β π β π) & β’ (π β π΅ = (Ring β© π)) & β’ (π β π» = ( RingHom βΎ (π΅ Γ π΅))) β β’ ((π β§ π₯ β π΅) β ((IdβπΆ)βπ₯) β (π₯π»π₯)) | ||
Theorem | rhmsubcrngclem2 46044* | Lemma 2 for rhmsubcrngc 46045. (Contributed by AV, 12-Mar-2020.) |
β’ πΆ = (RngCatβπ) & β’ (π β π β π) & β’ (π β π΅ = (Ring β© π)) & β’ (π β π» = ( RingHom βΎ (π΅ Γ π΅))) β β’ ((π β§ π₯ β π΅) β βπ¦ β π΅ βπ§ β π΅ βπ β (π₯π»π¦)βπ β (π¦π»π§)(π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯π»π§)) | ||
Theorem | rhmsubcrngc 46045 | 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 46046 | 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 46047 | 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 46048 | An inverse in the category of unital rings is the converse operation. (Contributed by AV, 14-Feb-2020.) |
β’ πΆ = (RingCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ π = (InvβπΆ) β β’ (π β (πΉ(πππ)πΊ β (πΉ β (π RingIso π) β§ πΊ = β‘πΉ))) | ||
Theorem | ringciso 46049 | An isomorphism in the category of unital rings is a bijection. (Contributed by AV, 14-Feb-2020.) |
β’ πΆ = (RingCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ πΌ = (IsoβπΆ) β β’ (π β (πΉ β (ππΌπ) β πΉ β (π RingIso π))) | ||
Theorem | ringcbasbas 46050 | 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 46051* | 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 46052* | Lemma 1 for funcringcsetcALTV2 46061. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) β β’ ((π β§ π β π΅) β (πΉβπ) = (Baseβπ)) | ||
Theorem | funcringcsetcALTV2lem2 46053* | Lemma 2 for funcringcsetcALTV2 46061. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) β β’ ((π β§ π β π΅) β (πΉβπ) β π) | ||
Theorem | funcringcsetcALTV2lem3 46054* | Lemma 3 for funcringcsetcALTV2 46061. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) β β’ (π β πΉ:π΅βΆπΆ) | ||
Theorem | funcringcsetcALTV2lem4 46055* | Lemma 4 for funcringcsetcALTV2 46061. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ (π β πΊ Fn (π΅ Γ π΅)) | ||
Theorem | funcringcsetcALTV2lem5 46056* | Lemma 5 for funcringcsetcALTV2 46061. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΊπ) = ( I βΎ (π RingHom π))) | ||
Theorem | funcringcsetcALTV2lem6 46057* | Lemma 6 for funcringcsetcALTV2 46061. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ ((π β§ (π β π΅ β§ π β π΅) β§ π» β (π RingHom π)) β ((ππΊπ)βπ») = π») | ||
Theorem | funcringcsetcALTV2lem7 46058* | Lemma 7 for funcringcsetcALTV2 46061. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ ((π β§ π β π΅) β ((ππΊπ)β((Idβπ )βπ)) = ((Idβπ)β(πΉβπ))) | ||
Theorem | funcringcsetcALTV2lem8 46059* | Lemma 8 for funcringcsetcALTV2 46061. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΊπ):(π(Hom βπ )π)βΆ((πΉβπ)(Hom βπ)(πΉβπ))) | ||
Theorem | funcringcsetcALTV2lem9 46060* | Lemma 9 for funcringcsetcALTV2 46061. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ ((π β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π» β (π(Hom βπ )π) β§ πΎ β (π(Hom βπ )π))) β ((ππΊπ)β(πΎ(β¨π, πβ©(compβπ )π)π»)) = (((ππΊπ)βπΎ)(β¨(πΉβπ), (πΉβπ)β©(compβπ)(πΉβπ))((ππΊπ)βπ»))) | ||
Theorem | funcringcsetcALTV2 46061* | 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 46062 | 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 46063* | 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 46064 | 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 46065 | A morphism of rings is a function. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RingCatALTVβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ π» = (Hom βπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (πΉ β (ππ»π) β πΉ:(Baseβπ)βΆ(Baseβπ))) | ||
Theorem | ringccofvalALTV 46066* | 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 46067 | Composition in the category of rings. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RingCatALTVβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ Β· = (compβπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ β (π RingHom π)) & β’ (π β πΊ β (π RingHom π)) β β’ (π β (πΊ(β¨π, πβ© Β· π)πΉ) = (πΊ β πΉ)) | ||
Theorem | ringccatidALTV 46068* | Lemma for ringccatALTV 46069. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RingCatALTVβπ) & β’ π΅ = (BaseβπΆ) β β’ (π β π β (πΆ β Cat β§ (IdβπΆ) = (π₯ β π΅ β¦ ( I βΎ (Baseβπ₯))))) | ||
Theorem | ringccatALTV 46069 | The category of rings is a category. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RingCatALTVβπ) β β’ (π β π β πΆ β Cat) | ||
Theorem | ringcidALTV 46070 | 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 46071 | 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 46072 | 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 46073 | 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 46074 | 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 46075* | Lemma 1 for funcringcsetcALTV 46084. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatALTVβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) β β’ ((π β§ π β π΅) β (πΉβπ) = (Baseβπ)) | ||
Theorem | funcringcsetclem2ALTV 46076* | Lemma 2 for funcringcsetcALTV 46084. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatALTVβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) β β’ ((π β§ π β π΅) β (πΉβπ) β π) | ||
Theorem | funcringcsetclem3ALTV 46077* | Lemma 3 for funcringcsetcALTV 46084. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatALTVβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) β β’ (π β πΉ:π΅βΆπΆ) | ||
Theorem | funcringcsetclem4ALTV 46078* | Lemma 4 for funcringcsetcALTV 46084. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatALTVβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ (π β πΊ Fn (π΅ Γ π΅)) | ||
Theorem | funcringcsetclem5ALTV 46079* | Lemma 5 for funcringcsetcALTV 46084. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatALTVβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΊπ) = ( I βΎ (π RingHom π))) | ||
Theorem | funcringcsetclem6ALTV 46080* | Lemma 6 for funcringcsetcALTV 46084. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatALTVβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ ((π β§ (π β π΅ β§ π β π΅) β§ π» β (π RingHom π)) β ((ππΊπ)βπ») = π») | ||
Theorem | funcringcsetclem7ALTV 46081* | Lemma 7 for funcringcsetcALTV 46084. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatALTVβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ ((π β§ π β π΅) β ((ππΊπ)β((Idβπ )βπ)) = ((Idβπ)β(πΉβπ))) | ||
Theorem | funcringcsetclem8ALTV 46082* | Lemma 8 for funcringcsetcALTV 46084. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatALTVβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΊπ):(π(Hom βπ )π)βΆ((πΉβπ)(Hom βπ)(πΉβπ))) | ||
Theorem | funcringcsetclem9ALTV 46083* | Lemma 9 for funcringcsetcALTV 46084. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatALTVβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ ((π β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π» β (π(Hom βπ )π) β§ πΎ β (π(Hom βπ )π))) β ((ππΊπ)β(πΎ(β¨π, πβ©(compβπ )π)π»)) = (((ππΊπ)βπΎ)(β¨(πΉβπ), (πΉβπ)β©(compβπ)(πΉβπ))((ππΊπ)βπ»))) | ||
Theorem | funcringcsetcALTV 46084* | 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 46085 | 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 46086 | 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 46087* | 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 46088 | 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 46089* | Lemma 1 for srhmsubc 46092. (Contributed by AV, 19-Feb-2020.) |
β’ βπ β π π β Ring & β’ πΆ = (π β© π) β β’ (π β πΆ β π β (π β© Ring)) | ||
Theorem | srhmsubclem2 46090* | Lemma 2 for srhmsubc 46092. (Contributed by AV, 19-Feb-2020.) |
β’ βπ β π π β Ring & β’ πΆ = (π β© π) β β’ ((π β π β§ π β πΆ) β π β (Baseβ(RingCatβπ))) | ||
Theorem | srhmsubclem3 46091* | Lemma 3 for srhmsubc 46092. (Contributed by AV, 19-Feb-2020.) |
β’ βπ β π π β Ring & β’ πΆ = (π β© π) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ ((π β π β§ (π β πΆ β§ π β πΆ)) β (ππ½π) = (π(Hom β(RingCatβπ))π)) | ||
Theorem | srhmsubc 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.) |
β’ βπ β π π β Ring & β’ πΆ = (π β© π) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β π½ β (Subcatβ(RingCatβπ))) | ||
Theorem | sringcat 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.) |
β’ βπ β π π β Ring & β’ πΆ = (π β© π) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β ((RingCatβπ) βΎcat π½) β Cat) | ||
Theorem | crhmsubc 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.) |
β’ πΆ = (π β© CRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β π½ β (Subcatβ(RingCatβπ))) | ||
Theorem | cringcat 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.) |
β’ πΆ = (π β© CRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β ((RingCatβπ) βΎcat π½) β Cat) | ||
Theorem | drhmsubc 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.) |
β’ πΆ = (π β© DivRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β π½ β (Subcatβ(RingCatβπ))) | ||
Theorem | drngcat 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.) |
β’ πΆ = (π β© DivRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β ((RingCatβπ) βΎcat π½) β Cat) | ||
Theorem | fldcat 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.) |
β’ πΆ = (π β© DivRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) & β’ π· = (π β© Field) & β’ πΉ = (π β π·, π β π· β¦ (π RingHom π )) β β’ (π β π β ((RingCatβπ) βΎcat πΉ) β Cat) | ||
Theorem | fldc 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.) |
β’ πΆ = (π β© DivRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) & β’ π· = (π β© Field) & β’ πΉ = (π β π·, π β π· β¦ (π RingHom π )) β β’ (π β π β (((RingCatβπ) βΎcat π½) βΎcat πΉ) β Cat) | ||
Theorem | fldhmsubc 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.) |
β’ πΆ = (π β© DivRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) & β’ π· = (π β© Field) & β’ πΉ = (π β π·, π β π· β¦ (π RingHom π )) β β’ (π β π β πΉ β (Subcatβ((RingCatβπ) βΎcat π½))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |