Theorems · Theorem · group theory

MonoidHom.comp_noncommPiCoprod

∀ {M : Type u_1} [inst : Monoid M] {ι : Type u_2} [inst_1 : Fintype ι] {N : ι → Type u_3}
  [inst_2 : (i : ι) → Monoid (N i)] (ϕ : (i : ι) → N i →* M)
  {hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)} {P : Type u_4} [inst_3 : Monoid P]
  {f : M →* P}
  (hcomm' : optParam (Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((f.comp (ϕ i)) x) ((f.comp (ϕ j)) y)) ⋯),
  f.comp (MonoidHom.noncommPiCoprod ϕ hcomm) = MonoidHom.noncommPiCoprod (fun i => f.comp (ϕ i)) hcomm'

Given monoid morphisms φᵢ : Nᵢ → M and f : M → P, if we have sufficient commutativity, then f ∘ (∐ᵢ φᵢ) = ∐ᵢ (f ∘ φᵢ)

Defined in

Mathlib.GroupTheory.NoncommPiCoprod

Cited by

1 results in Mathlib

Foundations

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

Assumes

MonoidFintypeMonoidMonoid