Canonical homomorphism from a pair of monoids

This file defines the construction of the canonical homomorphism from a pair of monoids.

Given two morphisms of monoids f : M →* P and g : N →* P where elements in the images of the two morphisms commute, we obtain a canonical morphism MonoidHom.noncommCoprod : M × N →* P whose composition with inl M N coincides with f and whose composition with inr M N coincides with g.

There is an analogue MulHom.noncommCoprod when f and g are only MulHoms.

Main theorems:

• noncommCoprod_comp_inr and noncommCoprod_comp_inl prove that the compositions of MonoidHom.noncommCoprod f g _ with inl M N and inr M N coincide with f and g.
• comp_noncommCoprod proves that the composition of a morphism of monoids h with noncommCoprod f g _ coincides with noncommCoprod (h.comp f) (h.comp g).

For a product of a family of morphisms of monoids, see MonoidHom.noncommPiCoprod.

def MulHom.noncommCoprod {M : Type u_1} {N : Type u_2} {P : Type u_3} [Mul M] [Mul N] [Semigroup P] (f : M →ₙ* P) (g : N →ₙ* P) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)) : M × N →ₙ* P

Coproduct of two MulHoms with the same codomain with Commute assumption: f.noncommCoprod g _ (p : M × N) = f p.1 * g p.2. (For the commutative case, use MulHom.coprod)

Equations

• f.noncommCoprod g comm = { toFun := fun (mn : M × N) => f mn.1 * g mn.2, map_mul' := ⋯ }

def AddHom.noncommCoprod {M : Type u_1} {N : Type u_2} {P : Type u_3} [Add M] [Add N] [AddSemigroup P] (f : M →ₙ+ P) (g : N →ₙ+ P) (comm : ∀ (m : M) (n : N), AddCommute (f m) (g n)) : M × N →ₙ+ P

Coproduct of two AddHoms with the same codomain with AddCommute assumption: f.noncommCoprod g _ (p : M × N) = f p.1 + g p.2. (For the commutative case, use AddHom.coprod)

Equations

• f.noncommCoprod g comm = { toFun := fun (mn : M × N) => f mn.1 + g mn.2, map_add' := ⋯ }

@[simp]

theorem MulHom.noncommCoprod_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [Mul M] [Mul N] [Semigroup P] (f : M →ₙ* P) (g : N →ₙ* P) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)) (mn : M × N) : (f.noncommCoprod g comm) mn = f mn.1 * g mn.2

@[simp]

theorem AddHom.noncommCoprod_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [Add M] [Add N] [AddSemigroup P] (f : M →ₙ+ P) (g : N →ₙ+ P) (comm : ∀ (m : M) (n : N), AddCommute (f m) (g n)) (mn : M × N) : (f.noncommCoprod g comm) mn = f mn.1 + g mn.2

theorem MulHom.noncommCoprod_apply' {M : Type u_1} {N : Type u_2} {P : Type u_3} [Mul M] [Mul N] [Semigroup P] (f : M →ₙ* P) (g : N →ₙ* P) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)) (mn : M × N) : (f.noncommCoprod g comm) mn = g mn.2 * f mn.1

Variant of MulHom.noncommCoprod_apply with the product written in the other direction`

theorem AddHom.noncommCoprod_apply' {M : Type u_1} {N : Type u_2} {P : Type u_3} [Add M] [Add N] [AddSemigroup P] (f : M →ₙ+ P) (g : N →ₙ+ P) (comm : ∀ (m : M) (n : N), AddCommute (f m) (g n)) (mn : M × N) : (f.noncommCoprod g comm) mn = g mn.2 + f mn.1

Variant of AddHom.noncommCoprod_apply, with the sum written in the other direction

theorem MulHom.comp_noncommCoprod {M : Type u_1} {N : Type u_2} {P : Type u_3} [Mul M] [Mul N] [Semigroup P] (f : M →ₙ* P) (g : N →ₙ* P) {Q : Type u_4} [Semigroup Q] (h : P →ₙ* Q) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)) : h.comp (f.noncommCoprod g comm) = (h.comp f).noncommCoprod (h.comp g) ⋯

theorem AddHom.comp_noncommCoprod {M : Type u_1} {N : Type u_2} {P : Type u_3} [Add M] [Add N] [AddSemigroup P] (f : M →ₙ+ P) (g : N →ₙ+ P) {Q : Type u_4} [AddSemigroup Q] (h : P →ₙ+ Q) (comm : ∀ (m : M) (n : N), AddCommute (f m) (g n)) : h.comp (f.noncommCoprod g comm) = (h.comp f).noncommCoprod (h.comp g) ⋯

def MonoidHom.noncommCoprod {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [Monoid P] (f : M →* P) (g : N →* P) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)) : M × N →* P

Coproduct of two MonoidHoms with the same codomain, with a commutation assumption: f.noncommCoprod g _ (p : M × N) = f p.1 * g p.2. (Noncommutative case; in the commutative case, use MonoidHom.coprod.)

Equations

• f.noncommCoprod g comm = { toFun := fun (mn : M × N) => f mn.1 * g mn.2, map_one' := ⋯, map_mul' := ⋯ }

def AddMonoidHom.noncommCoprod {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddMonoid P] (f : M →+ P) (g : N →+ P) (comm : ∀ (m : M) (n : N), AddCommute (f m) (g n)) : M × N →+ P

Coproduct of two AddMonoidHoms with the same codomain, with a commutation assumption: f.noncommCoprod g (p : M × N) = f p.1 + g p.2. (Noncommutative case; in the commutative case, use AddHom.coprod.)

Equations

• f.noncommCoprod g comm = { toFun := fun (mn : M × N) => f mn.1 + g mn.2, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem AddMonoidHom.noncommCoprod_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddMonoid P] (f : M →+ P) (g : N →+ P) (comm : ∀ (m : M) (n : N), AddCommute (f m) (g n)) (mn : M × N) : (f.noncommCoprod g comm) mn = f mn.1 + g mn.2

@[simp]

theorem MonoidHom.noncommCoprod_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [Monoid P] (f : M →* P) (g : N →* P) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)) (mn : M × N) : (f.noncommCoprod g comm) mn = f mn.1 * g mn.2

theorem MonoidHom.noncommCoprod_apply' {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [Monoid P] (f : M →* P) (g : N →* P) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)) (mn : M × N) : (f.noncommCoprod g comm) mn = g mn.2 * f mn.1

Variant of MonoidHom.noncomCoprod_apply with the product written in the other direction`

theorem AddMonoidHom.noncommCoprod_apply' {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddMonoid P] (f : M →+ P) (g : N →+ P) (comm : ∀ (m : M) (n : N), AddCommute (f m) (g n)) (mn : M × N) : (f.noncommCoprod g comm) mn = g mn.2 + f mn.1

Variant of AddMonoidHom.noncomCoprod_apply with the sum written in the other direction

@[simp]

theorem MonoidHom.noncommCoprod_comp_inl {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [Monoid P] (f : M →* P) (g : N →* P) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)) : (f.noncommCoprod g comm).comp (inl M N) = f

@[simp]

theorem AddMonoidHom.noncommCoprod_comp_inl {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddMonoid P] (f : M →+ P) (g : N →+ P) (comm : ∀ (m : M) (n : N), AddCommute (f m) (g n)) : (f.noncommCoprod g comm).comp (inl M N) = f

@[simp]

theorem MonoidHom.noncommCoprod_comp_inr {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [Monoid P] (f : M →* P) (g : N →* P) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)) : (f.noncommCoprod g comm).comp (inr M N) = g

@[simp]

theorem AddMonoidHom.noncommCoprod_comp_inr {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddMonoid P] (f : M →+ P) (g : N →+ P) (comm : ∀ (m : M) (n : N), AddCommute (f m) (g n)) : (f.noncommCoprod g comm).comp (inr M N) = g

@[simp]

theorem MonoidHom.noncommCoprod_unique {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [Monoid P] (f : M × N →* P) : (f.comp (inl M N)).noncommCoprod (f.comp (inr M N)) ⋯ = f

@[simp]

theorem AddMonoidHom.noncommCoprod_unique {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddMonoid P] (f : M × N →+ P) : (f.comp (inl M N)).noncommCoprod (f.comp (inr M N)) ⋯ = f

@[simp]

theorem MonoidHom.noncommCoprod_inl_inr {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] : (inl M N).noncommCoprod (inr M N) ⋯ = id (M × N)

@[simp]

theorem AddMonoidHom.noncommCoprod_inl_inr {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddMonoid N] : (inl M N).noncommCoprod (inr M N) ⋯ = id (M × N)

theorem MonoidHom.comp_noncommCoprod {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [Monoid P] (f : M →* P) (g : N →* P) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)) {Q : Type u_4} [Monoid Q] (h : P →* Q) : h.comp (f.noncommCoprod g comm) = (h.comp f).noncommCoprod (h.comp g) ⋯

theorem AddMonoidHom.comp_noncommCoprod {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddMonoid P] (f : M →+ P) (g : N →+ P) (comm : ∀ (m : M) (n : N), AddCommute (f m) (g n)) {Q : Type u_4} [AddMonoid Q] (h : P →+ Q) : h.comp (f.noncommCoprod g comm) = (h.comp f).noncommCoprod (h.comp g) ⋯

theorem MonoidHom.noncommCoprod_injective {M : Type u_4} {N : Type u_5} {P : Type u_6} [Group M] [Group N] [Group P] (f : M →* P) (g : N →* P) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)) : Function.Injective ⇑(f.noncommCoprod g comm) ↔ Function.Injective ⇑f ∧ Function.Injective ⇑g ∧ Disjoint f.range g.range

theorem MonoidHom.noncommCoprod_range {M : Type u_4} {N : Type u_5} {P : Type u_6} [Group M] [Group N] [Group P] (f : M →* P) (g : N →* P) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)) : (f.noncommCoprod g comm).range = f.range ⊔ g.range