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).

instance Prod.instDistrib {R : Type u_1} {S : Type u_3} [Distrib R] [Distrib S] : Distrib (R × S)

Product of two distributive types is distributive.

instance Prod.instNonUnitalNonAssocSemiring {R : Type u_1} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] : NonUnitalNonAssocSemiring (R × S)

Product of two NonUnitalNonAssocSemirings is a NonUnitalNonAssocSemiring.

instance Prod.instNonUnitalSemiring {R : Type u_1} {S : Type u_3} [NonUnitalSemiring R] [NonUnitalSemiring S] : NonUnitalSemiring (R × S)

Product of two NonUnitalSemirings is a NonUnitalSemiring.

instance Prod.instNonAssocSemiring {R : Type u_1} {S : Type u_3} [NonAssocSemiring R] [NonAssocSemiring S] : NonAssocSemiring (R × S)

Product of two NonAssocSemirings is a NonAssocSemiring.

instance Prod.instSemiring {R : Type u_1} {S : Type u_3} [Semiring R] [Semiring S] : Semiring (R × S)

Product of two semirings is a semiring.

instance Prod.instNonUnitalCommSemiring {R : Type u_1} {S : Type u_3} [NonUnitalCommSemiring R] [NonUnitalCommSemiring S] : NonUnitalCommSemiring (R × S)

Product of two NonUnitalCommSemirings is a NonUnitalCommSemiring.

instance Prod.instCommSemiring {R : Type u_1} {S : Type u_3} [CommSemiring R] [CommSemiring S] : CommSemiring (R × S)

Product of two commutative semirings is a commutative semiring.

instance Prod.instNonUnitalNonAssocRing {R : Type u_1} {S : Type u_3} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] : NonUnitalNonAssocRing (R × S)

instance Prod.instNonUnitalRing {R : Type u_1} {S : Type u_3} [NonUnitalRing R] [NonUnitalRing S] : NonUnitalRing (R × S)

instance Prod.instNonAssocRing {R : Type u_1} {S : Type u_3} [NonAssocRing R] [NonAssocRing S] : NonAssocRing (R × S)

instance Prod.instRing {R : Type u_1} {S : Type u_3} [Ring R] [Ring S] : Ring (R × S)

Product of two rings is a ring.

instance Prod.instNonUnitalCommRing {R : Type u_1} {S : Type u_3} [NonUnitalCommRing R] [NonUnitalCommRing S] : NonUnitalCommRing (R × S)

Product of two NonUnitalCommRings is a NonUnitalCommRing.

instance Prod.instCommRing {R : Type u_1} {S : Type u_3} [CommRing R] [CommRing S] : CommRing (R × S)

Product of two commutative rings is a commutative ring.

def NonUnitalRingHom.fst (R : Type u_1) (S : Type u_3) [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] : R × S →ₙ+* R

Given non-unital semirings R, S, the natural projection homomorphism from R × S to R.

def NonUnitalRingHom.snd (R : Type u_1) (S : Type u_3) [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] : R × S →ₙ+* S

Given non-unital semirings R, S, the natural projection homomorphism from R × S to S.

@[simp]

theorem NonUnitalRingHom.coe_fst {R : Type u_1} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] : ⇑(fst R S) = Prod.fst

@[simp]

theorem NonUnitalRingHom.coe_snd {R : Type u_1} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] : ⇑(snd R S) = Prod.snd

def NonUnitalRingHom.prod {R : Type u_1} {S : Type u_3} {T : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring T] (f : R →ₙ+* S) (g : R →ₙ+* T) : R →ₙ+* S × T

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)

@[simp]

theorem NonUnitalRingHom.prod_apply {R : Type u_1} {S : Type u_3} {T : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring T] (f : R →ₙ+* S) (g : R →ₙ+* T) (x : R) : (f.prod g) x = (f x, g x)

@[simp]

theorem NonUnitalRingHom.fst_comp_prod {R : Type u_1} {S : Type u_3} {T : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring T] (f : R →ₙ+* S) (g : R →ₙ+* T) : (fst S T).comp (f.prod g) = f

@[simp]

theorem NonUnitalRingHom.snd_comp_prod {R : Type u_1} {S : Type u_3} {T : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring T] (f : R →ₙ+* S) (g : R →ₙ+* T) : (snd S T).comp (f.prod g) = g

theorem NonUnitalRingHom.prod_unique {R : Type u_1} {S : Type u_3} {T : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring T] (f : R →ₙ+* S × T) : ((fst S T).comp f).prod ((snd S T).comp f) = f

def NonUnitalRingHom.prodMap {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring R'] [NonUnitalNonAssocSemiring S'] (f : R →ₙ+* R') (g : S →ₙ+* S') : R × S →ₙ+* R' × S'

Prod.map as a NonUnitalRingHom.

theorem NonUnitalRingHom.prodMap_def {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring R'] [NonUnitalNonAssocSemiring S'] (f : R →ₙ+* R') (g : S →ₙ+* S') : f.prodMap g = (f.comp (fst R S)).prod (g.comp (snd R S))

@[simp]

theorem NonUnitalRingHom.coe_prodMap {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring R'] [NonUnitalNonAssocSemiring S'] (f : R →ₙ+* R') (g : S →ₙ+* S') : ⇑(f.prodMap g) = Prod.map ⇑f ⇑g

theorem NonUnitalRingHom.prod_comp_prodMap {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} {T : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring R'] [NonUnitalNonAssocSemiring S'] [NonUnitalNonAssocSemiring T] (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)

def RingHom.fst (R : Type u_1) (S : Type u_3) [NonAssocSemiring R] [NonAssocSemiring S] : R × S →+* R

Given semirings R, S, the natural projection homomorphism from R × S to R.

def RingHom.snd (R : Type u_1) (S : Type u_3) [NonAssocSemiring R] [NonAssocSemiring S] : R × S →+* S

Given semirings R, S, the natural projection homomorphism from R × S to S.

instance RingHom.instRingHomSurjectiveProdFst (R : Type u_6) (S : Type u_7) [Semiring R] [Semiring S] : RingHomSurjective (fst R S)

instance RingHom.instRingHomSurjectiveProdSnd (R : Type u_6) (S : Type u_7) [Semiring R] [Semiring S] : RingHomSurjective (snd R S)

@[simp]

theorem RingHom.coe_fst {R : Type u_1} {S : Type u_3} [NonAssocSemiring R] [NonAssocSemiring S] : ⇑(fst R S) = Prod.fst

@[simp]

theorem RingHom.coe_snd {R : Type u_1} {S : Type u_3} [NonAssocSemiring R] [NonAssocSemiring S] : ⇑(snd R S) = Prod.snd

def RingHom.prod {R : Type u_1} {S : Type u_3} {T : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring T] (f : R →+* S) (g : R →+* T) : R →+* S × T

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)

@[simp]

theorem RingHom.prod_apply {R : Type u_1} {S : Type u_3} {T : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring T] (f : R →+* S) (g : R →+* T) (x : R) : (f.prod g) x = (f x, g x)

@[simp]

theorem RingHom.fst_comp_prod {R : Type u_1} {S : Type u_3} {T : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring T] (f : R →+* S) (g : R →+* T) : (fst S T).comp (f.prod g) = f

@[simp]

theorem RingHom.snd_comp_prod {R : Type u_1} {S : Type u_3} {T : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring T] (f : R →+* S) (g : R →+* T) : (snd S T).comp (f.prod g) = g

theorem RingHom.prod_unique {R : Type u_1} {S : Type u_3} {T : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring T] (f : R →+* S × T) : ((fst S T).comp f).prod ((snd S T).comp f) = f

def RingHom.prodMap {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] (f : R →+* R') (g : S →+* S') : R × S →+* R' × S'

Prod.map as a RingHom.

theorem RingHom.prodMap_def {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] (f : R →+* R') (g : S →+* S') : f.prodMap g = (f.comp (fst R S)).prod (g.comp (snd R S))

@[simp]

theorem RingHom.coe_prodMap {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] (f : R →+* R') (g : S →+* S') : ⇑(f.prodMap g) = Prod.map ⇑f ⇑g

theorem RingHom.prod_comp_prodMap {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} {T : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] [NonAssocSemiring T] (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)

def RingEquiv.prodComm {R : Type u_1} {S : Type u_3} [NonAssocSemiring R] [NonAssocSemiring S] : R × S ≃+* S × R

Swapping components as an equivalence of (semi)rings.

@[simp]

theorem RingEquiv.coe_prodComm {R : Type u_1} {S : Type u_3} [NonAssocSemiring R] [NonAssocSemiring S] : ⇑prodComm = Prod.swap

@[simp]

theorem RingEquiv.coe_prodComm_symm {R : Type u_1} {S : Type u_3} [NonAssocSemiring R] [NonAssocSemiring S] : ⇑prodComm.symm = Prod.swap

@[simp]

theorem RingEquiv.fst_comp_coe_prodComm {R : Type u_1} {S : Type u_3} [NonAssocSemiring R] [NonAssocSemiring S] : (RingHom.fst S R).comp ↑prodComm = RingHom.snd R S

@[simp]

theorem RingEquiv.snd_comp_coe_prodComm {R : Type u_1} {S : Type u_3} [NonAssocSemiring R] [NonAssocSemiring S] : (RingHom.snd S R).comp ↑prodComm = RingHom.fst R S

def RingEquiv.prodProdProdComm (R : Type u_1) (R' : Type u_2) (S : Type u_3) (S' : Type u_4) [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] : (R × R') × S × S' ≃+* (R × S) × R' × S'

Four-way commutativity of Prod. The name matches mul_mul_mul_comm.

@[simp]

theorem RingEquiv.prodProdProdComm_apply (R : Type u_1) (R' : Type u_2) (S : Type u_3) (S' : Type u_4) [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] (rrss : (R × R') × S × S') : (prodProdProdComm R R' S S') rrss = ((rrss.1.1, rrss.2.1), rrss.1.2, rrss.2.2)

@[simp]

theorem RingEquiv.prodProdProdComm_symm (R : Type u_1) (R' : Type u_2) (S : Type u_3) (S' : Type u_4) [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] : (prodProdProdComm R R' S S').symm = prodProdProdComm R S R' S'

@[simp]

theorem RingEquiv.prodProdProdComm_toAddEquiv (R : Type u_1) (R' : Type u_2) (S : Type u_3) (S' : Type u_4) [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] : ↑(prodProdProdComm R R' S S') = AddEquiv.prodProdProdComm R R' S S'

@[simp]

theorem RingEquiv.prodProdProdComm_toMulEquiv (R : Type u_1) (R' : Type u_2) (S : Type u_3) (S' : Type u_4) [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] : ↑(prodProdProdComm R R' S S') = MulEquiv.prodProdProdComm R R' S S'

@[simp]

theorem RingEquiv.prodProdProdComm_toEquiv (R : Type u_1) (R' : Type u_2) (S : Type u_3) (S' : Type u_4) [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] : ↑(prodProdProdComm R R' S S') = Equiv.prodProdProdComm R R' S S'

def RingEquiv.prodZeroRing (R : Type u_1) (S : Type u_3) [NonAssocSemiring R] [NonAssocSemiring S] [Subsingleton S] : R ≃+* R × S

A ring R is isomorphic to R × S when S is the zero ring

@[simp]

theorem RingEquiv.prodZeroRing_apply (R : Type u_1) (S : Type u_3) [NonAssocSemiring R] [NonAssocSemiring S] [Subsingleton S] (x : R) : (prodZeroRing R S) x = (x, 0)

@[simp]

theorem RingEquiv.prodZeroRing_symm_apply (R : Type u_1) (S : Type u_3) [NonAssocSemiring R] [NonAssocSemiring S] [Subsingleton S] (self : R × S) : (prodZeroRing R S).symm self = self.1

def RingEquiv.zeroRingProd (R : Type u_1) (S : Type u_3) [NonAssocSemiring R] [NonAssocSemiring S] [Subsingleton S] : R ≃+* S × R

A ring R is isomorphic to S × R when S is the zero ring

@[simp]

theorem RingEquiv.zeroRingProd_apply (R : Type u_1) (S : Type u_3) [NonAssocSemiring R] [NonAssocSemiring S] [Subsingleton S] (x : R) : (zeroRingProd R S) x = (0, x)

@[simp]

theorem RingEquiv.zeroRingProd_symm_apply (R : Type u_1) (S : Type u_3) [NonAssocSemiring R] [NonAssocSemiring S] [Subsingleton S] (self : S × R) : (zeroRingProd R S).symm self = self.2

theorem false_of_nontrivial_of_product_domain (R : Type u_6) (S : Type u_7) [Semiring R] [Semiring S] [IsDomain (R × S)] [Nontrivial R] [Nontrivial S] : False

The product of two nontrivial rings is not a domain