mathlib3 documentation

algebra.ring.prod

Semiring, ring etc structures on R × S #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 and similarly for non_unital_ring_homs:

source
@[protected, instance]
def prod.distrib {R : Type u_3} {S : Type u_5} [distrib R] [distrib S] :
distrib (R × S)

Product of two distributive types is distributive.

Equations
source
@[protected, instance]
def prod.non_unital_non_assoc_semiring {R : Type u_3} {S : Type u_5} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] :
non_unital_non_assoc_semiring (R × S)

Product of two non_unital_non_assoc_semirings is a non_unital_non_assoc_semiring.

Equations
source
@[protected, instance]
def prod.non_unital_semiring {R : Type u_3} {S : Type u_5} [non_unital_semiring R] [non_unital_semiring S] :
non_unital_semiring (R × S)

Product of two non_unital_semirings is a non_unital_semiring.

Equations
source
@[protected, instance]
def prod.non_assoc_semiring {R : Type u_3} {S : Type u_5} [non_assoc_semiring R] [non_assoc_semiring S] :
non_assoc_semiring (R × S)

Product of two non_assoc_semirings is a non_assoc_semiring.

Equations
source
@[protected, instance]
def prod.semiring {R : Type u_3} {S : Type u_5} [semiring R] [semiring S] :
semiring (R × S)

Product of two semirings is a semiring.

Equations
source
@[protected, instance]
def prod.non_unital_comm_semiring {R : Type u_3} {S : Type u_5} [non_unital_comm_semiring R] [non_unital_comm_semiring S] :
non_unital_comm_semiring (R × S)

Product of two non_unital_comm_semirings is a non_unital_comm_semiring.

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

Product of two commutative semirings is a commutative semiring.

Equations
source
@[protected, instance]
def prod.non_unital_non_assoc_ring {R : Type u_3} {S : Type u_5} [non_unital_non_assoc_ring R] [non_unital_non_assoc_ring S] :
non_unital_non_assoc_ring (R × S)
Equations
source
@[protected, instance]
def prod.non_unital_ring {R : Type u_3} {S : Type u_5} [non_unital_ring R] [non_unital_ring S] :
non_unital_ring (R × S)
Equations
source
@[protected, instance]
def prod.non_assoc_ring {R : Type u_3} {S : Type u_5} [non_assoc_ring R] [non_assoc_ring S] :
non_assoc_ring (R × S)
Equations
source
@[protected, instance]
def prod.ring {R : Type u_3} {S : Type u_5} [ring R] [ring S] :
ring (R × S)

Product of two rings is a ring.

Equations
source
@[protected, instance]
def prod.non_unital_comm_ring {R : Type u_3} {S : Type u_5} [non_unital_comm_ring R] [non_unital_comm_ring S] :
non_unital_comm_ring (R × S)

Product of two non_unital_comm_rings is a non_unital_comm_ring.

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

Product of two commutative rings is a commutative ring.

Equations
source
def non_unital_ring_hom.fst (R : Type u_3) (S : Type u_5) [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] :
R × S →ₙ+* R

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

Equations
source
def non_unital_ring_hom.snd (R : Type u_3) (S : Type u_5) [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] :
R × S →ₙ+* S

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

Equations
source
@[simp]
theorem non_unital_ring_hom.coe_fst {R : Type u_3} {S : Type u_5} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] :
⇑(non_unital_ring_hom.fst R S) = prod.fst
source
@[simp]
theorem non_unital_ring_hom.coe_snd {R : Type u_3} {S : Type u_5} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] :
⇑(non_unital_ring_hom.snd R S) = prod.snd
source
@[protected]
def non_unital_ring_hom.prod {R : Type u_3} {S : Type u_5} {T : Type u_7} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] [non_unital_non_assoc_semiring 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)

Equations
source
@[simp]
theorem non_unital_ring_hom.prod_apply {R : Type u_3} {S : Type u_5} {T : Type u_7} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] [non_unital_non_assoc_semiring T] (f : R →ₙ+* S) (g : R →ₙ+* T) (x : R) :
⇑(f.prod g) x = (⇑f x, ⇑g x)
source
@[simp]
theorem non_unital_ring_hom.fst_comp_prod {R : Type u_3} {S : Type u_5} {T : Type u_7} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] [non_unital_non_assoc_semiring T] (f : R →ₙ+* S) (g : R →ₙ+* T) :
(non_unital_ring_hom.fst S T).comp (f.prod g) = f
source
@[simp]
theorem non_unital_ring_hom.snd_comp_prod {R : Type u_3} {S : Type u_5} {T : Type u_7} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] [non_unital_non_assoc_semiring T] (f : R →ₙ+* S) (g : R →ₙ+* T) :
(non_unital_ring_hom.snd S T).comp (f.prod g) = g
source
theorem non_unital_ring_hom.prod_unique {R : Type u_3} {S : Type u_5} {T : Type u_7} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] [non_unital_non_assoc_semiring T] (f : R →ₙ+* S × T) :
((non_unital_ring_hom.fst S T).comp f).prod ((non_unital_ring_hom.snd S T).comp f) = f
source
def non_unital_ring_hom.prod_map {R : Type u_3} {R' : Type u_4} {S : Type u_5} {S' : Type u_6} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] [non_unital_non_assoc_semiring R'] [non_unital_non_assoc_semiring S'] (f : R →ₙ+* R') (g : S →ₙ+* S') :
R × S →ₙ+* R' × S'

prod.map as a non_unital_ring_hom.

Equations
source
theorem non_unital_ring_hom.prod_map_def {R : Type u_3} {R' : Type u_4} {S : Type u_5} {S' : Type u_6} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] [non_unital_non_assoc_semiring R'] [non_unital_non_assoc_semiring S'] (f : R →ₙ+* R') (g : S →ₙ+* S') :
f.prod_map g = (f.comp (non_unital_ring_hom.fst R S)).prod (g.comp (non_unital_ring_hom.snd R S))
source
@[simp]
theorem non_unital_ring_hom.coe_prod_map {R : Type u_3} {R' : Type u_4} {S : Type u_5} {S' : Type u_6} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] [non_unital_non_assoc_semiring R'] [non_unital_non_assoc_semiring S'] (f : R →ₙ+* R') (g : S →ₙ+* S') :
⇑(f.prod_map g) = prod.map ⇑f ⇑g
source
theorem non_unital_ring_hom.prod_comp_prod_map {R : Type u_3} {R' : Type u_4} {S : Type u_5} {S' : Type u_6} {T : Type u_7} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] [non_unital_non_assoc_semiring R'] [non_unital_non_assoc_semiring S'] [non_unital_non_assoc_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_hom.fst (R : Type u_3) (S : Type u_5) [non_assoc_semiring R] [non_assoc_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_3) (S : Type u_5) [non_assoc_semiring R] [non_assoc_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_3} {S : Type u_5} [non_assoc_semiring R] [non_assoc_semiring S] :
⇑(ring_hom.fst R S) = prod.fst
source
@[simp]
theorem ring_hom.coe_snd {R : Type u_3} {S : Type u_5} [non_assoc_semiring R] [non_assoc_semiring S] :
⇑(ring_hom.snd R S) = prod.snd
source
@[protected]
def ring_hom.prod {R : Type u_3} {S : Type u_5} {T : Type u_7} [non_assoc_semiring R] [non_assoc_semiring S] [non_assoc_semiring 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)

Equations
source
@[simp]
theorem ring_hom.prod_apply {R : Type u_3} {S : Type u_5} {T : Type u_7} [non_assoc_semiring R] [non_assoc_semiring S] [non_assoc_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_3} {S : Type u_5} {T : Type u_7} [non_assoc_semiring R] [non_assoc_semiring S] [non_assoc_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_3} {S : Type u_5} {T : Type u_7} [non_assoc_semiring R] [non_assoc_semiring S] [non_assoc_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_3} {S : Type u_5} {T : Type u_7} [non_assoc_semiring R] [non_assoc_semiring S] [non_assoc_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_3} {R' : Type u_4} {S : Type u_5} {S' : Type u_6} [non_assoc_semiring R] [non_assoc_semiring S] [non_assoc_semiring R'] [non_assoc_semiring S'] (f : R →+* R') (g : S →+* S') :
R × S →+* R' × S'

prod.map as a ring_hom.

Equations
source
theorem ring_hom.prod_map_def {R : Type u_3} {R' : Type u_4} {S : Type u_5} {S' : Type u_6} [non_assoc_semiring R] [non_assoc_semiring S] [non_assoc_semiring R'] [non_assoc_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_3} {R' : Type u_4} {S : Type u_5} {S' : Type u_6} [non_assoc_semiring R] [non_assoc_semiring S] [non_assoc_semiring R'] [non_assoc_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_3} {R' : Type u_4} {S : Type u_5} {S' : Type u_6} {T : Type u_7} [non_assoc_semiring R] [non_assoc_semiring S] [non_assoc_semiring R'] [non_assoc_semiring S'] [non_assoc_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_3} {S : Type u_5} [non_assoc_semiring R] [non_assoc_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_3} {S : Type u_5} [non_assoc_semiring R] [non_assoc_semiring S] :
⇑ring_equiv.prod_comm = prod.swap
source
@[simp]
theorem ring_equiv.coe_prod_comm_symm {R : Type u_3} {S : Type u_5} [non_assoc_semiring R] [non_assoc_semiring S] :
⇑(ring_equiv.prod_comm.symm) = prod.swap
source
@[simp]
theorem ring_equiv.fst_comp_coe_prod_comm {R : Type u_3} {S : Type u_5} [non_assoc_semiring R] [non_assoc_semiring S] :
(ring_hom.fst S R).comp ↑ring_equiv.prod_comm = ring_hom.snd R S
source
@[simp]
theorem ring_equiv.snd_comp_coe_prod_comm {R : Type u_3} {S : Type u_5} [non_assoc_semiring R] [non_assoc_semiring S] :
(ring_hom.snd S R).comp ↑ring_equiv.prod_comm = ring_hom.fst R S
source
@[simp]
theorem ring_equiv.prod_prod_prod_comm_apply (R : Type u_3) (R' : Type u_4) (S : Type u_5) (S' : Type u_6) [non_assoc_semiring R] [non_assoc_semiring S] [non_assoc_semiring R'] [non_assoc_semiring S'] (rrss : (R × R') × S × S') :
⇑(ring_equiv.prod_prod_prod_comm R R' S S') rrss = ((rrss.fst.fst, rrss.snd.fst), rrss.fst.snd, rrss.snd.snd)
source
def ring_equiv.prod_prod_prod_comm (R : Type u_3) (R' : Type u_4) (S : Type u_5) (S' : Type u_6) [non_assoc_semiring R] [non_assoc_semiring S] [non_assoc_semiring R'] [non_assoc_semiring S'] :
(R × R') × S × S' ≃+* (R × S) × R' × S'

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

Equations
source
@[simp]
theorem ring_equiv.prod_prod_prod_comm_symm (R : Type u_3) (R' : Type u_4) (S : Type u_5) (S' : Type u_6) [non_assoc_semiring R] [non_assoc_semiring S] [non_assoc_semiring R'] [non_assoc_semiring S'] :
(ring_equiv.prod_prod_prod_comm R R' S S').symm = ring_equiv.prod_prod_prod_comm R S R' S'
source
@[simp]
theorem ring_equiv.prod_prod_prod_comm_to_add_equiv (R : Type u_3) (R' : Type u_4) (S : Type u_5) (S' : Type u_6) [non_assoc_semiring R] [non_assoc_semiring S] [non_assoc_semiring R'] [non_assoc_semiring S'] :
(ring_equiv.prod_prod_prod_comm R R' S S').to_add_equiv = add_equiv.prod_prod_prod_comm R R' S S'
source
@[simp]
theorem ring_equiv.prod_prod_prod_comm_to_mul_equiv (R : Type u_3) (R' : Type u_4) (S : Type u_5) (S' : Type u_6) [non_assoc_semiring R] [non_assoc_semiring S] [non_assoc_semiring R'] [non_assoc_semiring S'] :
(ring_equiv.prod_prod_prod_comm R R' S S').to_mul_equiv = mul_equiv.prod_prod_prod_comm R R' S S'
source
@[simp]
theorem ring_equiv.prod_prod_prod_comm_to_equiv (R : Type u_3) (R' : Type u_4) (S : Type u_5) (S' : Type u_6) [non_assoc_semiring R] [non_assoc_semiring S] [non_assoc_semiring R'] [non_assoc_semiring S'] :
(ring_equiv.prod_prod_prod_comm R R' S S').to_equiv = equiv.prod_prod_prod_comm R R' S S'
source
def ring_equiv.prod_zero_ring (R : Type u_3) (S : Type u_5) [non_assoc_semiring R] [non_assoc_semiring S] [subsingleton S] :
R ≃+* R × S

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

Equations
source
@[simp]
theorem ring_equiv.prod_zero_ring_symm_apply (R : Type u_3) (S : Type u_5) [non_assoc_semiring R] [non_assoc_semiring S] [subsingleton S] (self : R × S) :
⇑((ring_equiv.prod_zero_ring R S).symm) self = self.fst
source
@[simp]
theorem ring_equiv.prod_zero_ring_apply (R : Type u_3) (S : Type u_5) [non_assoc_semiring R] [non_assoc_semiring S] [subsingleton S] (x : R) :
⇑(ring_equiv.prod_zero_ring R S) x = (x, 0)
source
def ring_equiv.zero_ring_prod (R : Type u_3) (S : Type u_5) [non_assoc_semiring R] [non_assoc_semiring S] [subsingleton S] :
R ≃+* S × R

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

Equations
source
@[simp]
theorem ring_equiv.zero_ring_prod_apply (R : Type u_3) (S : Type u_5) [non_assoc_semiring R] [non_assoc_semiring S] [subsingleton S] (x : R) :
⇑(ring_equiv.zero_ring_prod R S) x = (0, x)
source
@[simp]
theorem ring_equiv.zero_ring_prod_symm_apply (R : Type u_3) (S : Type u_5) [non_assoc_semiring R] [non_assoc_semiring S] [subsingleton S] (self : S × R) :
⇑((ring_equiv.zero_ring_prod R S).symm) self = self.snd
source
theorem false_of_nontrivial_of_product_domain (R : Type u_1) (S : Type u_2) [ring R] [ring S] [is_domain (R × S)] [nontrivial R] [nontrivial S] :
false

The product of two nontrivial rings is not a domain

Order #

source
@[protected, instance]
def prod.ordered_semiring {α : Type u_1} {β : Type u_2} [ordered_semiring α] [ordered_semiring β] :
ordered_semiring (α × β)
Equations
source
@[protected, instance]
def prod.ordered_comm_semiring {α : Type u_1} {β : Type u_2} [ordered_comm_semiring α] [ordered_comm_semiring β] :
ordered_comm_semiring (α × β)
Equations
source
@[protected, instance]
def prod.ordered_ring {α : Type u_1} {β : Type u_2} [ordered_ring α] [ordered_ring β] :
ordered_ring (α × β)
Equations
source
@[protected, instance]
def prod.ordered_comm_ring {α : Type u_1} {β : Type u_2} [ordered_comm_ring α] [ordered_comm_ring β] :
ordered_comm_ring (α × β)
Equations