liftNatTrans_id — Mathlib

English

For any F: C ⥤ E and F': D ⥤ E with a lifting, liftNatTrans applied to the identity on F equals the identity on F'.

Русский

Для любых F: C ⥤ E и F': D ⥤ E с допускаемым поднятием, liftNatTrans от тождества на F даёт тождественный трансформацию на F'.

LaTeX

$$$\\text{liftNatTrans } L W F F F' F' (\\mathrm{Id}_F) = \\mathrm{Id}_{F'}$$$

Lean4

@[simp]
theorem liftNatTrans_id (F : C ⥤ E) (F' : D ⥤ E) [h : Lifting L W F F'] : liftNatTrans L W F F F' F' (𝟙 F) = 𝟙 F' :=
  natTrans_ext L W fun X =>
    by
    simp only [liftNatTrans_app, NatTrans.id_app, id_comp, Iso.hom_inv_id_app]
    rfl

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