pentagon_hom_inv_inv_inv_hom — Mathlib

English

Another instance of a pentagon-type coherence relation, relating inverses and whiskers in a five-term composition.

Русский

Еще одно когерентное условие типа пентагона, связывающее инверсы и взвешивания в пятичленной композиции.

LaTeX

$$$ (\alpha \text{ inv/whisker combos }) = (\alpha \text{ inv/whisker combos }) $$$

Lean4

@[reassoc (attr := simp)]
theorem pentagon_hom_inv_inv_inv_hom (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).hom ▷ i :=
  by
  rw [← cancel_epi (α_ f g (h ≫ i)).inv, ← cancel_mono ((α_ f g h).inv ▷ i)]
  simp

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