id_app — Mathlib

English

The app of the identity morphism equals the identity on sections: (id_X).app U = id_{X.presheaf.obj U}.

Русский

При применении к единичному морфизму получаем тождественную стрелку на секциях: (id_X).app U = id_{X.presheaf.obj U}.

LaTeX

$$$(\\mathrm{id}_X).app U = \\mathrm{id}_{X.presheaf.obj{\\; unop\\; U}}$$$

Lean4

@[simp]
theorem id_app {X : Scheme} (U : X.Opens) : (𝟙 X :).app U = 𝟙 _ :=
  rfl

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