Theorems · Definition · group theory

AddMonoidHom.noncommPiCoprodEquiv

{M : Type u_1} →
  [inst : AddMonoid M] →
    {ι : Type u_2} →
      [Fintype ι] →
        {N : ι → Type u_3} →
          [inst_2 : (i : ι) → AddMonoid (N i)] →
            [DecidableEq ι] →
              { ϕ // Pairwise fun i j => ∀ (x : N i) (y : N j), AddCommute ((ϕ i) x) ((ϕ j) y) } ≃
                (((i : ι) → N i) →+ M)

The universal property of MonoidHom.noncommPiCoprod Given monoid morphisms φᵢ : Nᵢ → M whose images pairwise commute, there exists a unique monoid morphism φ : Πᵢ Nᵢ → M that induces the φᵢ, and it is given by AddMonoidHom.noncommPiCoprod.

Defined in

Mathlib.GroupTheory.NoncommPiCoprod

Cited by

0 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddMonoidFintypeAddMonoidDecidableEq