pentagon_hom_hom_inv_hom_hom — Mathlib

English

A higher coherence relation expressing equality of two specific compositions of associators and whiskers with inverses and hom components in a pentagon-like diagram.

Русский

Высшее отношение когерентности, равенство двух конкретных композиционных последовательностей ассоциаторов и взвешиваний с обратными и гом-компонентами в диаграмме типа пентагон.

LaTeX

$$$ (\alpha \text{ terms }) = (\alpha \text{ terms }) $$$

Lean4

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

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