instIsMonHomWhiskerRight — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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