naturality_id_iso — Mathlib

English

Relates naturality to whisker and associator isomorphisms for StrongTrans between pseudofunctors.

Русский

Связь натуральности с изоморфизмами whisker и associator для StrongTrans между псевдофункторными функторными структурами.

LaTeX

$$$\alpha.naturality g = \mathrm{whiskerRightIso} (F.map₂Iso η.symm) (\alpha.app b) \circ \dots$$$

Lean4

theorem naturality_id_iso (α : F ⟶ G) (a : B) :
    α.naturality (𝟙 a) =
      whiskerRightIso (F.mapId a) (α.app a) ≪≫
        (λ_ (α.app a)) ≪≫ (ρ_ (α.app a)).symm ≪≫ whiskerLeftIso (α.app a) (G.mapId a).symm :=
  by
  ext
  simp [naturality_id_hom]

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