whisker_assoc_symm — Mathlib

English

A symmetry relation for whiskering on the left with respect to associator: whiskering left by f and the left and right associators yields equality with a composite involving η and associators.

Русский

Симметрия левого висения относительно ассоциатора: левое висение даст равенство через композиции η и ассоциаторами.

LaTeX

$$$ \\operatorname{whiskerLeft}(f, (η)) \\;=\\; (α_f g h)^{-1} \\circ (\\operatorname{whiskerRight}(η (g), h)) \\circ (α_{f', g, h})_{hom}^{-1}$$$

Lean4

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

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