naturality_comp_iso — Mathlib

English

Naturality of composition yields a chain of isomorphisms connecting different whiskerings.

Русский

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

LaTeX

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

Lean4

theorem naturality_comp_iso (α : F ⟶ G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c) :
    α.naturality (f ≫ g) =
      whiskerRightIso (F.mapComp f g) (α.app c) ≪≫
        (α_ _ _ _) ≪≫
          whiskerLeftIso (F.map f) (α.naturality g) ≪≫
            (α_ _ _ _).symm ≪≫
              whiskerRightIso (α.naturality f) (G.map g) ≪≫ α_ _ _ _ ≪≫ whiskerLeftIso (α.app a) (G.mapComp f g).symm :=
  by
  ext
  simp [naturality_comp_hom α f g]

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