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: #

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

source
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 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' := ⋯ }
Instances For
    source
    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'
    source
    @[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) :
    (f.noncommCoprod g comm) mn = f mn.1 + g mn.2
    source
    @[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
    source
    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' := ⋯ }
    Instances For
      source
      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) {Q : Type u_4} [AddSemigroup Q] (h : AddHom 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) ⋯
      source
      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) ⋯
      source
      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) :
      ((↑f).noncommCoprod (↑g) comm).toFun (x + y) = ((↑f).noncommCoprod (↑g) comm).toFun x + ((↑f).noncommCoprod (↑g) comm).toFun y
      source
      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 = let __spread.0 := (↑f).noncommCoprod (↑g) comm; { toFun := fun (mn : M × N) => f mn.1 + g mn.2, map_zero' := ⋯, map_add' := ⋯ }
      Instances For
        source
        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
        source
        @[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
        source
        @[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
        source
        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 = let __spread.0 := (↑f).noncommCoprod (↑g) comm; { toFun := fun (mn : M × N) => f mn.1 * g mn.2, map_one' := ⋯, map_mul' := ⋯ }
        Instances For
          source
          @[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 (AddMonoidHom.inl M N) = f
          source
          @[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 (MonoidHom.inl M N) = f
          source
          @[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 (AddMonoidHom.inr M N) = g
          source
          @[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 (MonoidHom.inr M N) = g
          source
          @[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 (AddMonoidHom.inl M N)).noncommCoprod (f.comp (AddMonoidHom.inr M N)) ⋯ = f
          source
          @[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 (MonoidHom.inl M N)).noncommCoprod (f.comp (MonoidHom.inr M N)) ⋯ = f
          source
          @[simp]
          theorem AddMonoidHom.noncommCoprod_inl_inr {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddMonoid N] :
          (AddMonoidHom.inl M N).noncommCoprod (AddMonoidHom.inr M N) ⋯ = AddMonoidHom.id (M × N)
          source
          @[simp]
          theorem MonoidHom.noncommCoprod_inl_inr {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] :
          (MonoidHom.inl M N).noncommCoprod (MonoidHom.inr M N) ⋯ = MonoidHom.id (M × N)
          source
          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) ⋯
          source
          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) ⋯