instIsMonHomWhiskerLeft — Mathlib

English

Left whiskering by a fixed object preserves the monoid-hom condition: if f is a monoid morphism, then X ⊗ f is also a monoid morphism.

Русский

Левый вайскеринг фиксированного объекта сохраняет условие моноидного гомома: если f — моноидный морфизм, то X ⊗ f тоже моноидный морфизм.

LaTeX

$$$\\text{If } f:\\,Y\\to Z\\text{ isMonHom, then } X\\otimes f:\\, X\\otimes Y\\to X\\otimes Z\\text{ isMonHom}$$$

Lean4

instance {f : Y ⟶ Z} [IsMonHom f] : IsMonHom (X ◁ f)
    where
  one_hom := by simpa using (inferInstanceAs <| IsMonHom (𝟙 X ⊗ₘ f)).one_hom
  mul_hom := by simpa using (inferInstanceAs <| IsMonHom (𝟙 X ⊗ₘ f)).mul_hom

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