naturality_comp_inv — Mathlib

English

Inverse naturaliy for composition expresses the inverse of naturaliy as a composite of whiskers and associators.

Русский

Обратная натуральность композиции выражается как композиция взвешиваний и ассоциаторов.

LaTeX

$$$(\alpha.naturality (inst.comp f g)).inv = \dots$$$

Lean4

@[reassoc, to_app]
theorem naturality_comp_inv (α : F ⟶ G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c) :
    (α.naturality (f ≫ g)).inv =
      α.app a ◁ (G.mapComp f g).hom ≫
        (α_ _ _ _).inv ≫
          (α.naturality f).inv ▷ G.map g ≫
            (α_ _ _ _).hom ≫ F.map f ◁ (α.naturality g).inv ≫ (α_ _ _ _).inv ≫ (F.mapComp f g).inv ▷ α.app c :=
  by simp [naturality_comp_iso α f g]

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