English
The coproduct composed with the left inclusion equals f.
Русский
Копродукт после вставки слева равен f.
LaTeX
$$$ (f.noncommCoprod g comm).\\mathrm{comp}(\\mathrm{inl} M N) = f.$$$
Lean4
/-- 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 `MonoidHom.noncommPiCoprod`. -/
@[to_additive /-- 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`. -/
]
def noncommPiCoprodEquiv [DecidableEq ι] :
{ ϕ : ∀ i, N i →* M // Pairwise fun i j => ∀ x y, Commute (ϕ i x) (ϕ j y) } ≃ ((∀ i, N i) →* M)
where
toFun ϕ := noncommPiCoprod ϕ.1 ϕ.2
invFun
f := ⟨fun i => f.comp (MonoidHom.mulSingle N i), fun _ _ hij x y => Commute.map (Pi.mulSingle_commute hij x y) f⟩
left_inv
ϕ := by
ext
simp only [coe_comp, Function.comp_apply, mulSingle_apply, noncommPiCoprod_mulSingle]
right_inv
f := pi_ext fun i x => by simp only [noncommPiCoprod_mulSingle, coe_comp, Function.comp_apply, mulSingle_apply]
