associator_inv_naturality_middle — Mathlib

English

Dual middle naturality: f ◁ η ▷ h and the inverses of associators satisfy an exchange with the inverse associator and whiskering.

Русский

Двойной средний натурализм: взаимодействие между f ◁ η ▷ h и обратными ассоциаторами через висение.

LaTeX

$$$ f \\triangleleft η \\triangleright h \\; \\circ \\; (α_f g' h)^{-1} = (α_f g h)^{-1} \\circ (f ◁ η) ▷ h \\circ (α_f g h)^{-1}$$$

Lean4

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

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