leftUnitor_naturality — Mathlib

English

Natural transformation given by the left unitor is natural in morphisms in the localized monoidal category.

Русский

Натуральность естественного преобразования левой единицы в локализованной монойдальной категории.

LaTeX

$$$\text{leftUnitor naturality: } 𝟙_{\text{LocMon}} \triangleleft f \;\circ\; (\lambda_Y)^{\mathrm{hom}} = (\lambda_X)^{\mathrm{hom}} \circ f$$$

Lean4

theorem leftUnitor_naturality {X Y : LocalizedMonoidal L W ε} (f : X ⟶ Y) :
    𝟙_ (LocalizedMonoidal L W ε) ◁ f ≫ (λ_ Y).hom = (λ_ X).hom ≫ f := by simp [monoidalCategoryStruct]

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