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:
@[protected, instance]
Product of two distributive types is distributive.
Equations
- prod.distrib = {mul := has_mul.mul prod.has_mul, add := has_add.add prod.has_add, left_distrib := _, right_distrib := _}
@[protected, instance]
def
prod.non_unital_non_assoc_semiring
{R : Type u_1}
{S : Type u_3}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S] :
Product of two non_unital_non_assoc_semirings is a non_unital_non_assoc_semiring.
Equations
- prod.non_unital_non_assoc_semiring = {add := add_comm_monoid.add prod.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero prod.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul prod.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := mul_zero_class.mul prod.mul_zero_class, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _}
@[protected, instance]
def
prod.non_unital_semiring
{R : Type u_1}
{S : Type u_3}
[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
- prod.non_unital_semiring = {add := non_unital_non_assoc_semiring.add prod.non_unital_non_assoc_semiring, add_assoc := _, zero := non_unital_non_assoc_semiring.zero prod.non_unital_non_assoc_semiring, zero_add := _, add_zero := _, nsmul := non_unital_non_assoc_semiring.nsmul prod.non_unital_non_assoc_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := non_unital_non_assoc_semiring.mul prod.non_unital_non_assoc_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _}
@[protected, instance]
def
prod.non_assoc_semiring
{R : Type u_1}
{S : Type u_3}
[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
- prod.non_assoc_semiring = {add := non_unital_non_assoc_semiring.add prod.non_unital_non_assoc_semiring, add_assoc := _, zero := non_unital_non_assoc_semiring.zero prod.non_unital_non_assoc_semiring, zero_add := _, add_zero := _, nsmul := non_unital_non_assoc_semiring.nsmul prod.non_unital_non_assoc_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := non_unital_non_assoc_semiring.mul prod.non_unital_non_assoc_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, one := mul_one_class.one prod.mul_one_class, one_mul := _, mul_one := _}
@[protected, instance]
Product of two semirings is a semiring.
Equations
- prod.semiring = {add := add_comm_monoid.add prod.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero prod.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul prod.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := monoid_with_zero.mul prod.monoid_with_zero, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := monoid_with_zero.one prod.monoid_with_zero, one_mul := _, mul_one := _, npow := monoid_with_zero.npow prod.monoid_with_zero, npow_zero' := _, npow_succ' := _}
@[protected, 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
- prod.comm_semiring = {add := semiring.add prod.semiring, add_assoc := _, zero := semiring.zero prod.semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul prod.semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semiring.mul prod.semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := semiring.one prod.semiring, one_mul := _, mul_one := _, npow := semiring.npow prod.semiring, npow_zero' := _, npow_succ' := _, mul_comm := _}
@[protected, instance]
def
prod.non_unital_non_assoc_ring
{R : Type u_1}
{S : Type u_3}
[non_unital_non_assoc_ring R]
[non_unital_non_assoc_ring S] :
non_unital_non_assoc_ring (R × S)
Equations
- prod.non_unital_non_assoc_ring = {add := add_comm_group.add prod.add_comm_group, add_assoc := _, zero := add_comm_group.zero prod.add_comm_group, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul prod.add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg prod.add_comm_group, sub := add_comm_group.sub prod.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul prod.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := non_unital_non_assoc_semiring.mul prod.non_unital_non_assoc_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _}
@[protected, instance]
Product of two rings is a ring.
Equations
- prod.ring = {add := add_comm_group.add prod.add_comm_group, add_assoc := _, zero := add_comm_group.zero prod.add_comm_group, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul prod.add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg prod.add_comm_group, sub := add_comm_group.sub prod.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul prod.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := semiring.mul prod.semiring, mul_assoc := _, one := semiring.one prod.semiring, one_mul := _, mul_one := _, npow := semiring.npow prod.semiring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}
@[protected, instance]
Product of two commutative rings is a commutative ring.
Equations
- prod.comm_ring = {add := ring.add prod.ring, add_assoc := _, zero := ring.zero prod.ring, zero_add := _, add_zero := _, nsmul := ring.nsmul prod.ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg prod.ring, sub := ring.sub prod.ring, sub_eq_add_neg := _, zsmul := ring.zsmul prod.ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := ring.mul prod.ring, mul_assoc := _, one := ring.one prod.ring, one_mul := _, mul_one := _, npow := ring.npow prod.ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}
Given semirings R, S, the natural projection homomorphism from R × S to R.
Given semirings R, S, the natural projection homomorphism from R × S to S.
@[simp]
theorem
ring_hom.coe_fst
{R : Type u_1}
{S : Type u_3}
[non_assoc_semiring R]
[non_assoc_semiring S] :
⇑(ring_hom.fst R S) = prod.fst
@[simp]
theorem
ring_hom.coe_snd
{R : Type u_1}
{S : Type u_3}
[non_assoc_semiring R]
[non_assoc_semiring S] :
⇑(ring_hom.snd R S) = prod.snd
@[protected]
def
ring_hom.prod
{R : Type u_1}
{S : Type u_3}
{T : Type u_5}
[non_assoc_semiring R]
[non_assoc_semiring S]
[non_assoc_semiring T]
(f : R →+* S)
(g : R →+* 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
ring_hom.prod_apply
{R : Type u_1}
{S : Type u_3}
{T : Type u_5}
[non_assoc_semiring R]
[non_assoc_semiring S]
[non_assoc_semiring T]
(f : R →+* S)
(g : R →+* T)
(x : R) :
@[simp]
theorem
ring_hom.fst_comp_prod
{R : Type u_1}
{S : Type u_3}
{T : Type u_5}
[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
@[simp]
theorem
ring_hom.snd_comp_prod
{R : Type u_1}
{S : Type u_3}
{T : Type u_5}
[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
theorem
ring_hom.prod_unique
{R : Type u_1}
{S : Type u_3}
{T : Type u_5}
[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
def
ring_hom.prod_map
{R : Type u_1}
{R' : Type u_2}
{S : Type u_3}
{S' : Type u_4}
[non_assoc_semiring R]
[non_assoc_semiring S]
[non_assoc_semiring R']
[non_assoc_semiring S']
(f : R →+* R')
(g : S →+* S') :
Equations
- f.prod_map g = ↑((f.comp (ring_hom.fst R S)).prod (g.comp (ring_hom.snd R S)))
theorem
ring_hom.prod_map_def
{R : Type u_1}
{R' : Type u_2}
{S : Type u_3}
{S' : Type u_4}
[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)))
@[simp]
theorem
ring_hom.coe_prod_map
{R : Type u_1}
{R' : Type u_2}
{S : Type u_3}
{S' : Type u_4}
[non_assoc_semiring R]
[non_assoc_semiring S]
[non_assoc_semiring R']
[non_assoc_semiring S']
(f : R →+* R')
(g : S →+* S') :
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}
[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') :
def
ring_equiv.prod_comm
{R : Type u_1}
{S : Type u_3}
[non_assoc_semiring R]
[non_assoc_semiring S] :
Swapping components as an equivalence of (semi)rings.
Equations
- ring_equiv.prod_comm = {to_fun := add_equiv.prod_comm.to_fun, inv_fun := add_equiv.prod_comm.inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}
@[simp]
theorem
ring_equiv.coe_prod_comm
{R : Type u_1}
{S : Type u_3}
[non_assoc_semiring R]
[non_assoc_semiring S] :
@[simp]
theorem
ring_equiv.coe_prod_comm_symm
{R : Type u_1}
{S : Type u_3}
[non_assoc_semiring R]
[non_assoc_semiring S] :
@[simp]
theorem
ring_equiv.fst_comp_coe_prod_comm
{R : Type u_1}
{S : Type u_3}
[non_assoc_semiring R]
[non_assoc_semiring S] :
(ring_hom.fst S R).comp ↑ring_equiv.prod_comm = ring_hom.snd R S
@[simp]
theorem
ring_equiv.snd_comp_coe_prod_comm
{R : Type u_1}
{S : Type u_3}
[non_assoc_semiring R]
[non_assoc_semiring S] :
(ring_hom.snd S R).comp ↑ring_equiv.prod_comm = ring_hom.fst R S
def
ring_equiv.prod_zero_ring
(R : Type u_1)
(S : Type u_3)
[non_assoc_semiring R]
[non_assoc_semiring S]
[subsingleton S] :
A ring R is isomorphic to R × S when S is the zero ring
@[simp]
theorem
ring_equiv.prod_zero_ring_symm_apply
(R : Type u_1)
(S : Type u_3)
[non_assoc_semiring R]
[non_assoc_semiring S]
[subsingleton S]
(self : R × S) :
⇑((ring_equiv.prod_zero_ring R S).symm) self = self.fst
@[simp]
theorem
ring_equiv.prod_zero_ring_apply
(R : Type u_1)
(S : Type u_3)
[non_assoc_semiring R]
[non_assoc_semiring S]
[subsingleton S]
(x : R) :
⇑(ring_equiv.prod_zero_ring R S) x = (x, 0)
def
ring_equiv.zero_ring_prod
(R : Type u_1)
(S : Type u_3)
[non_assoc_semiring R]
[non_assoc_semiring S]
[subsingleton S] :
A ring R is isomorphic to S × R when S is the zero ring
@[simp]
theorem
ring_equiv.zero_ring_prod_apply
(R : Type u_1)
(S : Type u_3)
[non_assoc_semiring R]
[non_assoc_semiring S]
[subsingleton S]
(x : R) :
⇑(ring_equiv.zero_ring_prod R S) x = (0, x)
@[simp]
theorem
ring_equiv.zero_ring_prod_symm_apply
(R : Type u_1)
(S : Type u_3)
[non_assoc_semiring R]
[non_assoc_semiring S]
[subsingleton S]
(self : S × R) :
⇑((ring_equiv.zero_ring_prod R S).symm) self = self.snd
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] :
The product of two nontrivial rings is not a domain