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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cznabel 46001 | The ring constructed from a β€/nβ€ structure by replacing the (multiplicative) ring operation by a constant operation is an abelian group. (Contributed by AV, 16-Feb-2020.) |
β’ π = (β€/nβ€βπ) & β’ π΅ = (Baseβπ) & β’ π = (π sSet β¨(.rβndx), (π₯ β π΅, π¦ β π΅ β¦ πΆ)β©) β β’ ((π β β β§ πΆ β π΅) β π β Abel) | ||
Theorem | cznrng 46002* | The ring constructed from a β€/nβ€ structure by replacing the (multiplicative) ring operation by a constant operation is a non-unital ring. (Contributed by AV, 17-Feb-2020.) |
β’ π = (β€/nβ€βπ) & β’ π΅ = (Baseβπ) & β’ π = (π sSet β¨(.rβndx), (π₯ β π΅, π¦ β π΅ β¦ πΆ)β©) & β’ 0 = (0gβπ) β β’ ((π β β β§ πΆ = 0 ) β π β Rng) | ||
Theorem | cznnring 46003* | The ring constructed from a β€/nβ€ structure with 1 < π by replacing the (multiplicative) ring operation by a constant operation is not a unital ring. (Contributed by AV, 17-Feb-2020.) |
β’ π = (β€/nβ€βπ) & β’ π΅ = (Baseβπ) & β’ π = (π sSet β¨(.rβndx), (π₯ β π΅, π¦ β π΅ β¦ πΆ)β©) & β’ 0 = (0gβπ) β β’ ((π β (β€β₯β2) β§ πΆ β π΅) β π β Ring) | ||
The "category of non-unital rings" RngCat is the category of all non-unital rings Rng in a universe and non-unital ring homomorphisms RngHomo between these rings. This category is defined as "category restriction" of the category of extensible structures ExtStrCat, which restricts the objects to non-unital rings and the morphisms to the non-unital ring homomorphisms, while the composition of morphisms is preserved, see df-rngc 46006. Alternately, the category of non-unital rings could have been defined as extensible structure consisting of three components/slots for the objects, morphisms and composition, see df-rngcALTV 46007 or dfrngc2 46019. 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 non-unital rings (relativized to a subset or "universe" π’) (π’ β© Rng), see rngcbas 46012, and the morphisms/arrows are the non-unital ring homomorphisms restricted to this subset of the non-unital rings ( RngHomo βΎ (π΅ Γ π΅)), see rngchomfval 46013, whereas the composition is the ordinary composition of functions, see rngccofval 46017 and rngcco 46018. By showing that the non-unital ring homomorphisms between non-unital rings are a subcategory subset (βcat) of the mappings between base sets of extensible structures, see rnghmsscmap 46021, it can be shown that the non-unital ring homomorphisms between non-unital rings are a subcategory (Subcat) of the category of extensible structures, see rnghmsubcsetc 46024. It follows that the category of non-unital rings RngCat is actually a category, see rngccat 46025 with the identity function as identity arrow, see rngcid 46026. | ||
Syntax | crngc 46004 | Extend class notation to include the category Rng. |
class RngCat | ||
Syntax | crngcALTV 46005 | Extend class notation to include the category Rng. (New usage is discouraged.) |
class RngCatALTV | ||
Definition | df-rngc 46006 | Definition of the category Rng, relativized to a subset π’. This is the category of all non-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, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.) |
β’ RngCat = (π’ β V β¦ ((ExtStrCatβπ’) βΎcat ( RngHomo βΎ ((π’ β© Rng) Γ (π’ β© Rng))))) | ||
Definition | df-rngcALTV 46007* | Definition of the category Rng, relativized to a subset π’. This is the category of all non-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. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.) |
β’ RngCatALTV = (π’ β V β¦ β¦(π’ β© Rng) / πβ¦{β¨(Baseβndx), πβ©, β¨(Hom βndx), (π₯ β π, π¦ β π β¦ (π₯ RngHomo π¦))β©, β¨(compβndx), (π£ β (π Γ π), π§ β π β¦ (π β ((2nd βπ£) RngHomo π§), π β ((1st βπ£) RngHomo (2nd βπ£)) β¦ (π β π)))β©}) | ||
Theorem | rngcvalALTV 46008* | Value of the category of non-unital rings (in a universe). (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.) |
β’ πΆ = (RngCatALTVβπ) & β’ (π β π β π) & β’ (π β π΅ = (π β© Rng)) & β’ (π β π» = (π₯ β π΅, π¦ β π΅ β¦ (π₯ RngHomo π¦))) & β’ (π β Β· = (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) RngHomo π§), π β ((1st βπ£) RngHomo (2nd βπ£)) β¦ (π β π)))) β β’ (π β πΆ = {β¨(Baseβndx), π΅β©, β¨(Hom βndx), π»β©, β¨(compβndx), Β· β©}) | ||
Theorem | rngcval 46009 | Value of the category of non-unital rings (in a universe). (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.) |
β’ πΆ = (RngCatβπ) & β’ (π β π β π) & β’ (π β π΅ = (π β© Rng)) & β’ (π β π» = ( RngHomo βΎ (π΅ Γ π΅))) β β’ (π β πΆ = ((ExtStrCatβπ) βΎcat π»)) | ||
Theorem | rnghmresfn 46010 | The class of non-unital ring homomorphisms restricted to subsets of non-unital rings is a function. (Contributed by AV, 4-Mar-2020.) |
β’ (π β π΅ = (π β© Rng)) & β’ (π β π» = ( RngHomo βΎ (π΅ Γ π΅))) β β’ (π β π» Fn (π΅ Γ π΅)) | ||
Theorem | rnghmresel 46011 | An element of the non-unital ring homomorphisms restricted to a subset of non-unital rings is a non-unital ring homomorphisms. (Contributed by AV, 9-Mar-2020.) |
β’ (π β π» = ( RngHomo βΎ (π΅ Γ π΅))) β β’ ((π β§ (π β π΅ β§ π β π΅) β§ πΉ β (ππ»π)) β πΉ β (π RngHomo π)) | ||
Theorem | rngcbas 46012 | Set of objects of the category of non-unital rings (in a universe). (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.) |
β’ πΆ = (RngCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) β β’ (π β π΅ = (π β© Rng)) | ||
Theorem | rngchomfval 46013 | Set of arrows of the category of non-unital rings (in a universe). (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.) |
β’ πΆ = (RngCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ π» = (Hom βπΆ) β β’ (π β π» = ( RngHomo βΎ (π΅ Γ π΅))) | ||
Theorem | rngchom 46014 | Set of arrows of the category of non-unital rings (in a universe). (Contributed by AV, 27-Feb-2020.) |
β’ πΆ = (RngCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ π» = (Hom βπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (ππ»π) = (π RngHomo π)) | ||
Theorem | elrngchom 46015 | A morphism of non-unital rings is a function. (Contributed by AV, 27-Feb-2020.) |
β’ πΆ = (RngCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ π» = (Hom βπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (πΉ β (ππ»π) β πΉ:(Baseβπ)βΆ(Baseβπ))) | ||
Theorem | rngchomfeqhom 46016 | The functionalized Hom-set operation equals the Hom-set operation in the category of non-unital rings (in a universe). (Contributed by AV, 9-Mar-2020.) |
β’ πΆ = (RngCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) β β’ (π β (Homf βπΆ) = (Hom βπΆ)) | ||
Theorem | rngccofval 46017 | Composition in the category of non-unital rings. (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.) |
β’ πΆ = (RngCatβπ) & β’ (π β π β π) & β’ Β· = (compβπΆ) β β’ (π β Β· = (compβ(ExtStrCatβπ))) | ||
Theorem | rngcco 46018 | Composition in the category of non-unital rings. (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.) |
β’ πΆ = (RngCatβπ) & β’ (π β π β π) & β’ Β· = (compβπΆ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β πΉ:(Baseβπ)βΆ(Baseβπ)) & β’ (π β πΊ:(Baseβπ)βΆ(Baseβπ)) β β’ (π β (πΊ(β¨π, πβ© Β· π)πΉ) = (πΊ β πΉ)) | ||
Theorem | dfrngc2 46019 | Alternate definition of the category of non-unital rings (in a universe). (Contributed by AV, 16-Mar-2020.) |
β’ πΆ = (RngCatβπ) & β’ (π β π β π) & β’ (π β π΅ = (π β© Rng)) & β’ (π β π» = ( RngHomo βΎ (π΅ Γ π΅))) & β’ (π β Β· = (compβ(ExtStrCatβπ))) β β’ (π β πΆ = {β¨(Baseβndx), π΅β©, β¨(Hom βndx), π»β©, β¨(compβndx), Β· β©}) | ||
Theorem | rnghmsscmap2 46020* | The non-unital ring homomorphisms between non-unital rings (in a universe) are a subcategory subset of the mappings between base sets of non-unital rings (in the same universe). (Contributed by AV, 6-Mar-2020.) |
β’ (π β π β π) & β’ (π β π = (Rng β© π)) β β’ (π β ( RngHomo βΎ (π Γ π )) βcat (π₯ β π , π¦ β π β¦ ((Baseβπ¦) βm (Baseβπ₯)))) | ||
Theorem | rnghmsscmap 46021* | The non-unital ring homomorphisms between non-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.) |
β’ (π β π β π) & β’ (π β π = (Rng β© π)) β β’ (π β ( RngHomo βΎ (π Γ π )) βcat (π₯ β π, π¦ β π β¦ ((Baseβπ¦) βm (Baseβπ₯)))) | ||
Theorem | rnghmsubcsetclem1 46022 | Lemma 1 for rnghmsubcsetc 46024. (Contributed by AV, 9-Mar-2020.) |
β’ πΆ = (ExtStrCatβπ) & β’ (π β π β π) & β’ (π β π΅ = (Rng β© π)) & β’ (π β π» = ( RngHomo βΎ (π΅ Γ π΅))) β β’ ((π β§ π₯ β π΅) β ((IdβπΆ)βπ₯) β (π₯π»π₯)) | ||
Theorem | rnghmsubcsetclem2 46023* | Lemma 2 for rnghmsubcsetc 46024. (Contributed by AV, 9-Mar-2020.) |
β’ πΆ = (ExtStrCatβπ) & β’ (π β π β π) & β’ (π β π΅ = (Rng β© π)) & β’ (π β π» = ( RngHomo βΎ (π΅ Γ π΅))) β β’ ((π β§ π₯ β π΅) β βπ¦ β π΅ βπ§ β π΅ βπ β (π₯π»π¦)βπ β (π¦π»π§)(π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯π»π§)) | ||
Theorem | rnghmsubcsetc 46024 | The non-unital ring homomorphisms between non-unital rings (in a universe) are a subcategory of the category of extensible structures. (Contributed by AV, 9-Mar-2020.) |
β’ πΆ = (ExtStrCatβπ) & β’ (π β π β π) & β’ (π β π΅ = (Rng β© π)) & β’ (π β π» = ( RngHomo βΎ (π΅ Γ π΅))) β β’ (π β π» β (SubcatβπΆ)) | ||
Theorem | rngccat 46025 | The category of non-unital rings is a category. (Contributed by AV, 27-Feb-2020.) (Revised by AV, 9-Mar-2020.) |
β’ πΆ = (RngCatβπ) β β’ (π β π β πΆ β Cat) | ||
Theorem | rngcid 46026 | The identity arrow in the category of non-unital rings is the identity function. (Contributed by AV, 27-Feb-2020.) (Revised by AV, 10-Mar-2020.) |
β’ πΆ = (RngCatβπ) & β’ π΅ = (BaseβπΆ) & β’ 1 = (IdβπΆ) & β’ (π β π β π) & β’ (π β π β π΅) & β’ π = (Baseβπ) β β’ (π β ( 1 βπ) = ( I βΎ π)) | ||
Theorem | rngcsect 46027 | A section in the category of non-unital rings, written out. (Contributed by AV, 28-Feb-2020.) |
β’ πΆ = (RngCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ πΈ = (Baseβπ) & β’ π = (SectβπΆ) β β’ (π β (πΉ(πππ)πΊ β (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π) β§ (πΊ β πΉ) = ( I βΎ πΈ)))) | ||
Theorem | rngcinv 46028 | An inverse in the category of non-unital rings is the converse operation. (Contributed by AV, 28-Feb-2020.) |
β’ πΆ = (RngCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ π = (InvβπΆ) β β’ (π β (πΉ(πππ)πΊ β (πΉ β (π RngIsom π) β§ πΊ = β‘πΉ))) | ||
Theorem | rngciso 46029 | An isomorphism in the category of non-unital rings is a bijection. (Contributed by AV, 28-Feb-2020.) |
β’ πΆ = (RngCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ πΌ = (IsoβπΆ) β β’ (π β (πΉ β (ππΌπ) β πΉ β (π RngIsom π))) | ||
Theorem | rngcbasALTV 46030 | Set of objects of the category of non-unital rings (in a universe). (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.) |
β’ πΆ = (RngCatALTVβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) β β’ (π β π΅ = (π β© Rng)) | ||
Theorem | rngchomfvalALTV 46031* | 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 | rngchomALTV 46032 | 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 46033 | 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 46034* | 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 46035 | 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 46036* | Lemma for rngccatALTV 46037. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.) |
β’ πΆ = (RngCatALTVβπ) & β’ π΅ = (BaseβπΆ) β β’ (π β π β (πΆ β Cat β§ (IdβπΆ) = (π₯ β π΅ β¦ ( I βΎ (Baseβπ₯))))) | ||
Theorem | rngccatALTV 46037 | The category of non-unital rings is a category. (Contributed by AV, 27-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RngCatALTVβπ) β β’ (π β π β πΆ β Cat) | ||
Theorem | rngcidALTV 46038 | 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 46039 | 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 46040 | 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 46041 | 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 46042* | 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 46043 | 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 46044* | 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 46045* | 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 46046, using cofuval2 17707 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 46044, and the "natural forgetful functor" from the category of extensible structures into the category of sets, see funcestrcsetc 17971. (Contributed by AV, 26-Mar-2020.) |
β’ π = (RngCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RngHomo π¦)))) β β’ (π β πΉ(π Func π)πΊ) | ||
Theorem | funcrngcsetcALT 46046* | Alternate proof of funcrngcsetc 46045, using cofuval2 17707 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 46044, and the "natural forgetful functor" from the category of extensible structures into the category of sets, see funcestrcsetc 17971. Surprisingly, this proof is longer than the direct proof given in funcrngcsetc 46045. (Contributed by AV, 30-Mar-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π = (RngCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RngHomo π¦)))) β β’ (π β πΉ(π Func π)πΊ) | ||
Theorem | zrinitorngc 46047 | 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 46048 | 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 46049 | 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 46052. 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 46065. 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 46058, and the morphisms/arrows are the ring homomorphisms restricted to this subset of the rings ( RingHom βΎ (π΅ Γ π΅)), see ringchomfval 46059, whereas the composition is the ordinary composition of functions, see ringccofval 46063 and ringcco 46064. By showing that the ring homomorphisms between rings are a subcategory subset (βcat) of the mappings between base sets of extensible structures, see rhmsscmap 46067, it can be shown that the ring homomorphisms between rings are a subcategory (Subcat) of the category of extensible structures, see rhmsubcsetc 46070. It follows that the category of rings RingCat is actually a category, see ringccat 46071 with the identity function as identity arrow, see ringcid 46072. 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 46073, and that the ring homomorphisms between rings are a subcategory of the category of non-unital rings, see rhmsubcrngc 46076. 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 46077: ((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 46082. | ||
Syntax | cringc 46050 | Extend class notation to include the category Ring. |
class RingCat | ||
Syntax | cringcALTV 46051 | Extend class notation to include the category Ring. (New usage is discouraged.) |
class RingCatALTV | ||
Definition | df-ringc 46052 | 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 46053* | 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 46054* | 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 46055 | 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 46056 | 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 46057 | 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 46058 | 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 46059 | 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 46060 | Set of arrows of the category of unital rings (in a universe). (Contributed by AV, 14-Feb-2020.) |
β’ πΆ = (RingCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ π» = (Hom βπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (ππ»π) = (π RingHom π)) | ||
Theorem | elringchom 46061 | A morphism of unital rings is a function. (Contributed by AV, 14-Feb-2020.) |
β’ πΆ = (RingCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ π» = (Hom βπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (πΉ β (ππ»π) β πΉ:(Baseβπ)βΆ(Baseβπ))) | ||
Theorem | ringchomfeqhom 46062 | 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 46063 | 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 46064 | 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 46065 | 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 46066* | 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 46067* | 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 46068 | Lemma 1 for rhmsubcsetc 46070. (Contributed by AV, 9-Mar-2020.) |
β’ πΆ = (ExtStrCatβπ) & β’ (π β π β π) & β’ (π β π΅ = (Ring β© π)) & β’ (π β π» = ( RingHom βΎ (π΅ Γ π΅))) β β’ ((π β§ π₯ β π΅) β ((IdβπΆ)βπ₯) β (π₯π»π₯)) | ||
Theorem | rhmsubcsetclem2 46069* | Lemma 2 for rhmsubcsetc 46070. (Contributed by AV, 9-Mar-2020.) |
β’ πΆ = (ExtStrCatβπ) & β’ (π β π β π) & β’ (π β π΅ = (Ring β© π)) & β’ (π β π» = ( RingHom βΎ (π΅ Γ π΅))) β β’ ((π β§ π₯ β π΅) β βπ¦ β π΅ βπ§ β π΅ βπ β (π₯π»π¦)βπ β (π¦π»π§)(π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯π»π§)) | ||
Theorem | rhmsubcsetc 46070 | 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 46071 | The category of unital rings is a category. (Contributed by AV, 14-Feb-2020.) (Revised by AV, 9-Mar-2020.) |
β’ πΆ = (RingCatβπ) β β’ (π β π β πΆ β Cat) | ||
Theorem | ringcid 46072 | 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 46073 | 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 46074 | Lemma 1 for rhmsubcrngc 46076. (Contributed by AV, 9-Mar-2020.) |
β’ πΆ = (RngCatβπ) & β’ (π β π β π) & β’ (π β π΅ = (Ring β© π)) & β’ (π β π» = ( RingHom βΎ (π΅ Γ π΅))) β β’ ((π β§ π₯ β π΅) β ((IdβπΆ)βπ₯) β (π₯π»π₯)) | ||
Theorem | rhmsubcrngclem2 46075* | Lemma 2 for rhmsubcrngc 46076. (Contributed by AV, 12-Mar-2020.) |
β’ πΆ = (RngCatβπ) & β’ (π β π β π) & β’ (π β π΅ = (Ring β© π)) & β’ (π β π» = ( RingHom βΎ (π΅ Γ π΅))) β β’ ((π β§ π₯ β π΅) β βπ¦ β π΅ βπ§ β π΅ βπ β (π₯π»π¦)βπ β (π¦π»π§)(π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯π»π§)) | ||
Theorem | rhmsubcrngc 46076 | 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 46077 | 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 46078 | 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 46079 | An inverse in the category of unital rings is the converse operation. (Contributed by AV, 14-Feb-2020.) |
β’ πΆ = (RingCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ π = (InvβπΆ) β β’ (π β (πΉ(πππ)πΊ β (πΉ β (π RingIso π) β§ πΊ = β‘πΉ))) | ||
Theorem | ringciso 46080 | An isomorphism in the category of unital rings is a bijection. (Contributed by AV, 14-Feb-2020.) |
β’ πΆ = (RingCatβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ πΌ = (IsoβπΆ) β β’ (π β (πΉ β (ππΌπ) β πΉ β (π RingIso π))) | ||
Theorem | ringcbasbas 46081 | 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 46082* | 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 46083* | Lemma 1 for funcringcsetcALTV2 46092. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) β β’ ((π β§ π β π΅) β (πΉβπ) = (Baseβπ)) | ||
Theorem | funcringcsetcALTV2lem2 46084* | Lemma 2 for funcringcsetcALTV2 46092. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) β β’ ((π β§ π β π΅) β (πΉβπ) β π) | ||
Theorem | funcringcsetcALTV2lem3 46085* | Lemma 3 for funcringcsetcALTV2 46092. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) β β’ (π β πΉ:π΅βΆπΆ) | ||
Theorem | funcringcsetcALTV2lem4 46086* | Lemma 4 for funcringcsetcALTV2 46092. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ (π β πΊ Fn (π΅ Γ π΅)) | ||
Theorem | funcringcsetcALTV2lem5 46087* | Lemma 5 for funcringcsetcALTV2 46092. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΊπ) = ( I βΎ (π RingHom π))) | ||
Theorem | funcringcsetcALTV2lem6 46088* | Lemma 6 for funcringcsetcALTV2 46092. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ ((π β§ (π β π΅ β§ π β π΅) β§ π» β (π RingHom π)) β ((ππΊπ)βπ») = π») | ||
Theorem | funcringcsetcALTV2lem7 46089* | Lemma 7 for funcringcsetcALTV2 46092. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ ((π β§ π β π΅) β ((ππΊπ)β((Idβπ )βπ)) = ((Idβπ)β(πΉβπ))) | ||
Theorem | funcringcsetcALTV2lem8 46090* | Lemma 8 for funcringcsetcALTV2 46092. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΊπ):(π(Hom βπ )π)βΆ((πΉβπ)(Hom βπ)(πΉβπ))) | ||
Theorem | funcringcsetcALTV2lem9 46091* | Lemma 9 for funcringcsetcALTV2 46092. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ ((π β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π» β (π(Hom βπ )π) β§ πΎ β (π(Hom βπ )π))) β ((ππΊπ)β(πΎ(β¨π, πβ©(compβπ )π)π»)) = (((ππΊπ)βπΎ)(β¨(πΉβπ), (πΉβπ)β©(compβπ)(πΉβπ))((ππΊπ)βπ»))) | ||
Theorem | funcringcsetcALTV2 46092* | 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 46093 | 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 46094* | 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 46095 | 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 46096 | A morphism of rings is a function. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RingCatALTVβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ π» = (Hom βπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (πΉ β (ππ»π) β πΉ:(Baseβπ)βΆ(Baseβπ))) | ||
Theorem | ringccofvalALTV 46097* | 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 46098 | Composition in the category of rings. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RingCatALTVβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ Β· = (compβπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ β (π RingHom π)) & β’ (π β πΊ β (π RingHom π)) β β’ (π β (πΊ(β¨π, πβ© Β· π)πΉ) = (πΊ β πΉ)) | ||
Theorem | ringccatidALTV 46099* | Lemma for ringccatALTV 46100. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RingCatALTVβπ) & β’ π΅ = (BaseβπΆ) β β’ (π β π β (πΆ β Cat β§ (IdβπΆ) = (π₯ β π΅ β¦ ( I βΎ (Baseβπ₯))))) | ||
Theorem | ringccatALTV 46100 | The category of rings is a category. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RingCatALTVβπ) β β’ (π β π β πΆ β Cat) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |