![]() |
Metamath
Proof Explorer Theorem List (p. 206 of 484) | < 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: | ![]() (1-30748) |
![]() (30749-32271) |
![]() (32272-48316) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | subrngmcl 20501 | A subgroup is closed under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.) Generalization of subrgmcl 20530. (Revised by AV, 14-Feb-2025.) |
⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝐴 ∈ (SubRng‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 · 𝑌) ∈ 𝐴) | ||
Theorem | issubrng2 20502* | Characterize the subrings of a ring by closure properties. (Contributed by AV, 15-Feb-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ Rng → (𝐴 ∈ (SubRng‘𝑅) ↔ (𝐴 ∈ (SubGrp‘𝑅) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴))) | ||
Theorem | opprsubrng 20503 | Being a subring is a symmetric property. (Contributed by AV, 15-Feb-2025.) |
⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (SubRng‘𝑅) = (SubRng‘𝑂) | ||
Theorem | subrngint 20504 | The intersection of a nonempty collection of subrings is a subring. (Contributed by AV, 15-Feb-2025.) |
⊢ ((𝑆 ⊆ (SubRng‘𝑅) ∧ 𝑆 ≠ ∅) → ∩ 𝑆 ∈ (SubRng‘𝑅)) | ||
Theorem | subrngin 20505 | The intersection of two subrings is a subring. (Contributed by AV, 15-Feb-2025.) |
⊢ ((𝐴 ∈ (SubRng‘𝑅) ∧ 𝐵 ∈ (SubRng‘𝑅)) → (𝐴 ∩ 𝐵) ∈ (SubRng‘𝑅)) | ||
Theorem | subrngmre 20506 | The subrings of a non-unital ring are a Moore system. (Contributed by AV, 15-Feb-2025.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Rng → (SubRng‘𝑅) ∈ (Moore‘𝐵)) | ||
Theorem | subsubrng 20507 | A subring of a subring is a subring. (Contributed by AV, 15-Feb-2025.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) ⇒ ⊢ (𝐴 ∈ (SubRng‘𝑅) → (𝐵 ∈ (SubRng‘𝑆) ↔ (𝐵 ∈ (SubRng‘𝑅) ∧ 𝐵 ⊆ 𝐴))) | ||
Theorem | subsubrng2 20508 | The set of subrings of a subring are the smaller subrings. (Contributed by AV, 15-Feb-2025.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) ⇒ ⊢ (𝐴 ∈ (SubRng‘𝑅) → (SubRng‘𝑆) = ((SubRng‘𝑅) ∩ 𝒫 𝐴)) | ||
Theorem | rhmimasubrnglem 20509* | Lemma for rhmimasubrng 20510: Modified part of mhmima 18784. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 16-Feb-2025.) |
⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (SubRng‘𝑅)) → ∀𝑥 ∈ (𝐹 “ 𝑋)∀𝑦 ∈ (𝐹 “ 𝑋)(𝑥(+g‘𝑁)𝑦) ∈ (𝐹 “ 𝑋)) | ||
Theorem | rhmimasubrng 20510 | The homomorphic image of a subring is a subring. (Contributed by AV, 16-Feb-2025.) |
⊢ ((𝐹 ∈ (𝑀 RingHom 𝑁) ∧ 𝑋 ∈ (SubRng‘𝑀)) → (𝐹 “ 𝑋) ∈ (SubRng‘𝑁)) | ||
Theorem | cntzsubrng 20511 | Centralizers in a non-unital ring are subrings. (Contributed by AV, 17-Feb-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ ((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubRng‘𝑅)) | ||
Theorem | subrngpropd 20512* | If two structures have the same ring components (properties), they have the same set of subrings. (Contributed by AV, 17-Feb-2025.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (SubRng‘𝐾) = (SubRng‘𝐿)) | ||
Syntax | csubrg 20513 | Extend class notation with all subrings of a ring. |
class SubRing | ||
Syntax | crgspn 20514 | Extend class notation with span of a set of elements over a ring. |
class RingSpan | ||
Definition | df-subrg 20515* |
Define a subring of a ring as a set of elements that is a ring in its
own right and contains the multiplicative identity.
The additional constraint is necessary because the multiplicative identity of a ring, unlike the additive identity of a ring/group or the multiplicative identity of a field, cannot be identified by a local property. Thus, it is possible for a subset of a ring to be a ring while not containing the true identity if it contains a false identity. For instance, the subset (ℤ × {0}) of (ℤ × ℤ) (where multiplication is componentwise) contains the false identity 〈1, 0〉 which preserves every element of the subset and thus appears to be the identity of the subset, but is not the identity of the larger ring. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ SubRing = (𝑤 ∈ Ring ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ ((𝑤 ↾s 𝑠) ∈ Ring ∧ (1r‘𝑤) ∈ 𝑠)}) | ||
Definition | df-rgspn 20516* | The ring-span of a set of elements in a ring is the smallest subring which contains all of them. (Contributed by Stefan O'Rear, 7-Dec-2014.) |
⊢ RingSpan = (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ (SubRing‘𝑤) ∣ 𝑠 ⊆ 𝑡})) | ||
Theorem | issubrg 20517 | The subring predicate. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Proof shortened by AV, 12-Oct-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) ↔ ((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴))) | ||
Theorem | subrgss 20518 | A subring is a subset. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ 𝐵) | ||
Theorem | subrgid 20519 | Every ring is a subring of itself. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐵 ∈ (SubRing‘𝑅)) | ||
Theorem | subrgring 20520 | A subring is a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑆 ∈ Ring) | ||
Theorem | subrgcrng 20521 | A subring of a commutative ring is a commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝐴 ∈ (SubRing‘𝑅)) → 𝑆 ∈ CRing) | ||
Theorem | subrgrcl 20522 | Reverse closure for a subring predicate. (Contributed by Mario Carneiro, 3-Dec-2014.) |
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring) | ||
Theorem | subrgsubg 20523 | A subring is a subgroup. (Contributed by Mario Carneiro, 3-Dec-2014.) |
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅)) | ||
Theorem | subrgsubrng 20524 | A subring of a unital ring is a subring of a non-unital ring. (Contributed by AV, 30-Mar-2025.) |
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubRng‘𝑅)) | ||
Theorem | subrg0 20525 | A subring always has the same additive identity. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 0 = (0g‘𝑆)) | ||
Theorem | subrg1cl 20526 | A subring contains the multiplicative identity. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 1 ∈ 𝐴) | ||
Theorem | subrgbas 20527 | Base set of a subring structure. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 = (Base‘𝑆)) | ||
Theorem | subrg1 20528 | A subring always has the same multiplicative identity. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 1 = (1r‘𝑆)) | ||
Theorem | subrgacl 20529 | A subring is closed under addition. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ + = (+g‘𝑅) ⇒ ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 + 𝑌) ∈ 𝐴) | ||
Theorem | subrgmcl 20530 | A subgroup is closed under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.) (Proof shortened by AV, 30-Mar-2025.) |
⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 · 𝑌) ∈ 𝐴) | ||
Theorem | subrgsubm 20531 | A subring is a submonoid of the multiplicative monoid. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubMnd‘𝑀)) | ||
Theorem | subrgdvds 20532 | If an element divides another in a subring, then it also divides the other in the parent ring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ ∥ = (∥r‘𝑅) & ⊢ 𝐸 = (∥r‘𝑆) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐸 ⊆ ∥ ) | ||
Theorem | subrguss 20533 | A unit of a subring is a unit of the parent ring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑉 = (Unit‘𝑆) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑉 ⊆ 𝑈) | ||
Theorem | subrginv 20534 | A subring always has the same inversion function, for elements that are invertible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ 𝑈 = (Unit‘𝑆) & ⊢ 𝐽 = (invr‘𝑆) ⇒ ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (𝐼‘𝑋) = (𝐽‘𝑋)) | ||
Theorem | subrgdv 20535 | A subring always has the same division function, for elements that are invertible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ / = (/r‘𝑅) & ⊢ 𝑈 = (Unit‘𝑆) & ⊢ 𝐸 = (/r‘𝑆) ⇒ ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → (𝑋 / 𝑌) = (𝑋𝐸𝑌)) | ||
Theorem | subrgunit 20536 | An element of a ring is a unit of a subring iff it is a unit of the parent ring and both it and its inverse are in the subring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑉 = (Unit‘𝑆) & ⊢ 𝐼 = (invr‘𝑅) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑋 ∈ 𝑉 ↔ (𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ (𝐼‘𝑋) ∈ 𝐴))) | ||
Theorem | subrgugrp 20537 | The units of a subring form a subgroup of the unit group of the original ring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑉 = (Unit‘𝑆) & ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑉 ∈ (SubGrp‘𝐺)) | ||
Theorem | issubrg2 20538* | Characterize the subrings of a ring by closure properties. (Contributed by Mario Carneiro, 3-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐴 ∈ (SubRing‘𝑅) ↔ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴))) | ||
Theorem | opprsubrg 20539 | Being a subring is a symmetric property. (Contributed by Mario Carneiro, 6-Dec-2014.) |
⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (SubRing‘𝑅) = (SubRing‘𝑂) | ||
Theorem | subrgnzr 20540 | A subring of a nonzero ring is nonzero. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) ⇒ ⊢ ((𝑅 ∈ NzRing ∧ 𝐴 ∈ (SubRing‘𝑅)) → 𝑆 ∈ NzRing) | ||
Theorem | subrgint 20541 | The intersection of a nonempty collection of subrings is a subring. (Contributed by Stefan O'Rear, 30-Nov-2014.) (Revised by Mario Carneiro, 7-Dec-2014.) |
⊢ ((𝑆 ⊆ (SubRing‘𝑅) ∧ 𝑆 ≠ ∅) → ∩ 𝑆 ∈ (SubRing‘𝑅)) | ||
Theorem | subrgin 20542 | The intersection of two subrings is a subring. (Contributed by Stefan O'Rear, 30-Nov-2014.) (Revised by Mario Carneiro, 7-Dec-2014.) |
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐵 ∈ (SubRing‘𝑅)) → (𝐴 ∩ 𝐵) ∈ (SubRing‘𝑅)) | ||
Theorem | subrgmre 20543 | The subrings of a ring are a Moore system. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (SubRing‘𝑅) ∈ (Moore‘𝐵)) | ||
Theorem | subsubrg 20544 | A subring of a subring is a subring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝐵 ∈ (SubRing‘𝑆) ↔ (𝐵 ∈ (SubRing‘𝑅) ∧ 𝐵 ⊆ 𝐴))) | ||
Theorem | subsubrg2 20545 | The set of subrings of a subring are the smaller subrings. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → (SubRing‘𝑆) = ((SubRing‘𝑅) ∩ 𝒫 𝐴)) | ||
Theorem | issubrg3 20546 | A subring is an additive subgroup which is also a multiplicative submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝑆 ∈ (SubRing‘𝑅) ↔ (𝑆 ∈ (SubGrp‘𝑅) ∧ 𝑆 ∈ (SubMnd‘𝑀)))) | ||
Theorem | resrhm 20547 | Restriction of a ring homomorphism to a subring is a homomorphism. (Contributed by Mario Carneiro, 12-Mar-2015.) |
⊢ 𝑈 = (𝑆 ↾s 𝑋) ⇒ ⊢ ((𝐹 ∈ (𝑆 RingHom 𝑇) ∧ 𝑋 ∈ (SubRing‘𝑆)) → (𝐹 ↾ 𝑋) ∈ (𝑈 RingHom 𝑇)) | ||
Theorem | resrhm2b 20548 | Restriction of the codomain of a (ring) homomorphism. resghm2b 19195 analog. (Contributed by SN, 7-Feb-2025.) |
⊢ 𝑈 = (𝑇 ↾s 𝑋) ⇒ ⊢ ((𝑋 ∈ (SubRing‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) → (𝐹 ∈ (𝑆 RingHom 𝑇) ↔ 𝐹 ∈ (𝑆 RingHom 𝑈))) | ||
Theorem | rhmeql 20549 | The equalizer of two ring homomorphisms is a subring. (Contributed by Stefan O'Rear, 7-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ ((𝐹 ∈ (𝑆 RingHom 𝑇) ∧ 𝐺 ∈ (𝑆 RingHom 𝑇)) → dom (𝐹 ∩ 𝐺) ∈ (SubRing‘𝑆)) | ||
Theorem | rhmima 20550 | The homomorphic image of a subring is a subring. (Contributed by Stefan O'Rear, 10-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ ((𝐹 ∈ (𝑀 RingHom 𝑁) ∧ 𝑋 ∈ (SubRing‘𝑀)) → (𝐹 “ 𝑋) ∈ (SubRing‘𝑁)) | ||
Theorem | rnrhmsubrg 20551 | The range of a ring homomorphism is a subring. (Contributed by SN, 18-Nov-2023.) |
⊢ (𝐹 ∈ (𝑀 RingHom 𝑁) → ran 𝐹 ∈ (SubRing‘𝑁)) | ||
Theorem | cntzsubr 20552 | Centralizers in a ring are subrings. (Contributed by Stefan O'Rear, 6-Sep-2015.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubRing‘𝑅)) | ||
Theorem | pwsdiagrhm 20553* | Diagonal homomorphism into a structure power (Rings). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥})) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊) → 𝐹 ∈ (𝑅 RingHom 𝑌)) | ||
Theorem | subrgpropd 20554* | If two structures have the same group components (properties), they have the same set of subrings. (Contributed by Mario Carneiro, 9-Feb-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (SubRing‘𝐾) = (SubRing‘𝐿)) | ||
Theorem | rhmpropd 20555* | Ring homomorphism depends only on the ring attributes of structures. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐽)) & ⊢ (𝜑 → 𝐶 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → 𝐶 = (Base‘𝑀)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐽)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝑀)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐽)𝑦) = (𝑥(.r‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝑀)𝑦)) ⇒ ⊢ (𝜑 → (𝐽 RingHom 𝐾) = (𝐿 RingHom 𝑀)) | ||
The "category of non-unital rings" RngCat is the category of all non-unital rings Rng in a universe and non-unital ring homomorphisms RngHom 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 20557. 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 dfrngc2 20568. 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 20561, and the morphisms/arrows are the non-unital ring homomorphisms restricted to this subset of the non-unital rings ( RngHom ↾ (𝐵 × 𝐵)), see rngchomfval 20562, whereas the composition is the ordinary composition of functions, see rngccofval 20566 and rngcco 20567. 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 20570, 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 20573. It follows that the category of non-unital rings RngCat is actually a category, see rngccat 20574 with the identity function as identity arrow, see rngcid 20575. | ||
Syntax | crngc 20556 | Extend class notation to include the category Rng. |
class RngCat | ||
Definition | df-rngc 20557 | 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 ( RngHom ↾ ((𝑢 ∩ Rng) × (𝑢 ∩ Rng))))) | ||
Theorem | rngcval 20558 | 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)) & ⊢ (𝜑 → 𝐻 = ( RngHom ↾ (𝐵 × 𝐵))) ⇒ ⊢ (𝜑 → 𝐶 = ((ExtStrCat‘𝑈) ↾cat 𝐻)) | ||
Theorem | rnghmresfn 20559 | The class of non-unital ring homomorphisms restricted to subsets of non-unital rings is a function. (Contributed by AV, 4-Mar-2020.) |
⊢ (𝜑 → 𝐵 = (𝑈 ∩ Rng)) & ⊢ (𝜑 → 𝐻 = ( RngHom ↾ (𝐵 × 𝐵))) ⇒ ⊢ (𝜑 → 𝐻 Fn (𝐵 × 𝐵)) | ||
Theorem | rnghmresel 20560 | 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.) |
⊢ (𝜑 → 𝐻 = ( RngHom ↾ (𝐵 × 𝐵))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝐹 ∈ (𝑋𝐻𝑌)) → 𝐹 ∈ (𝑋 RngHom 𝑌)) | ||
Theorem | rngcbas 20561 | 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 20562 | 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 ‘𝐶) ⇒ ⊢ (𝜑 → 𝐻 = ( RngHom ↾ (𝐵 × 𝐵))) | ||
Theorem | rngchom 20563 | Set of arrows of the category of non-unital rings (in a universe). (Contributed by AV, 27-Feb-2020.) |
⊢ 𝐶 = (RngCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐻𝑌) = (𝑋 RngHom 𝑌)) | ||
Theorem | elrngchom 20564 | A morphism of non-unital rings is a function. (Contributed by AV, 27-Feb-2020.) |
⊢ 𝐶 = (RngCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) → 𝐹:(Base‘𝑋)⟶(Base‘𝑌))) | ||
Theorem | rngchomfeqhom 20565 | 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 20566 | 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 20567 | 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 20568 | Alternate definition of the category of non-unital rings (in a universe). (Contributed by AV, 16-Mar-2020.) |
⊢ 𝐶 = (RngCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Rng)) & ⊢ (𝜑 → 𝐻 = ( RngHom ↾ (𝐵 × 𝐵))) & ⊢ (𝜑 → · = (comp‘(ExtStrCat‘𝑈))) ⇒ ⊢ (𝜑 → 𝐶 = {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx), · 〉}) | ||
Theorem | rnghmsscmap2 20569* | 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 ∩ 𝑈)) ⇒ ⊢ (𝜑 → ( RngHom ↾ (𝑅 × 𝑅)) ⊆cat (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑅 ↦ ((Base‘𝑦) ↑m (Base‘𝑥)))) | ||
Theorem | rnghmsscmap 20570* | 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 ∩ 𝑈)) ⇒ ⊢ (𝜑 → ( RngHom ↾ (𝑅 × 𝑅)) ⊆cat (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑m (Base‘𝑥)))) | ||
Theorem | rnghmsubcsetclem1 20571 | Lemma 1 for rnghmsubcsetc 20573. (Contributed by AV, 9-Mar-2020.) |
⊢ 𝐶 = (ExtStrCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 = (Rng ∩ 𝑈)) & ⊢ (𝜑 → 𝐻 = ( RngHom ↾ (𝐵 × 𝐵))) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐻𝑥)) | ||
Theorem | rnghmsubcsetclem2 20572* | Lemma 2 for rnghmsubcsetc 20573. (Contributed by AV, 9-Mar-2020.) |
⊢ 𝐶 = (ExtStrCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 = (Rng ∩ 𝑈)) & ⊢ (𝜑 → 𝐻 = ( RngHom ↾ (𝐵 × 𝐵))) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐻𝑧)) | ||
Theorem | rnghmsubcsetc 20573 | 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 ∩ 𝑈)) & ⊢ (𝜑 → 𝐻 = ( RngHom ↾ (𝐵 × 𝐵))) ⇒ ⊢ (𝜑 → 𝐻 ∈ (Subcat‘𝐶)) | ||
Theorem | rngccat 20574 | 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 20575 | 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 20576 | A section in the category of non-unital rings, written out. (Contributed by AV, 28-Feb-2020.) |
⊢ 𝐶 = (RngCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐸 = (Base‘𝑋) & ⊢ 𝑆 = (Sect‘𝐶) ⇒ ⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ (𝐹 ∈ (𝑋 RngHom 𝑌) ∧ 𝐺 ∈ (𝑌 RngHom 𝑋) ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐸)))) | ||
Theorem | rngcinv 20577 | An inverse in the category of non-unital rings is the converse operation. (Contributed by AV, 28-Feb-2020.) |
⊢ 𝐶 = (RngCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑁 = (Inv‘𝐶) ⇒ ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹 ∈ (𝑋 RngIso 𝑌) ∧ 𝐺 = ◡𝐹))) | ||
Theorem | rngciso 20578 | An isomorphism in the category of non-unital rings is a bijection. (Contributed by AV, 28-Feb-2020.) |
⊢ 𝐶 = (RngCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐼 = (Iso‘𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ 𝐹 ∈ (𝑋 RngIso 𝑌))) | ||
Theorem | rngcifuestrc 20579* | 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 ↾ (𝑥 RngHom 𝑦)))) ⇒ ⊢ (𝜑 → 𝐹(𝑅 Func 𝐸)𝐺) | ||
Theorem | funcrngcsetc 20580* | 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 20581, using cofuval2 17880 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 20579, and the "natural forgetful functor" from the category of extensible structures into the category of sets, see funcestrcsetc 18147. (Contributed by AV, 26-Mar-2020.) |
⊢ 𝑅 = (RngCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RngHom 𝑦)))) ⇒ ⊢ (𝜑 → 𝐹(𝑅 Func 𝑆)𝐺) | ||
Theorem | funcrngcsetcALT 20581* | Alternate proof of funcrngcsetc 20580, using cofuval2 17880 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 20579, and the "natural forgetful functor" from the category of extensible structures into the category of sets, see funcestrcsetc 18147. Surprisingly, this proof is longer than the direct proof given in funcrngcsetc 20580. (Contributed by AV, 30-Mar-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑅 = (RngCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RngHom 𝑦)))) ⇒ ⊢ (𝜑 → 𝐹(𝑅 Func 𝑆)𝐺) | ||
Theorem | zrinitorngc 20582 | 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 20583 | 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 20584 | 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 20586. 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 20597. 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 20590, and the morphisms/arrows are the ring homomorphisms restricted to this subset of the rings ( RingHom ↾ (𝐵 × 𝐵)), see ringchomfval 20591, whereas the composition is the ordinary composition of functions, see ringccofval 20595 and ringcco 20596. By showing that the ring homomorphisms between rings are a subcategory subset (⊆cat) of the mappings between base sets of extensible structures, see rhmsscmap 20599, it can be shown that the ring homomorphisms between rings are a subcategory (Subcat) of the category of extensible structures, see rhmsubcsetc 20602. It follows that the category of rings RingCat is actually a category, see ringccat 20603 with the identity function as identity arrow, see ringcid 20604. 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 20605, and that the ring homomorphisms between rings are a subcategory of the category of non-unital rings, see rhmsubcrngc 20608. 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 20609: ((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 20614. | ||
Syntax | cringc 20585 | Extend class notation to include the category Ring. |
class RingCat | ||
Definition | df-ringc 20586 | 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))))) | ||
Theorem | ringcval 20587 | 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 20588 | 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 20589 | 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 20590 | 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 20591 | 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 20592 | Set of arrows of the category of unital rings (in a universe). (Contributed by AV, 14-Feb-2020.) |
⊢ 𝐶 = (RingCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐻𝑌) = (𝑋 RingHom 𝑌)) | ||
Theorem | elringchom 20593 | A morphism of unital rings is a function. (Contributed by AV, 14-Feb-2020.) |
⊢ 𝐶 = (RingCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) → 𝐹:(Base‘𝑋)⟶(Base‘𝑌))) | ||
Theorem | ringchomfeqhom 20594 | 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 20595 | 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 20596 | 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 20597 | 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 20598* | 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 20599* | 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 20600 | Lemma 1 for rhmsubcsetc 20602. (Contributed by AV, 9-Mar-2020.) |
⊢ 𝐶 = (ExtStrCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 = (Ring ∩ 𝑈)) & ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵))) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐻𝑥)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |