Documentation

Mathlib.Algebra.Ring.Prod

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

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

instance Prod.instDistribProd {R : Type u_1} {S : Type u_2} [inst : Distrib R] [inst : Distrib S] :
Distrib (R × S)

Product of two distributive types is distributive.

Equations
  • One or more equations did not get rendered due to their size.

Product of two NonUnitalNonAssocSemirings is a NonUnitalNonAssocSemiring.

Equations
  • One or more equations did not get rendered due to their size.
instance Prod.instNonUnitalSemiringProd {R : Type u_1} {S : Type u_2} [inst : NonUnitalSemiring R] [inst : NonUnitalSemiring S] :

Product of two NonUnitalSemirings is a NonUnitalSemiring.

Equations
  • One or more equations did not get rendered due to their size.
instance Prod.instNonAssocSemiringProd {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] :

Product of two NonAssocSemirings is a NonAssocSemiring.

Equations
  • One or more equations did not get rendered due to their size.
instance Prod.instSemiringProd {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : Semiring S] :
Semiring (R × S)

Product of two semirings is a semiring.

Equations
  • One or more equations did not get rendered due to their size.

Product of two NonUnitalCommSemirings is a NonUnitalCommSemiring.

Equations
  • One or more equations did not get rendered due to their size.
instance Prod.instCommSemiringProd {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst : CommSemiring S] :

Product of two commutative semirings is a commutative semiring.

Equations
Equations
  • One or more equations did not get rendered due to their size.
instance Prod.instNonUnitalRingProd {R : Type u_1} {S : Type u_2} [inst : NonUnitalRing R] [inst : NonUnitalRing S] :
Equations
  • One or more equations did not get rendered due to their size.
instance Prod.instNonAssocRingProd {R : Type u_1} {S : Type u_2} [inst : NonAssocRing R] [inst : NonAssocRing S] :
Equations
  • One or more equations did not get rendered due to their size.
instance Prod.instRingProd {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst : Ring S] :
Ring (R × S)

Product of two rings is a ring.

Equations
  • One or more equations did not get rendered due to their size.
instance Prod.instNonUnitalCommRingProd {R : Type u_1} {S : Type u_2} [inst : NonUnitalCommRing R] [inst : NonUnitalCommRing S] :

Product of two NonUnitalCommRings is a NonUnitalCommRing.

Equations
  • One or more equations did not get rendered due to their size.
instance Prod.instCommRingProd {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst : CommRing S] :
CommRing (R × S)

Product of two commutative rings is a commutative ring.

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

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

Equations
  • One or more equations did not get rendered due to their size.
def NonUnitalRingHom.snd (R : Type u_1) (S : Type u_2) [inst : NonUnitalNonAssocSemiring R] [inst : NonUnitalNonAssocSemiring S] :
R × S →ₙ+* S

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

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem NonUnitalRingHom.coe_fst {R : Type u_1} {S : Type u_2} [inst : NonUnitalNonAssocSemiring R] [inst : NonUnitalNonAssocSemiring S] :
↑(NonUnitalRingHom.fst R S) = Prod.fst
@[simp]
theorem NonUnitalRingHom.coe_snd {R : Type u_1} {S : Type u_2} [inst : NonUnitalNonAssocSemiring R] [inst : NonUnitalNonAssocSemiring S] :
↑(NonUnitalRingHom.snd R S) = Prod.snd
def NonUnitalRingHom.prod {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : NonUnitalNonAssocSemiring R] [inst : NonUnitalNonAssocSemiring S] [inst : NonUnitalNonAssocSemiring T] (f : R →ₙ+* S) (g : R →ₙ+* T) :
R →ₙ+* S × T

Combine two non-unital ring homomorphisms f : R →ₙ+* S→ₙ+* S, g : R →ₙ+* T→ₙ+* T into f.prod g : R →ₙ+* S × T→ₙ+* S × T× T given by (f.prod g) x = (f x, g x)

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem NonUnitalRingHom.prod_apply {R : Type u_3} {S : Type u_1} {T : Type u_2} [inst : NonUnitalNonAssocSemiring R] [inst : NonUnitalNonAssocSemiring S] [inst : NonUnitalNonAssocSemiring T] (f : R →ₙ+* S) (g : R →ₙ+* T) (x : R) :
↑(NonUnitalRingHom.prod f g) x = (f x, g x)
@[simp]
theorem NonUnitalRingHom.coe_prodMap {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [inst : NonUnitalNonAssocSemiring R] [inst : NonUnitalNonAssocSemiring S] [inst : NonUnitalNonAssocSemiring R'] [inst : NonUnitalNonAssocSemiring S'] (f : R →ₙ+* R') (g : S →ₙ+* S') :
def RingHom.fst (R : Type u_1) (S : Type u_2) [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] :
R × S →+* R

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

Equations
  • One or more equations did not get rendered due to their size.
def RingHom.snd (R : Type u_1) (S : Type u_2) [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] :
R × S →+* S

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

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem RingHom.coe_fst {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] :
↑(RingHom.fst R S) = Prod.fst
@[simp]
theorem RingHom.coe_snd {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] :
↑(RingHom.snd R S) = Prod.snd
def RingHom.prod {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] [inst : NonAssocSemiring T] (f : R →+* S) (g : R →+* T) :
R →+* S × T

Combine two ring homomorphisms f : R →+* S→+* S, g : R →+* T→+* T into f.prod g : R →+* S × T→+* S × T× T given by (f.prod g) x = (f x, g x)

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem RingHom.prod_apply {R : Type u_3} {S : Type u_1} {T : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] [inst : NonAssocSemiring T] (f : R →+* S) (g : R →+* T) (x : R) :
↑(RingHom.prod f g) x = (f x, g x)
@[simp]
theorem RingHom.fst_comp_prod {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] [inst : NonAssocSemiring T] (f : R →+* S) (g : R →+* T) :
@[simp]
theorem RingHom.snd_comp_prod {R : Type u_1} {S : Type u_3} {T : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] [inst : NonAssocSemiring T] (f : R →+* S) (g : R →+* T) :
theorem RingHom.prod_unique {R : Type u_1} {S : Type u_3} {T : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] [inst : NonAssocSemiring T] (f : R →+* S × T) :
def RingHom.prodMap {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] [inst : NonAssocSemiring R'] [inst : NonAssocSemiring S'] (f : R →+* R') (g : S →+* S') :
R × S →+* R' × S'

Prod.map as a RingHom.

Equations
theorem RingHom.prodMap_def {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] [inst : NonAssocSemiring R'] [inst : NonAssocSemiring S'] (f : R →+* R') (g : S →+* S') :
@[simp]
theorem RingHom.coe_prodMap {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] [inst : NonAssocSemiring R'] [inst : NonAssocSemiring S'] (f : R →+* R') (g : S →+* S') :
↑(RingHom.prodMap f g) = Prod.map f g
theorem RingHom.prod_comp_prodMap {R : Type u_2} {R' : Type u_4} {S : Type u_3} {S' : Type u_5} {T : Type u_1} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] [inst : NonAssocSemiring R'] [inst : NonAssocSemiring S'] [inst : NonAssocSemiring T] (f : T →+* R) (g : T →+* S) (f' : R →+* R') (g' : S →+* S') :
def RingEquiv.prodComm {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] :
R × S ≃+* S × R

Swapping components as an equivalence of (semi)rings.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem RingEquiv.coe_prod_comm {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] :
RingEquiv.prodComm = Prod.swap
@[simp]
theorem RingEquiv.coe_prod_comm_symm {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] :
↑(RingEquiv.symm RingEquiv.prodComm) = Prod.swap
@[simp]
theorem RingEquiv.fst_comp_coe_prod_comm {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] :
RingHom.comp (RingHom.fst S R) RingEquiv.prodComm = RingHom.snd R S
@[simp]
theorem RingEquiv.snd_comp_coe_prod_comm {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] :
RingHom.comp (RingHom.snd S R) RingEquiv.prodComm = RingHom.fst R S
@[simp]
theorem RingEquiv.prodZeroRing_apply (R : Type u_1) (S : Type u_2) [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] [inst : Subsingleton S] (x : R) :
↑(RingEquiv.prodZeroRing R S) x = (x, 0)
@[simp]
theorem RingEquiv.prodZeroRing_symm_apply (R : Type u_1) (S : Type u_2) [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] [inst : Subsingleton S] (self : R × S) :
↑(RingEquiv.symm (RingEquiv.prodZeroRing R S)) self = self.fst
def RingEquiv.prodZeroRing (R : Type u_1) (S : Type u_2) [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] [inst : Subsingleton S] :
R ≃+* R × S

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

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem RingEquiv.zeroRingProd_apply (R : Type u_1) (S : Type u_2) [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] [inst : Subsingleton S] (x : R) :
↑(RingEquiv.zeroRingProd R S) x = (0, x)
@[simp]
theorem RingEquiv.zeroRingProd_symm_apply (R : Type u_1) (S : Type u_2) [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] [inst : Subsingleton S] (self : S × R) :
↑(RingEquiv.symm (RingEquiv.zeroRingProd R S)) self = self.snd
def RingEquiv.zeroRingProd (R : Type u_1) (S : Type u_2) [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] [inst : Subsingleton S] :
R ≃+* S × R

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

Equations
  • One or more equations did not get rendered due to their size.
theorem false_of_nontrivial_of_product_domain (R : Type u_1) (S : Type u_2) [inst : Ring R] [inst : Ring S] [inst : IsDomain (R × S)] [inst : Nontrivial R] [inst : Nontrivial S] :

The product of two nontrivial rings is not a domain

Order #

instance instOrderedSemiringProd {α : Type u_1} {β : Type u_2} [inst : OrderedSemiring α] [inst : OrderedSemiring β] :
Equations
  • One or more equations did not get rendered due to their size.
instance instOrderedCommSemiringProd {α : Type u_1} {β : Type u_2} [inst : OrderedCommSemiring α] [inst : OrderedCommSemiring β] :
Equations
  • One or more equations did not get rendered due to their size.
instance instOrderedRingProd {α : Type u_1} {β : Type u_2} [inst : OrderedRing α] [inst : OrderedRing β] :
OrderedRing (α × β)
Equations
  • One or more equations did not get rendered due to their size.
instance instOrderedCommRingProd {α : Type u_1} {β : Type u_2} [inst : OrderedCommRing α] [inst : OrderedCommRing β] :
Equations