naturality_id_hom — Mathlib

English

A canonical expression of naturaliy at identity as a composite of whiskers and associators, yielding an isomorphism.

Русский

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

LaTeX

$$$\alpha.naturality (\mathrm{Id} a)$$$

Lean4

@[reassoc, to_app]
theorem naturality_id_hom (α : F ⟶ G) (a : B) :
    (α.naturality (𝟙 a)).hom =
      (F.mapId a).hom ▷ α.app a ≫ (λ_ (α.app a)).hom ≫ (ρ_ (α.app a)).inv ≫ α.app a ◁ (G.mapId a).inv :=
  by simp [← assoc, ← IsIso.comp_inv_eq]

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