noncommCoprod_inl_inr — Mathlib

English

There is a natural equivalence between the family of monoid homomorphisms with pairwise commuting images and the monoid homomorphisms out of the product, given by noncommPiCoprod.

Русский

Существует естественное эквивалентное соответствие между семейством гомоморфизмов с попарно несовместимыми образами и гомоморфизмами из произведения, заданное через noncommPiCoprod.

LaTeX

$$$\\text{MonoidHom}.noncommPiCoprodEquiv \\colon (\\{\\varphi_i: N_i \\to M\\}) \\simeq ((\\prod_i N_i) \\to M) $ с соответствующим отображением.$$

Lean4

@[to_additive (attr := simp)]
theorem noncommCoprod_inl_inr {M N : Type*} [Monoid M] [Monoid N] :
    (inl M N).noncommCoprod (inr M N) commute_inl_inr = id (M × N) :=
  noncommCoprod_unique <| .id (M × N)

Похожие утверждения