doc-next-gen

Mathlib.Algebra.Ring.Prod

Module docstring

{"# Semiring, ring etc structures on R × S

In this file we define two-binop (Semiring, Ring etc) structures on R × S. We also prove trivial simp lemmas, and define the following operations on RingHoms and similarly for NonUnitalRingHoms:

  • fst R S : R × S →+* R, snd R S : R × S →+* S: projections Prod.fst and Prod.snd as RingHoms;
  • f.prod g : R →+* S × T: sends x to (f x, g x);
  • f.prod_map g : R × S → R' × S': Prod.map f g as a RingHom, sends (x, y) to (f x, g y). "}
Prod.instDistrib instance
[Distrib R] [Distrib S] : Distrib (R × S)
Full source 
/-- Product of two distributive types is distributive. -/
instance instDistrib [Distrib R] [Distrib S] : Distrib (R × S) where
  left_distrib _ _ _ := by ext <;> exact left_distrib ..
  right_distrib _ _ _ := by ext <;> exact right_distrib ..
Distributive Structure on Product Types
Informal description
For any two types $R$ and $S$ each equipped with a distributive structure, the product $R \times S$ is also a distributive structure, where addition and multiplication are defined componentwise.
Prod.instNonUnitalNonAssocSemiring instance
[NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] : NonUnitalNonAssocSemiring (R × S)
Full source 
/-- Product of two `NonUnitalNonAssocSemiring`s is a `NonUnitalNonAssocSemiring`. -/
instance instNonUnitalNonAssocSemiring [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] :
    NonUnitalNonAssocSemiring (R × S) :=
  { inferInstanceAs (AddCommMonoid (R × S)),
    inferInstanceAs (Distrib (R × S)),
    inferInstanceAs (MulZeroClass (R × S)) with }
Product of Non-Unital Non-Associative Semirings is a Non-Unital Non-Associative Semiring
Informal description
For any two types $R$ and $S$ each equipped with a non-unital non-associative semiring structure, the product $R \times S$ is also a non-unital non-associative semiring with pointwise addition and multiplication.
Prod.instNonUnitalSemiring instance
[NonUnitalSemiring R] [NonUnitalSemiring S] : NonUnitalSemiring (R × S)
Full source 
/-- Product of two `NonUnitalSemiring`s is a `NonUnitalSemiring`. -/
instance instNonUnitalSemiring [NonUnitalSemiring R] [NonUnitalSemiring S] :
    NonUnitalSemiring (R × S) :=
  { inferInstanceAs (NonUnitalNonAssocSemiring (R × S)),
    inferInstanceAs (SemigroupWithZero (R × S)) with }
Product of Non-Unital Semirings is a Non-Unital Semiring
Informal description
For any two non-unital semirings $R$ and $S$, the product $R \times S$ is also a non-unital semiring with pointwise addition and multiplication.
Prod.instNonAssocSemiring instance
[NonAssocSemiring R] [NonAssocSemiring S] : NonAssocSemiring (R × S)
Full source 
/-- Product of two `NonAssocSemiring`s is a `NonAssocSemiring`. -/
instance instNonAssocSemiring [NonAssocSemiring R] [NonAssocSemiring S] :
    NonAssocSemiring (R × S) :=
  { inferInstanceAs (NonUnitalNonAssocSemiring (R × S)),
    inferInstanceAs (MulZeroOneClass (R × S)),
    inferInstanceAs (AddMonoidWithOne (R × S)) with }
Product of Non-Associative Semirings is a Non-Associative Semiring
Informal description
For any two non-associative semirings $R$ and $S$, the product $R \times S$ is also a non-associative semiring with pointwise addition and multiplication.
Prod.instSemiring instance
[Semiring R] [Semiring S] : Semiring (R × S)
Full source 
/-- Product of two semirings is a semiring. -/
instance instSemiring [Semiring R] [Semiring S] : Semiring (R × S) :=
  { inferInstanceAs (NonUnitalSemiring (R × S)),
    inferInstanceAs (NonAssocSemiring (R × S)),
    inferInstanceAs (MonoidWithZero (R × S)) with }
Product of Semirings is a Semiring
Informal description
For any two semirings $R$ and $S$, the product $R \times S$ is also a semiring with pointwise addition and multiplication.
Prod.instNonUnitalCommSemiring instance
[NonUnitalCommSemiring R] [NonUnitalCommSemiring S] : NonUnitalCommSemiring (R × S)
Full source 
/-- Product of two `NonUnitalCommSemiring`s is a `NonUnitalCommSemiring`. -/
instance instNonUnitalCommSemiring [NonUnitalCommSemiring R] [NonUnitalCommSemiring S] :
    NonUnitalCommSemiring (R × S) :=
  { inferInstanceAs (NonUnitalSemiring (R × S)), inferInstanceAs (CommSemigroup (R × S)) with }
Product of Non-Unital Commutative Semirings is a Non-Unital Commutative Semiring
Informal description
For any two non-unital commutative semirings $R$ and $S$, the product $R \times S$ is also a non-unital commutative semiring with pointwise addition and multiplication.
Prod.instCommSemiring instance
[CommSemiring R] [CommSemiring S] : CommSemiring (R × S)
Full source 
/-- Product of two commutative semirings is a commutative semiring. -/
instance instCommSemiring [CommSemiring R] [CommSemiring S] : CommSemiring (R × S) :=
  { inferInstanceAs (Semiring (R × S)), inferInstanceAs (CommMonoid (R × S)) with }
Product of Commutative Semirings is a Commutative Semiring
Informal description
For any two commutative semirings $R$ and $S$, the product $R \times S$ is also a commutative semiring with pointwise addition and multiplication.
Prod.instNonUnitalNonAssocRing instance
[NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] : NonUnitalNonAssocRing (R × S)
Full source 
instance instNonUnitalNonAssocRing [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] :
    NonUnitalNonAssocRing (R × S) :=
  { inferInstanceAs (AddCommGroup (R × S)),
    inferInstanceAs (NonUnitalNonAssocSemiring (R × S)) with }
Product of Non-Unital Non-Associative Rings is a Non-Unital Non-Associative Ring
Informal description
For any two types $R$ and $S$ each equipped with a non-unital non-associative ring structure, the product $R \times S$ is also a non-unital non-associative ring with pointwise addition and multiplication.
Prod.instNonUnitalRing instance
[NonUnitalRing R] [NonUnitalRing S] : NonUnitalRing (R × S)
Full source 
instance instNonUnitalRing [NonUnitalRing R] [NonUnitalRing S] : NonUnitalRing (R × S) :=
  { inferInstanceAs (NonUnitalNonAssocRing (R × S)),
    inferInstanceAs (NonUnitalSemiring (R × S)) with }
Product of Non-Unital Rings is a Non-Unital Ring
Informal description
For any two non-unital rings $R$ and $S$, the product $R \times S$ is also a non-unital ring with pointwise addition and multiplication.
Prod.instNonAssocRing instance
[NonAssocRing R] [NonAssocRing S] : NonAssocRing (R × S)
Full source 
instance instNonAssocRing [NonAssocRing R] [NonAssocRing S] : NonAssocRing (R × S) :=
  { inferInstanceAs (NonUnitalNonAssocRing (R × S)),
    inferInstanceAs (NonAssocSemiring (R × S)),
    inferInstanceAs (AddGroupWithOne (R × S)) with }
Product of Non-Associative Rings is a Non-Associative Ring
Informal description
For any two non-associative rings $R$ and $S$, the product $R \times S$ is also a non-associative ring with pointwise addition and multiplication.
Prod.instNonUnitalCommRing instance
[NonUnitalCommRing R] [NonUnitalCommRing S] : NonUnitalCommRing (R × S)
Full source 
/-- Product of two `NonUnitalCommRing`s is a `NonUnitalCommRing`. -/
instance instNonUnitalCommRing [NonUnitalCommRing R] [NonUnitalCommRing S] :
    NonUnitalCommRing (R × S) :=
  { inferInstanceAs (NonUnitalRing (R × S)), inferInstanceAs (CommSemigroup (R × S)) with }
Product of Non-Unital Commutative Rings is a Non-Unital Commutative Ring
Informal description
For any two non-unital commutative rings $R$ and $S$, the product $R \times S$ is also a non-unital commutative ring with pointwise addition and multiplication.
Prod.instCommRing instance
[CommRing R] [CommRing S] : CommRing (R × S)
Full source 
/-- Product of two commutative rings is a commutative ring. -/
instance instCommRing [CommRing R] [CommRing S] : CommRing (R × S) :=
  { inferInstanceAs (Ring (R × S)), inferInstanceAs (CommMonoid (R × S)) with }
Product of Commutative Rings is a Commutative Ring
Informal description
For any two commutative rings $R$ and $S$, the product $R \times S$ is also a commutative ring with componentwise addition and multiplication.
NonUnitalRingHom.fst definition
: R × S →ₙ+* R
Full source 
/-- Given non-unital semirings `R`, `S`, the natural projection homomorphism from `R × S` to `R`. -/
def fst : R × SR × S →ₙ+* R :=
  { MulHom.fst R S, AddMonoidHom.fst R S with toFun := Prod.fst }
First projection as a non-unital ring homomorphism
Informal description
Given non-unital semirings \( R \) and \( S \), the natural projection homomorphism from \( R \times S \) to \( R \) is a non-unital ring homomorphism that maps each pair \( (x, y) \) to its first component \( x \). This homomorphism preserves both the additive and multiplicative structures of the semirings.
NonUnitalRingHom.snd definition
: R × S →ₙ+* S
Full source 
/-- Given non-unital semirings `R`, `S`, the natural projection homomorphism from `R × S` to `S`. -/
def snd : R × SR × S →ₙ+* S :=
  { MulHom.snd R S, AddMonoidHom.snd R S with toFun := Prod.snd }
Second projection as a non-unital ring homomorphism
Informal description
Given non-unital semirings \( R \) and \( S \), the natural projection homomorphism from \( R \times S \) to \( S \) maps each pair \((x, y)\) to its second component \( y \). This homomorphism preserves both the additive and multiplicative structures of the semirings.
NonUnitalRingHom.coe_fst theorem
: ⇑(fst R S) = Prod.fst
Full source 
@[simp]
theorem coe_fst : ⇑(fst R S) = Prod.fst :=
  rfl
First Projection Homomorphism as Standard Projection
Informal description
The underlying function of the first projection non-unital ring homomorphism from $R \times S$ to $R$ is equal to the standard first projection function $\text{fst} : R \times S \to R$.
NonUnitalRingHom.coe_snd theorem
: ⇑(snd R S) = Prod.snd
Full source 
@[simp]
theorem coe_snd : ⇑(snd R S) = Prod.snd :=
  rfl
Coefficient of Second Projection Non-Unital Ring Homomorphism Equals Standard Projection
Informal description
The underlying function of the second projection non-unital ring homomorphism from $R \times S$ to $S$ is equal to the standard second projection function $\operatorname{snd} : R \times S \to S$.
NonUnitalRingHom.prod definition
(f : R →ₙ+* S) (g : R →ₙ+* T) : R →ₙ+* S × T
Full source 
/-- Combine two non-unital ring homomorphisms `f : R →ₙ+* S`, `g : R →ₙ+* T` into
`f.prod g : R →ₙ+* S × T` given by `(f.prod g) x = (f x, g x)` -/
protected def prod (f : R →ₙ+* S) (g : R →ₙ+* T) : R →ₙ+* S × T :=
  { MulHom.prod (f : MulHom R S) (g : MulHom R T), AddMonoidHom.prod (f : R →+ S) (g : R →+ T) with
    toFun := fun x => (f x, g x) }
Product of non-unital ring homomorphisms
Informal description
Given two non-unital ring homomorphisms \( f \colon R \to S \) and \( g \colon R \to T \), the function \( f \times g \colon R \to S \times T \) is defined by \( (f \times g)(x) = (f(x), g(x)) \) for all \( x \in R \). This function is itself a non-unital ring homomorphism, preserving both addition and multiplication.
NonUnitalRingHom.prod_apply theorem
(x) : f.prod g x = (f x, g x)
Full source 
@[simp]
theorem prod_apply (x) : f.prod g x = (f x, g x) :=
  rfl
Evaluation of Product Non-Unital Ring Homomorphism: $(f \times g)(x) = (f(x), g(x))$
Informal description
For any non-unital ring homomorphisms $f \colon R \to S$ and $g \colon R \to T$, and for any element $x \in R$, the product homomorphism $f \times g$ evaluated at $x$ is equal to $(f(x), g(x))$.
NonUnitalRingHom.fst_comp_prod theorem
: (fst S T).comp (f.prod g) = f
Full source 
@[simp]
theorem fst_comp_prod : (fst S T).comp (f.prod g) = f :=
  ext fun _ => rfl
First projection of product homomorphism equals original homomorphism
Informal description
For non-unital ring homomorphisms $f \colon R \to S$ and $g \colon R \to T$, the composition of the first projection homomorphism $\mathrm{fst} \colon S \times T \to S$ with the product homomorphism $f \times g \colon R \to S \times T$ equals $f$, i.e., $\mathrm{fst} \circ (f \times g) = f$.
NonUnitalRingHom.snd_comp_prod theorem
: (snd S T).comp (f.prod g) = g
Full source 
@[simp]
theorem snd_comp_prod : (snd S T).comp (f.prod g) = g :=
  ext fun _ => rfl
Composition of Second Projection with Product Homomorphism Equals Second Factor
Informal description
For any non-unital ring homomorphisms $f \colon R \to S$ and $g \colon R \to T$, the composition of the second projection homomorphism $\mathrm{snd}_{S,T} \colon S \times T \to T$ with the product homomorphism $f \times g \colon R \to S \times T$ equals $g$. In other words, $\mathrm{snd}_{S,T} \circ (f \times g) = g$.
NonUnitalRingHom.prod_unique theorem
(f : R →ₙ+* S × T) : ((fst S T).comp f).prod ((snd S T).comp f) = f
Full source 
theorem prod_unique (f : R →ₙ+* S × T) : ((fst S T).comp f).prod ((snd S T).comp f) = f :=
  ext fun x => by simp only [prod_apply, coe_fst, coe_snd, comp_apply]
Uniqueness of Non-Unital Ring Homomorphism via Projections
Informal description
For any non-unital ring homomorphism $f \colon R \to S \times T$, the composition of $f$ with the first and second projection homomorphisms $f_1 \colon S \times T \to S$ and $f_2 \colon S \times T \to T$ satisfies $(f_1 \circ f, f_2 \circ f) = f$. In other words, $f$ is uniquely determined by its compositions with the projection homomorphisms.
NonUnitalRingHom.prodMap definition
: R × S →ₙ+* R' × S'
Full source 
/-- `Prod.map` as a `NonUnitalRingHom`. -/
def prodMap : R × SR × S →ₙ+* R' × S' :=
  (f.comp (fst R S)).prod (g.comp (snd R S))
Product map of non-unital ring homomorphisms
Informal description
Given non-unital ring homomorphisms \( f \colon R \to R' \) and \( g \colon S \to S' \), the product map \( f \times g \colon R \times S \to R' \times S' \) is defined by \((f \times g)(x, y) = (f(x), g(y))\) for all \((x, y) \in R \times S\). This map is a non-unital ring homomorphism that preserves both addition and multiplication.
NonUnitalRingHom.prodMap_def theorem
: prodMap f g = (f.comp (fst R S)).prod (g.comp (snd R S))
Full source 
theorem prodMap_def : prodMap f g = (f.comp (fst R S)).prod (g.comp (snd R S)) :=
  rfl
Definition of Product Map via Projections for Non-Unital Ring Homomorphisms
Informal description
Given non-unital ring homomorphisms $f \colon R \to R'$ and $g \colon S \to S'$, the product map $\mathrm{prodMap}\, f\, g \colon R \times S \to R' \times S'$ is equal to the composition of $f$ with the first projection $\mathrm{fst}\, R\, S$ paired with the composition of $g$ with the second projection $\mathrm{snd}\, R\, S$. In other words, $\mathrm{prodMap}\, f\, g = (f \circ \mathrm{fst}\, R\, S, g \circ \mathrm{snd}\, R\, S)$.
NonUnitalRingHom.coe_prodMap theorem
: ⇑(prodMap f g) = Prod.map f g
Full source 
@[simp]
theorem coe_prodMap : ⇑(prodMap f g) = Prod.map f g :=
  rfl
Product map of non-unital ring homomorphisms equals product map of functions
Informal description
The underlying function of the product map of non-unital ring homomorphisms $f \colon R \to R'$ and $g \colon S \to S'$ is equal to the product map of functions, i.e., $(f \times g)(x, y) = (f(x), g(y))$ for all $(x, y) \in R \times S$.
NonUnitalRingHom.prod_comp_prodMap theorem
(f : T →ₙ+* R) (g : T →ₙ+* S) (f' : R →ₙ+* R') (g' : S →ₙ+* S') : (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)
Full source 
theorem prod_comp_prodMap (f : T →ₙ+* R) (g : T →ₙ+* S) (f' : R →ₙ+* R') (g' : S →ₙ+* S') :
    (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g) :=
  rfl
Composition of Product Maps Equals Product of Compositions for Non-Unital Ring Homomorphisms
Informal description
Given non-unital ring homomorphisms $f \colon T \to R$, $g \colon T \to S$, $f' \colon R \to R'$, and $g' \colon S \to S'$, the composition of the product map $(f' \times g')$ with the product homomorphism $(f \times g)$ is equal to the product of the compositions $(f' \circ f) \times (g' \circ g)$. That is, $$(f' \times g') \circ (f \times g) = (f' \circ f) \times (g' \circ g).$$
RingHom.fst definition
: R × S →+* R
Full source 
/-- Given semirings `R`, `S`, the natural projection homomorphism from `R × S` to `R`. -/
def fst : R × SR × S →+* R :=
  { MonoidHom.fst R S, AddMonoidHom.fst R S with toFun := Prod.fst }
First projection ring homomorphism
Informal description
The ring homomorphism from the product ring \( R \times S \) to \( R \) that projects onto the first component. It preserves addition, multiplication, and the multiplicative identity, mapping \((x, y)\) to \(x\).
RingHom.snd definition
: R × S →+* S
Full source 
/-- Given semirings `R`, `S`, the natural projection homomorphism from `R × S` to `S`. -/
def snd : R × SR × S →+* S :=
  { MonoidHom.snd R S, AddMonoidHom.snd R S with toFun := Prod.snd }
Second projection semiring homomorphism
Informal description
The natural projection homomorphism from the product semiring \( R \times S \) to the semiring \( S \), which maps each pair \((r, s)\) to its second component \(s\). This homomorphism preserves both the additive and multiplicative structures of the semirings.
RingHom.instRingHomSurjectiveProdFst instance
(R S) [Semiring R] [Semiring S] : RingHomSurjective (fst R S)
Full source 
instance (R S) [Semiring R] [Semiring S] : RingHomSurjective (fst R S) := ⟨(⟨⟨·, 0⟩, rfl⟩)⟩
Surjectivity of the First Projection Ring Homomorphism
Informal description
For any two semirings $R$ and $S$, the first projection homomorphism $fst : R \times S \to R$ is surjective.
RingHom.instRingHomSurjectiveProdSnd instance
(R S) [Semiring R] [Semiring S] : RingHomSurjective (snd R S)
Full source 
instance (R S) [Semiring R] [Semiring S] : RingHomSurjective (snd R S) := ⟨(⟨⟨0, ·⟩, rfl⟩)⟩
Surjectivity of the Second Projection Homomorphism on Product Semirings
Informal description
For any two semirings $R$ and $S$, the second projection homomorphism $snd : R \times S \to S$ is surjective.
RingHom.coe_fst theorem
: ⇑(fst R S) = Prod.fst
Full source 
@[simp]
theorem coe_fst : ⇑(fst R S) = Prod.fst :=
  rfl
First Projection Ring Homomorphism as Standard Projection
Informal description
The underlying function of the first projection ring homomorphism $\operatorname{fst} \colon R \times S \to R$ is equal to the standard first projection function $\operatorname{Prod.fst} \colon R \times S \to R$, which maps $(x, y) \mapsto x$.
RingHom.coe_snd theorem
: ⇑(snd R S) = Prod.snd
Full source 
@[simp]
theorem coe_snd : ⇑(snd R S) = Prod.snd :=
  rfl
Second Projection Ring Homomorphism as Standard Projection
Informal description
The underlying function of the second projection ring homomorphism $\text{snd} : R \times S \to S$ is equal to the standard second projection function $\text{Prod.snd} : R \times S \to S$.
RingHom.prod definition
(f : R →+* S) (g : R →+* T) : R →+* S × T
Full source 
/-- Combine two ring homomorphisms `f : R →+* S`, `g : R →+* T` into `f.prod g : R →+* S × T`
given by `(f.prod g) x = (f x, g x)` -/
protected def prod (f : R →+* S) (g : R →+* T) : R →+* S × T :=
  { MonoidHom.prod (f : R →* S) (g : R →* T), AddMonoidHom.prod (f : R →+ S) (g : R →+ T) with
    toFun := fun x => (f x, g x) }
Product of (semi-)ring homomorphisms
Informal description
Given two (semi-)ring homomorphisms \( f : R \to S \) and \( g : R \to T \), the function \( f \times g : R \to S \times T \) defined by \( (f \times g)(x) = (f(x), g(x)) \) is also a (semi-)ring homomorphism.
RingHom.prod_apply theorem
(x) : f.prod g x = (f x, g x)
Full source 
@[simp]
theorem prod_apply (x) : f.prod g x = (f x, g x) :=
  rfl
Evaluation of Product Ring Homomorphism: $(f \times g)(x) = (f(x), g(x))$
Informal description
For any ring homomorphisms $f \colon R \to S$ and $g \colon R \to T$, and any element $x \in R$, the product homomorphism $f \times g$ evaluated at $x$ equals $(f(x), g(x))$.
RingHom.fst_comp_prod theorem
: (fst S T).comp (f.prod g) = f
Full source 
@[simp]
theorem fst_comp_prod : (fst S T).comp (f.prod g) = f :=
  ext fun _ => rfl
Composition of first projection with product homomorphism equals first homomorphism
Informal description
For any ring homomorphisms $f \colon R \to S$ and $g \colon R \to T$, the composition of the first projection homomorphism $\mathrm{fst}_{S,T} \colon S \times T \to S$ with the product homomorphism $f \times g \colon R \to S \times T$ equals $f$.
RingHom.snd_comp_prod theorem
: (snd S T).comp (f.prod g) = g
Full source 
@[simp]
theorem snd_comp_prod : (snd S T).comp (f.prod g) = g :=
  ext fun _ => rfl
Composition of second projection with product homomorphism equals second homomorphism
Informal description
For any ring homomorphisms $f \colon R \to S$ and $g \colon R \to T$, the composition of the second projection homomorphism $\mathrm{snd}_{S,T} \colon S \times T \to T$ with the product homomorphism $f \times g \colon R \to S \times T$ equals $g$.
RingHom.prod_unique theorem
(f : R →+* S × T) : ((fst S T).comp f).prod ((snd S T).comp f) = f
Full source 
theorem prod_unique (f : R →+* S × T) : ((fst S T).comp f).prod ((snd S T).comp f) = f :=
  ext fun x => by simp only [prod_apply, coe_fst, coe_snd, comp_apply]
Uniqueness of Product Homomorphism via Projections
Informal description
For any ring homomorphism $f \colon R \to S \times T$, the product of the compositions of $f$ with the first and second projection homomorphisms equals $f$ itself. That is, $(f_1 \circ f, f_2 \circ f) = f$, where $f_1 \colon S \times T \to S$ and $f_2 \colon S \times T \to T$ are the projection homomorphisms.
RingHom.prodMap definition
: R × S →+* R' × S'
Full source 
/-- `Prod.map` as a `RingHom`. -/
def prodMap : R × SR × S →+* R' × S' :=
  (f.comp (fst R S)).prod (g.comp (snd R S))
Product map of ring homomorphisms
Informal description
Given ring homomorphisms \( f : R \to R' \) and \( g : S \to S' \), the function \( \text{prodMap} \) is the ring homomorphism from \( R \times S \) to \( R' \times S' \) defined by mapping \((x, y)\) to \((f(x), g(y))\).
RingHom.prodMap_def theorem
: prodMap f g = (f.comp (fst R S)).prod (g.comp (snd R S))
Full source 
theorem prodMap_def : prodMap f g = (f.comp (fst R S)).prod (g.comp (snd R S)) :=
  rfl
Definition of Product Map via Projections
Informal description
Given ring homomorphisms $f \colon R \to R'$ and $g \colon S \to S'$, the product map $\text{prodMap}\, f\, g$ is equal to the product of the compositions of $f$ with the first projection $\text{fst} \colon R \times S \to R$ and $g$ with the second projection $\text{snd} \colon R \times S \to S$. That is, \[ \text{prodMap}\, f\, g = (f \circ \text{fst}) \times (g \circ \text{snd}). \]
RingHom.coe_prodMap theorem
: ⇑(prodMap f g) = Prod.map f g
Full source 
@[simp]
theorem coe_prodMap : ⇑(prodMap f g) = Prod.map f g :=
  rfl
Coefficient of Product Map of Ring Homomorphisms Equals Product Map
Informal description
The underlying function of the ring homomorphism $\text{prodMap}\, f\, g$ is equal to the product map $\text{Prod.map}\, f\, g$, which sends $(x, y)$ to $(f(x), g(y))$.
RingHom.prod_comp_prodMap theorem
(f : T →+* R) (g : T →+* S) (f' : R →+* R') (g' : S →+* S') : (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)
Full source 
theorem prod_comp_prodMap (f : T →+* R) (g : T →+* S) (f' : R →+* R') (g' : S →+* S') :
    (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g) :=
  rfl
Composition of Product Maps Equals Product of Compositions
Informal description
Given ring homomorphisms $f \colon T \to R$, $g \colon T \to S$, $f' \colon R \to R'$, and $g' \colon S \to S'$, the composition of the product map $(f' \times g') \colon R \times S \to R' \times S'$ with the product homomorphism $(f \times g) \colon T \to R \times S$ equals the product of the compositions $(f' \circ f) \times (g' \circ g) \colon T \to R' \times S'$.
RingEquiv.prodComm definition
: R × S ≃+* S × R
Full source 
/-- Swapping components as an equivalence of (semi)rings. -/
def prodComm : R × SR × S ≃+* S × R :=
  { AddEquiv.prodComm, MulEquiv.prodComm with }
Ring equivalence by component swapping
Informal description
The ring equivalence between the product rings \( R \times S \) and \( S \times R \) is given by swapping the components, i.e., mapping \( (x, y) \) to \( (y, x) \). This equivalence preserves both the additive and multiplicative ring structures.
RingEquiv.coe_prodComm theorem
: ⇑(prodComm : R × S ≃+* S × R) = Prod.swap
Full source 
@[simp]
theorem coe_prodComm : ⇑(prodComm : R × SR × S ≃+* S × R) = Prod.swap :=
  rfl
Ring Equivalence `prodComm` is Component Swapping
Informal description
The underlying function of the ring equivalence `prodComm` between the product rings $R \times S$ and $S \times R$ is equal to the component-swapping function $\text{Prod.swap}$, which maps $(x, y)$ to $(y, x)$.
RingEquiv.coe_prodComm_symm theorem
: ⇑(prodComm : R × S ≃+* S × R).symm = Prod.swap
Full source 
@[simp]
theorem coe_prodComm_symm : ⇑(prodComm : R × SR × S ≃+* S × R).symm = Prod.swap :=
  rfl
Inverse of Ring Equivalence by Component Swapping is Component Swapping
Informal description
The underlying function of the inverse of the ring equivalence `prodComm` between $R \times S$ and $S \times R$ is equal to the component-swapping function $\text{Prod.swap}$, which maps $(x, y)$ to $(y, x)$.
RingEquiv.fst_comp_coe_prodComm theorem
: (RingHom.fst S R).comp ↑(prodComm : R × S ≃+* S × R) = RingHom.snd R S
Full source 
@[simp]
theorem fst_comp_coe_prodComm :
    (RingHom.fst S R).comp ↑(prodComm : R × SR × S ≃+* S × R) = RingHom.snd R S :=
  RingHom.ext fun _ => rfl
First Projection Composed with Product Commutativity Equals Second Projection
Informal description
The composition of the first projection ring homomorphism from $S \times R$ to $S$ with the ring equivalence $\text{prodComm} : R \times S \simeq+* S \times R$ is equal to the second projection ring homomorphism from $R \times S$ to $S$. In other words, for any $(x, y) \in R \times S$, we have $\text{fst}_{S,R}(\text{prodComm}(x, y)) = \text{snd}_{R,S}(x, y)$.
RingEquiv.snd_comp_coe_prodComm theorem
: (RingHom.snd S R).comp ↑(prodComm : R × S ≃+* S × R) = RingHom.fst R S
Full source 
@[simp]
theorem snd_comp_coe_prodComm :
    (RingHom.snd S R).comp ↑(prodComm : R × SR × S ≃+* S × R) = RingHom.fst R S :=
  RingHom.ext fun _ => rfl
Composition of Second Projection with Component Swap Equals First Projection
Informal description
The composition of the second projection ring homomorphism from $S \times R$ to $R$ with the ring equivalence that swaps components of $R \times S$ is equal to the first projection ring homomorphism from $R \times S$ to $R$. In other words, for any $(x, y) \in R \times S$, we have $\text{snd}_{S,R}(y, x) = \text{fst}_{R,S}(x, y)$.
RingEquiv.prodProdProdComm definition
: (R × R') × S × S' ≃+* (R × S) × R' × S'
Full source 
/-- Four-way commutativity of `Prod`. The name matches `mul_mul_mul_comm`. -/
@[simps apply]
def prodProdProdComm : (R × R') × S × S'(R × R') × S × S' ≃+* (R × S) × R' × S' :=
  { AddEquiv.prodProdProdComm R R' S S', MulEquiv.prodProdProdComm R R' S S' with
    toFun := fun rrss => ((rrss.1.1, rrss.2.1), (rrss.1.2, rrss.2.2))
    invFun := fun rsrs => ((rsrs.1.1, rsrs.2.1), (rsrs.1.2, rsrs.2.2)) }
Four-way product commutativity ring equivalence
Informal description
The ring equivalence between the products $(R \times R') \times (S \times S')$ and $(R \times S) \times (R' \times S')$, which rearranges the components as $((r, r'), (s, s')) \mapsto ((r, s), (r', s'))$. This equivalence preserves both the additive and multiplicative ring structures.
RingEquiv.prodProdProdComm_symm theorem
: (prodProdProdComm R R' S S').symm = prodProdProdComm R S R' S'
Full source 
@[simp]
theorem prodProdProdComm_symm : (prodProdProdComm R R' S S').symm = prodProdProdComm R S R' S' :=
  rfl
Symmetry of Four-Way Product Commutativity Ring Equivalence
Informal description
The symmetry of the four-way product commutativity ring equivalence states that the inverse of the equivalence $(R \times R') \times (S \times S') \simeq (R \times S) \times (R' \times S')$ is equal to the equivalence $(R \times S) \times (R' \times S') \simeq (R \times R') \times (S \times S')$.
RingEquiv.prodProdProdComm_toAddEquiv theorem
: (prodProdProdComm R R' S S' : _ ≃+ _) = AddEquiv.prodProdProdComm R R' S S'
Full source 
@[simp]
theorem prodProdProdComm_toAddEquiv :
    (prodProdProdComm R R' S S' : _ ≃+ _) = AddEquiv.prodProdProdComm R R' S S' :=
  rfl
Additive Equivalence Underlying Four-Way Product Commutativity Ring Isomorphism
Informal description
The additive equivalence underlying the ring isomorphism `prodProdProdComm` between $(R \times R') \times (S \times S')$ and $(R \times S) \times (R' \times S')$ is equal to the additive equivalence `AddEquiv.prodProdProdComm` that rearranges the components as $((r, r'), (s, s')) \mapsto ((r, s), (r', s'))$.
RingEquiv.prodProdProdComm_toMulEquiv theorem
: (prodProdProdComm R R' S S' : _ ≃* _) = MulEquiv.prodProdProdComm R R' S S'
Full source 
@[simp]
theorem prodProdProdComm_toMulEquiv :
    (prodProdProdComm R R' S S' : _ ≃* _) = MulEquiv.prodProdProdComm R R' S S' :=
  rfl
Underlying Multiplicative Equivalence of Four-Way Product Commutativity Ring Isomorphism
Informal description
The multiplicative equivalence underlying the ring isomorphism $\text{prodProdProdComm}$ between $(R \times R') \times (S \times S')$ and $(R \times S) \times (R' \times S')$ is equal to the multiplicative equivalence $\text{MulEquiv.prodProdProdComm}$ that rearranges the components as $((r, r'), (s, s')) \mapsto ((r, s), (r', s'))$.
RingEquiv.prodProdProdComm_toEquiv theorem
: (prodProdProdComm R R' S S' : _ ≃ _) = Equiv.prodProdProdComm R R' S S'
Full source 
@[simp]
theorem prodProdProdComm_toEquiv :
    (prodProdProdComm R R' S S' : _ ≃ _) = Equiv.prodProdProdComm R R' S S' :=
  rfl
Equivalence Underlying the Four-Way Product Commutativity Ring Isomorphism
Informal description
The underlying equivalence of the ring isomorphism `RingEquiv.prodProdProdComm` between $(R \times R') \times (S \times S')$ and $(R \times S) \times (R' \times S')$ is equal to the bijection `Equiv.prodProdProdComm` that rearranges the components as $((r, r'), (s, s')) \mapsto ((r, s), (r', s'))$.
RingEquiv.prodZeroRing definition
: R ≃+* R × S
Full source 
/-- A ring `R` is isomorphic to `R × S` when `S` is the zero ring -/
@[simps]
def prodZeroRing : R ≃+* R × S where
  toFun x := (x, 0)
  invFun := Prod.fst
  map_add' := by simp
  map_mul' := by simp
  left_inv _ := rfl
  right_inv x := by cases x; simp [eq_iff_true_of_subsingleton]
Ring isomorphism between $R$ and $R \times S$ when $S$ is the zero ring
Informal description
The ring isomorphism from a ring $R$ to the product ring $R \times S$, where $S$ is the zero ring. The isomorphism maps an element $x \in R$ to $(x, 0) \in R \times S$, and its inverse is the projection onto the first component. This isomorphism preserves both addition and multiplication.
RingEquiv.zeroRingProd definition
: R ≃+* S × R
Full source 
/-- A ring `R` is isomorphic to `S × R` when `S` is the zero ring -/
@[simps]
def zeroRingProd : R ≃+* S × R where
  toFun x := (0, x)
  invFun := Prod.snd
  map_add' := by simp
  map_mul' := by simp
  left_inv _ := rfl
  right_inv x := by cases x; simp [eq_iff_true_of_subsingleton]
Ring isomorphism between $R$ and $S \times R$ when $S$ is the zero ring
Informal description
The ring isomorphism from a ring $R$ to the product ring $S \times R$, where $S$ is the zero ring. The isomorphism maps an element $x \in R$ to $(0, x) \in S \times R$, and its inverse is the projection onto the second component. This isomorphism preserves both addition and multiplication.
false_of_nontrivial_of_product_domain theorem
(R S : Type*) [Semiring R] [Semiring S] [IsDomain (R × S)] [Nontrivial R] [Nontrivial S] : False
Full source 
/-- The product of two nontrivial rings is not a domain -/
theorem false_of_nontrivial_of_product_domain (R S : Type*) [Semiring R] [Semiring S]
    [IsDomain (R × S)] [Nontrivial R] [Nontrivial S] : False := by
  have :=
    NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero (show ((0 : R), (1 : S)) * (1, 0) = 0 by simp)
  rw [Prod.mk_eq_zero, Prod.mk_eq_zero] at this
  rcases this with (⟨_, h⟩ | ⟨h, _⟩)
  · exact zero_ne_one h.symm
  · exact zero_ne_one h.symm
Product of Nontrivial Semirings is Not a Domain
Informal description
If $R$ and $S$ are nontrivial semirings, then their product $R \times S$ cannot be an integral domain.