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 AddHom.noncommCoprod {M : Type u_1} {N : Type u_2} {P : Type u_3} [Add M] [Add N] [AddSemigroup P] (f : AddHom M P) (g : AddHom N P) (comm : ∀ (m : M) (n : N), AddCommute (f m) (g n)) : AddHom (M × N) P

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

Equations

• One or more equations did not get rendered due to their size.

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

@[simp]

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

@[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) : (MulHom.noncommCoprod f g comm) mn = f mn.1 * g mn.2

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 commutation assumption : f.noncommCoprod g _ (p : M × N) = f p.1 * g p.2. (For the commutative case, use MulHom.coprod)

Equations

• One or more equations did not get rendered due to their size.

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

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) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)) {Q : Type u_4} [Semigroup Q] (h : P →ₙ* Q) : MulHom.comp h (MulHom.noncommCoprod f g comm) = MulHom.noncommCoprod (MulHom.comp h f) (MulHom.comp h g) (_ : ∀ (m : M) (n : N), Commute (h (f m)) (h (g n)))

theorem AddMonoidHom.noncommCoprod.proof_2 {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)) (x : M × N) (y : M × N) : (AddHom.noncommCoprod (↑f) (↑g) comm).toFun (x + y) = (AddHom.noncommCoprod (↑f) (↑g) comm).toFun x + (AddHom.noncommCoprod (↑f) (↑g) comm).toFun y

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

• One or more equations did not get rendered due to their size.

theorem AddMonoidHom.noncommCoprod.proof_1 {M : Type u_2} {N : Type u_3} {P : Type u_1} [AddZeroClass M] [AddZeroClass N] [AddMonoid P] (f : M →+ P) (g : N →+ P) : f 0 + g 0 = 0

@[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) : (AddMonoidHom.noncommCoprod f 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) : (MonoidHom.noncommCoprod f g comm) mn = f mn.1 * g mn.2

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

• One or more equations did not get rendered due to their size.

@[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)) : AddMonoidHom.comp (AddMonoidHom.noncommCoprod f g comm) (AddMonoidHom.inl M N) = f

@[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)) : MonoidHom.comp (MonoidHom.noncommCoprod f g comm) (MonoidHom.inl M N) = f

@[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)) : AddMonoidHom.comp (AddMonoidHom.noncommCoprod f g comm) (AddMonoidHom.inr M N) = g

@[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)) : MonoidHom.comp (MonoidHom.noncommCoprod f g comm) (MonoidHom.inr M N) = g

@[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) : AddMonoidHom.noncommCoprod (AddMonoidHom.comp f (AddMonoidHom.inl M N)) (AddMonoidHom.comp f (AddMonoidHom.inr M N)) (_ : ∀ (x : M) (x_1 : N), AddCommute (f ((AddMonoidHom.inl M N) x)) (f ((AddMonoidHom.inr M N) x_1))) = f

@[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) : MonoidHom.noncommCoprod (MonoidHom.comp f (MonoidHom.inl M N)) (MonoidHom.comp f (MonoidHom.inr M N)) (_ : ∀ (x : M) (x_1 : N), Commute (f ((MonoidHom.inl M N) x)) (f ((MonoidHom.inr M N) x_1))) = f

@[simp]

theorem AddMonoidHom.noncommCoprod_inl_inr {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddMonoid N] : AddMonoidHom.noncommCoprod (AddMonoidHom.inl M N) (AddMonoidHom.inr M N) (_ : ∀ (m : M) (n : N), AddCommute ((AddMonoidHom.inl M N) m) ((AddMonoidHom.inr M N) n)) = AddMonoidHom.id (M × N)

@[simp]

theorem MonoidHom.noncommCoprod_inl_inr {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] : MonoidHom.noncommCoprod (MonoidHom.inl M N) (MonoidHom.inr M N) (_ : ∀ (m : M) (n : N), Commute ((MonoidHom.inl M N) m) ((MonoidHom.inr M N) n)) = MonoidHom.id (M × N)

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) : AddMonoidHom.comp h (AddMonoidHom.noncommCoprod f g comm) = AddMonoidHom.noncommCoprod (AddMonoidHom.comp h f) (AddMonoidHom.comp h g) (_ : ∀ (m : M) (n : N), AddCommute (h (f m)) (h (g 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) : MonoidHom.comp h (MonoidHom.noncommCoprod f g comm) = MonoidHom.noncommCoprod (MonoidHom.comp h f) (MonoidHom.comp h g) (_ : ∀ (m : M) (n : N), Commute (h (f m)) (h (g n)))