id_commMonCat_comp — Mathlib

English

For commutative monoids, composing with the identity morphism yields the same morphism: f ∘ id = f.

Русский

Для коммутативных моноидов композиция с единицей даёт тот же морфизм: f ∘ id = f.

LaTeX

$$$\mathrm{Hom}_{CommMonCat}(G, H)$, $f$ — монодоморфизм; $\mathrm{id}_G$ — идентичность; $\mathrm{MonCat}$ формирует $f \circ \mathrm{id} = f$.$$

Lean4

@[to_additive (attr := deprecated "Proven by `simp only [CommMonCat.hom_id, id_comp]`" (since := "2025-01-28"))]
theorem id_commMonCat_comp {G : Type u} [CommMonoid G] {H : CommMonCat.{u}} (f : G →* H) :
    MonoidHom.comp (CommMonCat.Hom.hom (𝟙 H)) f = f := by simp

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