Home | Metamath
Proof Explorer Theorem List (p. 443 of 450) | < 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-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44926) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | c0mhm 44201* | The constant mapping to zero is a monoid homomorphism. (Contributed by AV, 16-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑇) & ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 ) ⇒ ⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) → 𝐻 ∈ (𝑆 MndHom 𝑇)) | ||
Theorem | c0ghm 44202* | The constant mapping to zero is a group homomorphism. (Contributed by AV, 16-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑇) & ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 ) ⇒ ⊢ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → 𝐻 ∈ (𝑆 GrpHom 𝑇)) | ||
Theorem | c0rhm 44203* | The constant mapping to zero is a ring homomorphism from any ring to the zero ring. (Contributed by AV, 17-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑇) & ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 ) ⇒ ⊢ ((𝑆 ∈ Ring ∧ 𝑇 ∈ (Ring ∖ NzRing)) → 𝐻 ∈ (𝑆 RingHom 𝑇)) | ||
Theorem | c0rnghm 44204* | The constant mapping to zero is a nonunital ring homomorphism from any nonunital ring to the zero ring. (Contributed by AV, 17-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑇) & ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 ) ⇒ ⊢ ((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing)) → 𝐻 ∈ (𝑆 RngHomo 𝑇)) | ||
Theorem | c0snmgmhm 44205* | The constant mapping to zero is a magma homomorphism from a magma with one element to any monoid. (Contributed by AV, 17-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑇) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 ) ⇒ ⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ∧ (♯‘𝐵) = 1) → 𝐻 ∈ (𝑇 MgmHom 𝑆)) | ||
Theorem | c0snmhm 44206* | The constant mapping to zero is a monoid homomorphism from the trivial monoid (consisting of the zero only) to any monoid. (Contributed by AV, 17-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑇) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 ) & ⊢ 𝑍 = (0g‘𝑇) ⇒ ⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ∧ 𝐵 = {𝑍}) → 𝐻 ∈ (𝑇 MndHom 𝑆)) | ||
Theorem | c0snghm 44207* | The constant mapping to zero is a group homomorphism from the trivial group (consisting of the zero only) to any group. (Contributed by AV, 17-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑇) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 ) & ⊢ 𝑍 = (0g‘𝑇) ⇒ ⊢ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ∧ 𝐵 = {𝑍}) → 𝐻 ∈ (𝑇 GrpHom 𝑆)) | ||
Theorem | zrrnghm 44208* | The constant mapping to zero is a nonunital ring homomorphism from the zero ring to any nonunital ring. (Contributed by AV, 17-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑇) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 ) ⇒ ⊢ ((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing)) → 𝐻 ∈ (𝑇 RngHomo 𝑆)) | ||
Theorem | rhmfn 44209 | The mapping of two rings to the ring homomorphisms between them is a function. (Contributed by AV, 1-Mar-2020.) |
⊢ RingHom Fn (Ring × Ring) | ||
Theorem | rhmval 44210 | The ring homomorphisms between two rings. (Contributed by AV, 1-Mar-2020.) |
⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ Ring) → (𝑅 RingHom 𝑆) = ((𝑅 GrpHom 𝑆) ∩ ((mulGrp‘𝑅) MndHom (mulGrp‘𝑆)))) | ||
Theorem | rhmisrnghm 44211 | Each unital ring homomorphism is a non-unital ring homomorphism. (Contributed by AV, 29-Feb-2020.) |
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 RngHomo 𝑆)) | ||
Theorem | lidldomn1 44212* | If a (left) ideal (which is not the zero ideal) of a domain has a multiplicative identity element, the identity element is the identity of the domain. (Contributed by AV, 17-Feb-2020.) |
⊢ 𝐿 = (LIdeal‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) → (∀𝑥 ∈ 𝑈 ((𝐼 · 𝑥) = 𝑥 ∧ (𝑥 · 𝐼) = 𝑥) → 𝐼 = 1 )) | ||
Theorem | lidlssbas 44213 | The base set of the restriction of the ring to a (left) ideal is a subset of the base set of the ring. (Contributed by AV, 17-Feb-2020.) |
⊢ 𝐿 = (LIdeal‘𝑅) & ⊢ 𝐼 = (𝑅 ↾s 𝑈) ⇒ ⊢ (𝑈 ∈ 𝐿 → (Base‘𝐼) ⊆ (Base‘𝑅)) | ||
Theorem | lidlbas 44214 | A (left) ideal of a ring is the base set of the restriction of the ring to this ideal. (Contributed by AV, 17-Feb-2020.) |
⊢ 𝐿 = (LIdeal‘𝑅) & ⊢ 𝐼 = (𝑅 ↾s 𝑈) ⇒ ⊢ (𝑈 ∈ 𝐿 → (Base‘𝐼) = 𝑈) | ||
Theorem | lidlabl 44215 | A (left) ideal of a ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020.) |
⊢ 𝐿 = (LIdeal‘𝑅) & ⊢ 𝐼 = (𝑅 ↾s 𝑈) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → 𝐼 ∈ Abel) | ||
Theorem | lidlmmgm 44216 | The multiplicative group of a (left) ideal of a ring is a magma. (Contributed by AV, 17-Feb-2020.) |
⊢ 𝐿 = (LIdeal‘𝑅) & ⊢ 𝐼 = (𝑅 ↾s 𝑈) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → (mulGrp‘𝐼) ∈ Mgm) | ||
Theorem | lidlmsgrp 44217 | The multiplicative group of a (left) ideal of a ring is a semigroup. (Contributed by AV, 17-Feb-2020.) |
⊢ 𝐿 = (LIdeal‘𝑅) & ⊢ 𝐼 = (𝑅 ↾s 𝑈) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → (mulGrp‘𝐼) ∈ Smgrp) | ||
Theorem | lidlrng 44218 | A (left) ideal of a ring is a non-unital ring. (Contributed by AV, 17-Feb-2020.) |
⊢ 𝐿 = (LIdeal‘𝑅) & ⊢ 𝐼 = (𝑅 ↾s 𝑈) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → 𝐼 ∈ Rng) | ||
Theorem | zlidlring 44219 | The zero (left) ideal of a non-unital ring is a unital ring (the zero ring). (Contributed by AV, 16-Feb-2020.) |
⊢ 𝐿 = (LIdeal‘𝑅) & ⊢ 𝐼 = (𝑅 ↾s 𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → 𝐼 ∈ Ring) | ||
Theorem | uzlidlring 44220 | Only the zero (left) ideal or the unit (left) ideal of a domain is a unital ring. (Contributed by AV, 18-Feb-2020.) |
⊢ 𝐿 = (LIdeal‘𝑅) & ⊢ 𝐼 = (𝑅 ↾s 𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿) → (𝐼 ∈ Ring ↔ (𝑈 = { 0 } ∨ 𝑈 = 𝐵))) | ||
Theorem | lidldomnnring 44221 | A (left) ideal of a domain which is neither the zero ideal nor the unit ideal is not a unital ring. (Contributed by AV, 18-Feb-2020.) |
⊢ 𝐿 = (LIdeal‘𝑅) & ⊢ 𝐼 = (𝑅 ↾s 𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ∧ 𝑈 ≠ 𝐵)) → 𝐼 ∉ Ring) | ||
Theorem | 0even 44222* | 0 is an even integer. (Contributed by AV, 11-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} ⇒ ⊢ 0 ∈ 𝐸 | ||
Theorem | 1neven 44223* | 1 is not an even integer. (Contributed by AV, 12-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} ⇒ ⊢ 1 ∉ 𝐸 | ||
Theorem | 2even 44224* | 2 is an even integer. (Contributed by AV, 12-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} ⇒ ⊢ 2 ∈ 𝐸 | ||
Theorem | 2zlidl 44225* | The even integers are a (left) ideal of the ring of integers. (Contributed by AV, 20-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑈 = (LIdeal‘ℤring) ⇒ ⊢ 𝐸 ∈ 𝑈 | ||
Theorem | 2zrng 44226* | The ring of integers restricted to the even integers is a (non-unital) ring, the "ring of even integers". Remark: the structure of the complementary subset of the set of integers, the odd integers, is not even a magma, see oddinmgm 44102. (Contributed by AV, 20-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑈 = (LIdeal‘ℤring) & ⊢ 𝑅 = (ℤring ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ Rng | ||
Theorem | 2zrngbas 44227* | The base set of R is the set of all even integers. (Contributed by AV, 31-Jan-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝐸 = (Base‘𝑅) | ||
Theorem | 2zrngadd 44228* | The group addition operation of R is the addition of complex numbers. (Contributed by AV, 31-Jan-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ + = (+g‘𝑅) | ||
Theorem | 2zrng0 44229* | The additive identity of R is the complex number 0. (Contributed by AV, 11-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 0 = (0g‘𝑅) | ||
Theorem | 2zrngamgm 44230* | R is an (additive) magma. (Contributed by AV, 6-Jan-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ Mgm | ||
Theorem | 2zrngasgrp 44231* | R is an (additive) semigroup. (Contributed by AV, 4-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ Smgrp | ||
Theorem | 2zrngamnd 44232* | R is an (additive) monoid. (Contributed by AV, 11-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ Mnd | ||
Theorem | 2zrngacmnd 44233* | R is a commutative (additive) monoid. (Contributed by AV, 11-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ CMnd | ||
Theorem | 2zrngagrp 44234* | R is an (additive) group. (Contributed by AV, 6-Jan-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ Grp | ||
Theorem | 2zrngaabl 44235* | R is an (additive) abelian group. (Contributed by AV, 11-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ Abel | ||
Theorem | 2zrngmul 44236* | The ring multiplication operation of R is the multiplication on complex numbers. (Contributed by AV, 31-Jan-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ · = (.r‘𝑅) | ||
Theorem | 2zrngmmgm 44237* | R is a (multiplicative) magma. (Contributed by AV, 11-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ 𝑀 ∈ Mgm | ||
Theorem | 2zrngmsgrp 44238* | R is a (multiplicative) semigroup. (Contributed by AV, 4-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ 𝑀 ∈ Smgrp | ||
Theorem | 2zrngALT 44239* | The ring of integers restricted to the even integers is a (non-unital) ring, the "ring of even integers". Alternate version of 2zrng 44226, based on a restriction of the field of the complex numbers. The proof is based on the facts that the ring of even integers is an additive abelian group (see 2zrngaabl 44235) and a multiplicative semigroup (see 2zrngmsgrp 44238). (Contributed by AV, 11-Feb-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ 𝑅 ∈ Rng | ||
Theorem | 2zrngnmlid 44240* | R has no multiplicative (left) identity. (Contributed by AV, 12-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ ∀𝑏 ∈ 𝐸 ∃𝑎 ∈ 𝐸 (𝑏 · 𝑎) ≠ 𝑎 | ||
Theorem | 2zrngnmrid 44241* | R has no multiplicative (right) identity. (Contributed by AV, 12-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ ∀𝑎 ∈ (𝐸 ∖ {0})∀𝑏 ∈ 𝐸 (𝑎 · 𝑏) ≠ 𝑎 | ||
Theorem | 2zrngnmlid2 44242* | R has no multiplicative (left) identity. (Contributed by AV, 12-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ ∀𝑎 ∈ (𝐸 ∖ {0})∀𝑏 ∈ 𝐸 (𝑏 · 𝑎) ≠ 𝑎 | ||
Theorem | 2zrngnring 44243* | R is not a unital ring. (Contributed by AV, 6-Jan-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ 𝑅 ∉ Ring | ||
Theorem | cznrnglem 44244 | Lemma for cznrng 44246: The base set of the ring constructed from a ℤ/nℤ structure by replacing the (multiplicative) ring operation by a constant operation is the base set of the ℤ/nℤ structure. (Contributed by AV, 16-Feb-2020.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑋 = (𝑌 sSet 〈(.r‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)〉) ⇒ ⊢ 𝐵 = (Base‘𝑋) | ||
Theorem | cznabel 44245 | 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 44246* | 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 44247* | 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 44250. 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 44251 or dfrngc2 44263. 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 44256, and the morphisms/arrows are the non-unital ring homomorphisms restricted to this subset of the non-unital rings ( RngHomo ↾ (𝐵 × 𝐵)), see rngchomfval 44257, whereas the composition is the ordinary composition of functions, see rngccofval 44261 and rngcco 44262. 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 44265, 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 44268. It follows that the category of non-unital rings RngCat is actually a category, see rngccat 44269 with the identity function as identity arrow, see rngcid 44270. | ||
Syntax | crngc 44248 | Extend class notation to include the category Rng. |
class RngCat | ||
Syntax | crngcALTV 44249 | Extend class notation to include the category Rng. (New usage is discouraged.) |
class RngCatALTV | ||
Definition | df-rngc 44250 | 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 44251* | 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 44252* | 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 44253 | 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 44254 | 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 44255 | 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 44256 | 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 44257 | 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 44258 | 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 44259 | A morphism of non-unital rings is a function. (Contributed by AV, 27-Feb-2020.) |
⊢ 𝐶 = (RngCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) → 𝐹:(Base‘𝑋)⟶(Base‘𝑌))) | ||
Theorem | rngchomfeqhom 44260 | 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 44261 | 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 44262 | 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 44263 | 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 44264* | 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 44265* | 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 44266 | Lemma 1 for rnghmsubcsetc 44268. (Contributed by AV, 9-Mar-2020.) |
⊢ 𝐶 = (ExtStrCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 = (Rng ∩ 𝑈)) & ⊢ (𝜑 → 𝐻 = ( RngHomo ↾ (𝐵 × 𝐵))) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐻𝑥)) | ||
Theorem | rnghmsubcsetclem2 44267* | Lemma 2 for rnghmsubcsetc 44268. (Contributed by AV, 9-Mar-2020.) |
⊢ 𝐶 = (ExtStrCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 = (Rng ∩ 𝑈)) & ⊢ (𝜑 → 𝐻 = ( RngHomo ↾ (𝐵 × 𝐵))) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐻𝑧)) | ||
Theorem | rnghmsubcsetc 44268 | 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 44269 | 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 44270 | 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 44271 | 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 44272 | 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 44273 | An isomorphism in the category of non-unital rings is a bijection. (Contributed by AV, 28-Feb-2020.) |
⊢ 𝐶 = (RngCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐼 = (Iso‘𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ 𝐹 ∈ (𝑋 RngIsom 𝑌))) | ||
Theorem | rngcbasALTV 44274 | 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 44275* | 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 44276 | 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 44277 | 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 44278* | 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 44279 | 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 44280* | Lemma for rngccatALTV 44281. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.) |
⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝑈 ∈ 𝑉 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑥 ∈ 𝐵 ↦ ( I ↾ (Base‘𝑥))))) | ||
Theorem | rngccatALTV 44281 | The category of non-unital rings is a category. (Contributed by AV, 27-Feb-2020.) (New usage is discouraged.) |
⊢ 𝐶 = (RngCatALTV‘𝑈) ⇒ ⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat) | ||
Theorem | rngcidALTV 44282 | 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 44283 | 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 44284 | 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 44285 | 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 44286* | 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 44287 | 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 44288* | 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 44289* | 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 44290, using cofuval2 17157 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 44288, and the "natural forgetful functor" from the category of extensible structures into the category of sets, see funcestrcsetc 17399. (Contributed by AV, 26-Mar-2020.) |
⊢ 𝑅 = (RngCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RngHomo 𝑦)))) ⇒ ⊢ (𝜑 → 𝐹(𝑅 Func 𝑆)𝐺) | ||
Theorem | funcrngcsetcALT 44290* | Alternate proof of funcrngcsetc 44289, using cofuval2 17157 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 44288, and the "natural forgetful functor" from the category of extensible structures into the category of sets, see funcestrcsetc 17399. Surprisingly, this proof is longer than the direct proof given in funcrngcsetc 44289. (Contributed by AV, 30-Mar-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑅 = (RngCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RngHomo 𝑦)))) ⇒ ⊢ (𝜑 → 𝐹(𝑅 Func 𝑆)𝐺) | ||
Theorem | zrinitorngc 44291 | The zero ring is an initial object in the category of nonunital rings. (Contributed by AV, 18-Apr-2020.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RngCat‘𝑈) & ⊢ (𝜑 → 𝑍 ∈ (Ring ∖ NzRing)) & ⊢ (𝜑 → 𝑍 ∈ 𝑈) ⇒ ⊢ (𝜑 → 𝑍 ∈ (InitO‘𝐶)) | ||
Theorem | zrtermorngc 44292 | The zero ring is a terminal object in the category of nonunital rings. (Contributed by AV, 17-Apr-2020.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RngCat‘𝑈) & ⊢ (𝜑 → 𝑍 ∈ (Ring ∖ NzRing)) & ⊢ (𝜑 → 𝑍 ∈ 𝑈) ⇒ ⊢ (𝜑 → 𝑍 ∈ (TermO‘𝐶)) | ||
Theorem | zrzeroorngc 44293 | 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 44296. 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 44309. 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 44302, and the morphisms/arrows are the ring homomorphisms restricted to this subset of the rings ( RingHom ↾ (𝐵 × 𝐵)), see ringchomfval 44303, whereas the composition is the ordinary composition of functions, see ringccofval 44307 and ringcco 44308. By showing that the ring homomorphisms between rings are a subcategory subset (⊆cat) of the mappings between base sets of extensible structures, see rhmsscmap 44311, it can be shown that the ring homomorphisms between rings are a subcategory (Subcat) of the category of extensible structures, see rhmsubcsetc 44314. It follows that the category of rings RingCat is actually a category, see ringccat 44315 with the identity function as identity arrow, see ringcid 44316. 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 44317, and that the ring homomorphisms between rings are a subcategory of the category of non-unital rings, see rhmsubcrngc 44320. 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 44321: ((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 44326. | ||
Syntax | cringc 44294 | Extend class notation to include the category Ring. |
class RingCat | ||
Syntax | cringcALTV 44295 | Extend class notation to include the category Ring. (New usage is discouraged.) |
class RingCatALTV | ||
Definition | df-ringc 44296 | 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 44297* | 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 44298* | 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 44299 | 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 44300 | The class of unital ring homomorphisms restricted to subsets of unital rings is a function. (Contributed by AV, 10-Mar-2020.) |
⊢ (𝜑 → 𝐵 = (𝑈 ∩ Ring)) & ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵))) ⇒ ⊢ (𝜑 → 𝐻 Fn (𝐵 × 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |