pentagon_hom_inv_inv_inv_inv — Mathlib

English

A coherence condition in a bicategory relating two ways of composing associators and whiskers with inverse 2-cells; it expresses that two different parenthesizations of a five-fold composition are equal after taking inverses appropriately.

Русский

Соответствие коэренции в бикатегории между двумя способами композиции ассоциаторов и взвешиваний с обратными 2-ячейками; утверждает, что две разные расстановки скобок в пятиэлементной композиции равны после применения обратных.

LaTeX

$$$ (\mathrm{inv}(\alpha)) \; \triangleright \; \mathrm{...} = \dots $$$

Lean4

@[reassoc (attr := simp)]
theorem pentagon_hom_inv_inv_inv_inv (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
    f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv = (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i := by
  simp [← cancel_epi (f ◁ (α_ g h i).inv)]

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