# mathlibdocumentation

algebra.group.prod

# Monoid, group etc structures on M × N

In this file we define one-binop (monoid, group etc) structures on M × N. We also prove trivial simp lemmas, and define the following operations on monoid_homs:

• fst M N : M × N →* M, snd M N : M × N →* N: projections prod.fst and prod.snd as monoid_homs;
• inl M N : M →* M × N, inr M N : N →* M × N: inclusions of first/second monoid into the product;
• f.prod g :M →* N × P: sendsxto(f x, g x);
• f.coprod g : M × N →* P: sends (x, y) to f x * g y;
• f.prod_map g : M × N → M' × N': prod.map f g as a monoid_hom, sends (x, y) to (f x, g y).
@[instance]
def prod.has_mul {M : Type u_5} {N : Type u_6} [has_mul M] [has_mul N] :
has_mul (M × N)

Equations
@[instance]

@[simp]
theorem prod.fst_mul {M : Type u_5} {N : Type u_6} [has_mul M] [has_mul N] (p q : M × N) :
(p * q).fst = (p.fst) * q.fst

@[simp]
theorem prod.fst_add {M : Type u_5} {N : Type u_6} [has_add M] [has_add N] (p q : M × N) :
(p + q).fst = p.fst + q.fst

@[simp]
theorem prod.snd_add {M : Type u_5} {N : Type u_6} [has_add M] [has_add N] (p q : M × N) :
(p + q).snd = p.snd + q.snd

@[simp]
theorem prod.snd_mul {M : Type u_5} {N : Type u_6} [has_mul M] [has_mul N] (p q : M × N) :
(p * q).snd = (p.snd) * q.snd

@[simp]
theorem prod.mk_add_mk {M : Type u_5} {N : Type u_6} [has_add M] [has_add N] (a₁ a₂ : M) (b₁ b₂ : N) :
(a₁, b₁) + (a₂, b₂) = (a₁ + a₂, b₁ + b₂)

@[simp]
theorem prod.mk_mul_mk {M : Type u_5} {N : Type u_6} [has_mul M] [has_mul N] (a₁ a₂ : M) (b₁ b₂ : N) :
(a₁, b₁) * (a₂, b₂) = (a₁ * a₂, b₁ * b₂)

@[instance]
def prod.has_one {M : Type u_5} {N : Type u_6} [has_one M] [has_one N] :
has_one (M × N)

Equations
@[instance]
def prod.has_zero {M : Type u_5} {N : Type u_6} [has_zero M] [has_zero N] :
has_zero (M × N)

@[simp]
theorem prod.fst_zero {M : Type u_5} {N : Type u_6} [has_zero M] [has_zero N] :
0.fst = 0

@[simp]
theorem prod.fst_one {M : Type u_5} {N : Type u_6} [has_one M] [has_one N] :
1.fst = 1

@[simp]
theorem prod.snd_one {M : Type u_5} {N : Type u_6} [has_one M] [has_one N] :
1.snd = 1

@[simp]
theorem prod.snd_zero {M : Type u_5} {N : Type u_6} [has_zero M] [has_zero N] :
0.snd = 0

theorem prod.one_eq_mk {M : Type u_5} {N : Type u_6} [has_one M] [has_one N] :
1 = (1, 1)

theorem prod.zero_eq_mk {M : Type u_5} {N : Type u_6} [has_zero M] [has_zero N] :
0 = (0, 0)

@[simp]
theorem prod.mk_eq_zero {M : Type u_5} {N : Type u_6} [has_zero M] [has_zero N] {x : M} {y : N} :
(x, y) = 0 x = 0 y = 0

@[simp]
theorem prod.mk_eq_one {M : Type u_5} {N : Type u_6} [has_one M] [has_one N] {x : M} {y : N} :
(x, y) = 1 x = 1 y = 1

theorem prod.fst_mul_snd {M : Type u_5} {N : Type u_6} [monoid M] [monoid N] (p : M × N) :
(p.fst, 1) * (1, p.snd) = p

theorem prod.fst_add_snd {M : Type u_5} {N : Type u_6} [add_monoid M] [add_monoid N] (p : M × N) :
(p.fst, 0) + (0, p.snd) = p

@[instance]
def prod.has_neg {M : Type u_5} {N : Type u_6} [has_neg M] [has_neg N] :
has_neg (M × N)

@[instance]
def prod.has_inv {M : Type u_5} {N : Type u_6} [has_inv M] [has_inv N] :
has_inv (M × N)

Equations
@[simp]
theorem prod.fst_neg {G : Type u_3} {H : Type u_4} [has_neg G] [has_neg H] (p : G × H) :
(-p).fst = -p.fst

@[simp]
theorem prod.fst_inv {G : Type u_3} {H : Type u_4} [has_inv G] [has_inv H] (p : G × H) :

@[simp]
theorem prod.snd_inv {G : Type u_3} {H : Type u_4} [has_inv G] [has_inv H] (p : G × H) :

@[simp]
theorem prod.snd_neg {G : Type u_3} {H : Type u_4} [has_neg G] [has_neg H] (p : G × H) :
(-p).snd = -p.snd

@[simp]
theorem prod.inv_mk {G : Type u_3} {H : Type u_4} [has_inv G] [has_inv H] (a : G) (b : H) :
(a, b)⁻¹ = (a⁻¹, b⁻¹)

@[simp]
theorem prod.neg_mk {G : Type u_3} {H : Type u_4} [has_neg G] [has_neg H] (a : G) (b : H) :
-(a, b) = (-a, -b)

@[instance]
def prod.has_div {M : Type u_5} {N : Type u_6} [has_div M] [has_div N] :
has_div (M × N)

Equations
@[instance]
def prod.has_sub {M : Type u_5} {N : Type u_6} [has_sub M] [has_sub N] :
has_sub (M × N)

@[simp]
theorem prod.fst_sub {A : Type u_1} {B : Type u_2} [add_group A] [add_group B] (a b : A × B) :
(a - b).fst = a.fst - b.fst

@[simp]
theorem prod.snd_sub {A : Type u_1} {B : Type u_2} [add_group A] [add_group B] (a b : A × B) :
(a - b).snd = a.snd - b.snd

@[simp]
theorem prod.mk_sub_mk {A : Type u_1} {B : Type u_2} [add_group A] [add_group B] (x₁ x₂ : A) (y₁ y₂ : B) :
(x₁, y₁) - (x₂, y₂) = (x₁ - x₂, y₁ - y₂)

@[instance]
def prod.semigroup {M : Type u_5} {N : Type u_6} [semigroup M] [semigroup N] :

Equations
@[instance]
def prod.add_semigroup {M : Type u_5} {N : Type u_6}  :

@[instance]
def prod.monoid {M : Type u_5} {N : Type u_6} [monoid M] [monoid N] :
monoid (M × N)

Equations
@[instance]

@[instance]

@[instance]
def prod.group {G : Type u_3} {H : Type u_4} [group G] [group H] :
group (G × H)

Equations
@[instance]
def prod.add_comm_semigroup {G : Type u_3} {H : Type u_4}  :

@[instance]
def prod.comm_semigroup {G : Type u_3} {H : Type u_4}  :

Equations
@[instance]
def prod.left_cancel_add_semigroup {G : Type u_3} {H : Type u_4}  :

@[instance]
def prod.left_cancel_semigroup {G : Type u_3} {H : Type u_4}  :

Equations
@[instance]
def prod.right_cancel_add_semigroup {G : Type u_3} {H : Type u_4}  :

@[instance]
def prod.right_cancel_semigroup {G : Type u_3} {H : Type u_4}  :

Equations
@[instance]
def prod.add_comm_monoid {M : Type u_5} {N : Type u_6}  :

@[instance]
def prod.comm_monoid {M : Type u_5} {N : Type u_6} [comm_monoid M] [comm_monoid N] :

Equations
@[instance]
def prod.add_comm_group {G : Type u_3} {H : Type u_4}  :

@[instance]
def prod.comm_group {G : Type u_3} {H : Type u_4} [comm_group G] [comm_group H] :

Equations
def monoid_hom.fst (M : Type u_5) (N : Type u_6) [monoid M] [monoid N] :
M × N →* M

Given monoids M, N, the natural projection homomorphism from M × N to M.

Equations
M × N →+ M

Given additive monoids A, B, the natural projection homomorphism from A × B to A

def monoid_hom.snd (M : Type u_5) (N : Type u_6) [monoid M] [monoid N] :
M × N →* N

Given monoids M, N, the natural projection homomorphism from M × N to N.

Equations
M × N →+ N

Given additive monoids A, B, the natural projection homomorphism from A × B to B

def monoid_hom.inl (M : Type u_5) (N : Type u_6) [monoid M] [monoid N] :
M →* M × N

Given monoids M, N, the natural inclusion homomorphism from M to M × N.

Equations
M →+ M × N

Given additive monoids A, B, the natural inclusion homomorphism from A to A × B.

N →+ M × N

Given additive monoids A, B, the natural inclusion homomorphism from B to A × B.

def monoid_hom.inr (M : Type u_5) (N : Type u_6) [monoid M] [monoid N] :
N →* M × N

Given monoids M, N, the natural inclusion homomorphism from N to M × N.

Equations
@[simp]
theorem monoid_hom.coe_fst {M : Type u_5} {N : Type u_6} [monoid M] [monoid N] :

@[simp]

@[simp]

@[simp]
theorem monoid_hom.coe_snd {M : Type u_5} {N : Type u_6} [monoid M] [monoid N] :

@[simp]
theorem monoid_hom.inl_apply {M : Type u_5} {N : Type u_6} [monoid M] [monoid N] (x : M) :
N) x = (x, 1)

@[simp]
theorem add_monoid_hom.inl_apply {M : Type u_5} {N : Type u_6} [add_monoid M] [add_monoid N] (x : M) :
N) x = (x, 0)

@[simp]
theorem monoid_hom.inr_apply {M : Type u_5} {N : Type u_6} [monoid M] [monoid N] (y : N) :
N) y = (1, y)

@[simp]
theorem add_monoid_hom.inr_apply {M : Type u_5} {N : Type u_6} [add_monoid M] [add_monoid N] (y : N) :
N) y = (0, y)

@[simp]
theorem monoid_hom.fst_comp_inl {M : Type u_5} {N : Type u_6} [monoid M] [monoid N] :
N).comp N) =

@[simp]
N).comp N) =

@[simp]
N).comp N) = 0

@[simp]
theorem monoid_hom.snd_comp_inl {M : Type u_5} {N : Type u_6} [monoid M] [monoid N] :
N).comp N) = 1

@[simp]
N).comp N) = 0

@[simp]
theorem monoid_hom.fst_comp_inr {M : Type u_5} {N : Type u_6} [monoid M] [monoid N] :
N).comp N) = 1

@[simp]
N).comp N) =

@[simp]
theorem monoid_hom.snd_comp_inr {M : Type u_5} {N : Type u_6} [monoid M] [monoid N] :
N).comp N) =

def add_monoid_hom.prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_monoid M] [add_monoid N] [add_monoid P] (f : M →+ N) (g : M →+ P) :
M →+ N × P

Combine two add_monoid_homs f : M →+ N, g : M →+ P into f.prod g : M →+ N × P given by (f.prod g) x = (f x, g x)

def monoid_hom.prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [monoid M] [monoid N] [monoid P] (f : M →* N) (g : M →* P) :
M →* N × P

Combine two monoid_homs f : M →* N, g : M →* P into f.prod g : M →* N × P given by (f.prod g) x = (f x, g x)

Equations
@[simp]
theorem monoid_hom.prod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} [monoid M] [monoid N] [monoid P] (f : M →* N) (g : M →* P) (x : M) :
(f.prod g) x = (f x, g x)

@[simp]
theorem add_monoid_hom.prod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_monoid M] [add_monoid N] [add_monoid P] (f : M →+ N) (g : M →+ P) (x : M) :
(f.prod g) x = (f x, g x)

@[simp]
theorem add_monoid_hom.fst_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_monoid M] [add_monoid N] [add_monoid P] (f : M →+ N) (g : M →+ P) :
P).comp (f.prod g) = f

@[simp]
theorem monoid_hom.fst_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [monoid M] [monoid N] [monoid P] (f : M →* N) (g : M →* P) :
P).comp (f.prod g) = f

@[simp]
theorem add_monoid_hom.snd_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_monoid M] [add_monoid N] [add_monoid P] (f : M →+ N) (g : M →+ P) :
P).comp (f.prod g) = g

@[simp]
theorem monoid_hom.snd_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [monoid M] [monoid N] [monoid P] (f : M →* N) (g : M →* P) :
P).comp (f.prod g) = g

@[simp]
theorem monoid_hom.prod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} [monoid M] [monoid N] [monoid P] (f : M →* N × P) :
P).comp f).prod P).comp f) = f

@[simp]
theorem add_monoid_hom.prod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_monoid M] [add_monoid N] [add_monoid P] (f : M →+ N × P) :
P).comp f).prod P).comp f) = f

def add_monoid_hom.prod_map {M : Type u_5} {N : Type u_6} [add_monoid M] [add_monoid N] {M' : Type u_8} {N' : Type u_9} [add_monoid M'] [add_monoid N'] (f : M →+ M') (g : N →+ N') :
M × N →+ M' × N'

prod.map as an add_monoid_hom

def monoid_hom.prod_map {M : Type u_5} {N : Type u_6} [monoid M] [monoid N] {M' : Type u_8} {N' : Type u_9} [monoid M'] [monoid N'] (f : M →* M') (g : N →* N') :
M × N →* M' × N'

prod.map as a monoid_hom.

Equations
theorem add_monoid_hom.prod_map_def {M : Type u_5} {N : Type u_6} [add_monoid M] [add_monoid N] {M' : Type u_8} {N' : Type u_9} [add_monoid M'] [add_monoid N'] (f : M →+ M') (g : N →+ N') :
f.prod_map g = (f.comp N)).prod (g.comp N))

theorem monoid_hom.prod_map_def {M : Type u_5} {N : Type u_6} [monoid M] [monoid N] {M' : Type u_8} {N' : Type u_9} [monoid M'] [monoid N'] (f : M →* M') (g : N →* N') :
f.prod_map g = (f.comp N)).prod (g.comp N))

@[simp]
theorem monoid_hom.coe_prod_map {M : Type u_5} {N : Type u_6} [monoid M] [monoid N] {M' : Type u_8} {N' : Type u_9} [monoid M'] [monoid N'] (f : M →* M') (g : N →* N') :

@[simp]
theorem add_monoid_hom.coe_prod_map {M : Type u_5} {N : Type u_6} [add_monoid M] [add_monoid N] {M' : Type u_8} {N' : Type u_9} [add_monoid M'] [add_monoid N'] (f : M →+ M') (g : N →+ N') :

theorem add_monoid_hom.prod_comp_prod_map {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_monoid M] [add_monoid N] {M' : Type u_8} {N' : Type u_9} [add_monoid M'] [add_monoid N'] [add_monoid P] (f : P →+ M) (g : P →+ N) (f' : M →+ M') (g' : N →+ N') :
(f'.prod_map g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)

theorem monoid_hom.prod_comp_prod_map {M : Type u_5} {N : Type u_6} {P : Type u_7} [monoid M] [monoid N] {M' : Type u_8} {N' : Type u_9} [monoid M'] [monoid N'] [monoid P] (f : P →* M) (g : P →* N) (f' : M →* M') (g' : N →* N') :
(f'.prod_map g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)

def monoid_hom.coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [monoid M] [monoid N] [comm_monoid P] (f : M →* P) (g : N →* P) :
M × N →* P

Coproduct of two monoid_homs with the same codomain: f.coprod g (p : M × N) = f p.1 * g p.2.

Equations
def add_monoid_hom.coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_monoid M] [add_monoid N] (f : M →+ P) (g : N →+ P) :
M × N →+ P

Coproduct of two add_monoid_homs with the same codomain: f.coprod g (p : M × N) = f p.1 + g p.2.

@[simp]
theorem monoid_hom.coprod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} [monoid M] [monoid N] [comm_monoid P] (f : M →* P) (g : N →* P) (p : M × N) :
(f.coprod g) p = (f p.fst) * g p.snd

@[simp]
theorem add_monoid_hom.coprod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_monoid M] [add_monoid N] (f : M →+ P) (g : N →+ P) (p : M × N) :
(f.coprod g) p = f p.fst + g p.snd

@[simp]
theorem add_monoid_hom.coprod_comp_inl {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_monoid M] [add_monoid N] (f : M →+ P) (g : N →+ P) :
(f.coprod g).comp N) = f

@[simp]
theorem monoid_hom.coprod_comp_inl {M : Type u_5} {N : Type u_6} {P : Type u_7} [monoid M] [monoid N] [comm_monoid P] (f : M →* P) (g : N →* P) :
(f.coprod g).comp N) = f

@[simp]
theorem monoid_hom.coprod_comp_inr {M : Type u_5} {N : Type u_6} {P : Type u_7} [monoid M] [monoid N] [comm_monoid P] (f : M →* P) (g : N →* P) :
(f.coprod g).comp N) = g

@[simp]
theorem add_monoid_hom.coprod_comp_inr {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_monoid M] [add_monoid N] (f : M →+ P) (g : N →+ P) :
(f.coprod g).comp N) = g

@[simp]
theorem monoid_hom.coprod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} [monoid M] [monoid N] [comm_monoid P] (f : M × N →* P) :
(f.comp N)).coprod (f.comp N)) = f

@[simp]
theorem add_monoid_hom.coprod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_monoid M] [add_monoid N] (f : M × N →+ P) :
(f.comp N)).coprod (f.comp N)) = f

@[simp]
theorem add_monoid_hom.coprod_inl_inr {M : Type u_1} {N : Type u_2}  :

@[simp]
theorem monoid_hom.coprod_inl_inr {M : Type u_1} {N : Type u_2} [comm_monoid M] [comm_monoid N] :
N).coprod N) = monoid_hom.id (M × N)

theorem monoid_hom.comp_coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [monoid M] [monoid N] [comm_monoid P] {Q : Type u_1} [comm_monoid Q] (h : P →* Q) (f : M →* P) (g : N →* P) :
h.comp (f.coprod g) = (h.comp f).coprod (h.comp g)

def mul_equiv.prod_comm {M : Type u_5} {N : Type u_6} [monoid M] [monoid N] :
M × N ≃* N × M

The equivalence between M × N and N × M given by swapping the components is multiplicative.

Equations
M × N ≃+ N × M

The equivalence between M × N and N × M` given by swapping the components is additive.

@[simp]

@[simp]
theorem mul_equiv.coe_prod_comm {M : Type u_5} {N : Type u_6} [monoid M] [monoid N] :

@[simp]

@[simp]
theorem mul_equiv.coe_prod_comm_symm {M : Type u_5} {N : Type u_6} [monoid M] [monoid N] :