map_id_c_app — Mathlib

English

The identity map on j passes through the pushforward id and pushforward equality maps in the component c-app; a standard identity diagram in colimits.

Русский

Тождественный отображение на j проходит через pushforward-id и pushforward-eq в компоненте c-app.

LaTeX

$$$(F.map (\\mathrm{id}_j)).c.app U = (Pushforward.id (F.obj j).presheaf).inv.app U ≫ (pushforwardEq (by simp) (F.obj j).presheaf).hom.app U$$$

Lean4

@[simp]
theorem map_id_c_app (F : J ⥤ PresheafedSpace.{_, _, v} C) (j) (U) :
    (F.map (𝟙 j)).c.app U =
      (Pushforward.id (F.obj j).presheaf).inv.app U ≫ (pushforwardEq (by simp) (F.obj j).presheaf).hom.app U :=
  by simp [PresheafedSpace.congr_app (F.map_id j)]

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