naturality_comp_hom — Mathlib

English

Inverse naturality for a StrongTrans between F and G expresses the relation of the inverse of naturaility with whiskering actions.

Русский

Обратная натуральность для StrongTrans между F и G связывает обратную натуральность с взвешиванием.

LaTeX

$$$(\alpha.naturality g).inv = ...$$$

Lean4

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

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