pentagon_inv_inv_hom_inv_inv — Mathlib

English

A higher coherence relation expressing equality of two composites involving inverses and hom components in a pentagonal configuration.

Русский

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

LaTeX

$$$ (\alpha \text{inv}, \mathrm{hom}) \; = \; (\mathrm{hom}, \alpha \text{inv}) $$$

Lean4

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

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