Documentation

Mathlib.GroupTheory.NoncommCoprod

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

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

Instances For

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

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

Instances For

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) ⋯

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) ⋯

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

AddMonoidHom.noncommCoprod f g comm = let __spread.0 := AddHom.noncommCoprod (↑f) (↑g) comm; { toZeroHom := { toFun := fun (mn : M × N) => f mn.1 + g mn.2, map_zero' := ⋯ }, map_add' := ⋯ }

Instances For

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

MonoidHom.noncommCoprod f g comm = let __spread.0 := MulHom.noncommCoprod (↑f) (↑g) comm; { toOneHom := { toFun := fun (mn : M × N) => f mn.1 * g mn.2, map_one' := ⋯ }, map_mul' := ⋯ }

Instances For

@[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)) ⋯ = 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)) ⋯ = 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) ⋯ = 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) ⋯ = 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) ⋯

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) ⋯