associator_naturality_left — Mathlib

English

Naturalness of the associator with respect to left whiskering: whiskering an arrow η: f → f' on the left by g and h commutes with the associator. Precisely, (η ▷ g) ▷ h followed by (α_f' g h)^{hom} equals (α_f g h)^{hom} followed by η whiskered with (g ≫ h).

Русский

Натурализация ассоциатора по отношению к левому висению: уравнения для η: f → f' демонстрируют совместимость с ассоциатором при композициях.

LaTeX

$$$ (η \\triangleright g) \\triangleright h \\; \\circ \\; (\\alpha_f' g h)_{\\mathrm{hom}} = (\\alpha_f g h)_{\\mathrm{hom}} \\circ (η \\triangleright (g \\gg h)) $$$

Lean4

@[reassoc]
theorem associator_naturality_left {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d) :
    η ▷ g ▷ h ≫ (α_ f' g h).hom = (α_ f g h).hom ≫ η ▷ (g ≫ h) := by simp

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