mathlib documentation

algebra.ring.prod

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 ring_homs:

source
@[instance]
def prod.semiring {R : Type u_1} {S : Type u_3} [semiring R] [semiring S] :
semiring (R × S)

Product of two semirings is a semiring.

Equations
source
@[instance]
def prod.comm_semiring {R : Type u_1} {S : Type u_3} [comm_semiring R] [comm_semiring S] :
comm_semiring (R × S)

Product of two commutative semirings is a commutative semiring.

Equations
source
@[instance]
def prod.ring {R : Type u_1} {S : Type u_3} [ring R] [ring S] :
ring (R × S)

Product of two rings is a ring.

Equations
source
@[instance]
def prod.comm_ring {R : Type u_1} {S : Type u_3} [comm_ring R] [comm_ring S] :
comm_ring (R × S)

Product of two commutative rings is a commutative ring.

Equations
source
def ring_hom.fst (R : Type u_1) (S : Type u_3) [semiring R] [semiring S] :
R × S →+* R

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

Equations
source
def ring_hom.snd (R : Type u_1) (S : Type u_3) [semiring R] [semiring S] :
R × S →+* S

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

Equations
source
@[simp]
theorem ring_hom.coe_fst {R : Type u_1} {S : Type u_3} [semiring R] [semiring S] :
⇑(ring_hom.fst R S) = prod.fst

source
@[simp]
theorem ring_hom.coe_snd {R : Type u_1} {S : Type u_3} [semiring R] [semiring S] :
⇑(ring_hom.snd R S) = prod.snd

source
def ring_hom.prod {R : Type u_1} {S : Type u_3} {T : Type u_5} [semiring R] [semiring S] [semiring T] :
(R →+* S) → (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)

Equations
source
@[simp]
theorem ring_hom.prod_apply {R : Type u_1} {S : Type u_3} {T : Type u_5} [semiring R] [semiring S] [semiring T] (f : R →+* S) (g : R →+* T) (x : R) :
⇑(f.prod g) x = (⇑f x, ⇑g x)

source
@[simp]
theorem ring_hom.fst_comp_prod {R : Type u_1} {S : Type u_3} {T : Type u_5} [semiring R] [semiring S] [semiring T] (f : R →+* S) (g : R →+* T) :
(ring_hom.fst S T).comp (f.prod g) = f

source
@[simp]
theorem ring_hom.snd_comp_prod {R : Type u_1} {S : Type u_3} {T : Type u_5} [semiring R] [semiring S] [semiring T] (f : R →+* S) (g : R →+* T) :
(ring_hom.snd S T).comp (f.prod g) = g

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

source
def ring_hom.prod_map {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [semiring R] [semiring S] [semiring R'] [semiring S'] :
(R →+* R') → (S →+* S') → R × S →* R' × S'

prod.map as a ring_hom.

Equations
source
theorem ring_hom.prod_map_def {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [semiring R] [semiring S] [semiring R'] [semiring S'] (f : R →+* R') (g : S →+* S') :
f.prod_map g = ↑((f.comp (ring_hom.fst R S)).prod (g.comp (ring_hom.snd R S)))

source
@[simp]
theorem ring_hom.coe_prod_map {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [semiring R] [semiring S] [semiring R'] [semiring S'] (f : R →+* R') (g : S →+* S') :
⇑(f.prod_map g) = prod.map ⇑f ⇑g

source
theorem ring_hom.prod_comp_prod_map {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} {T : Type u_5} [semiring R] [semiring S] [semiring R'] [semiring S'] [semiring T] (f : T →* R) (g : T →* S) (f' : R →* R') (g' : S →* S') :
(f'.prod_map g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)

source
def ring_equiv.prod_comm (R : Type u_1) (S : Type u_3) [semiring R] [semiring S] :
R × S ≃+* S × R

Swapping components as an equivalence of (semi)rings.

Equations
source
@[simp]
theorem ring_equiv.coe_prod_comm (R : Type u_1) (S : Type u_3) [semiring R] [semiring S] :
⇑(ring_equiv.prod_comm R S) = prod.swap

source
@[simp]
theorem ring_equiv.coe_prod_comm_symm (R : Type u_1) (S : Type u_3) [semiring R] [semiring S] :
⇑((ring_equiv.prod_comm R S).symm) = prod.swap

source
@[simp]
theorem ring_equiv.coe_coe_prod_comm (R : Type u_1) (S : Type u_3) [semiring R] [semiring S] :
⇑↑(ring_equiv.prod_comm R S) = prod.swap

source
@[simp]
theorem ring_equiv.coe_coe_prod_comm_symm (R : Type u_1) (S : Type u_3) [semiring R] [semiring S] :
⇑↑((ring_equiv.prod_comm R S).symm) = prod.swap

source
@[simp]
theorem ring_equiv.fst_comp_coe_prod_comm (R : Type u_1) (S : Type u_3) [semiring R] [semiring S] :
(ring_hom.fst S R).comp ↑(ring_equiv.prod_comm R S) = ring_hom.snd R S

source
@[simp]
theorem ring_equiv.snd_comp_coe_prod_comm (R : Type u_1) (S : Type u_3) [semiring R] [semiring S] :
(ring_hom.snd S R).comp ↑(ring_equiv.prod_comm R S) = ring_hom.fst R S