pentagon_inv_hom_hom_hom_hom — Mathlib

English

A pentagon-type identity involving multiple instances of associator inverses and whiskers of hom components.

Русский

Пентагональная когерентность с несколькими инверсами ассоциаторов и взвешиваниями гом-компонентов.

LaTeX

$$$ (\alpha \text{inv}) \; \text{ and } \ (\alpha \text{hom}) \text{ in a pentagon} $$$

Lean4

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

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