morphismRestrict_id — Mathlib

English

Restricting the identity morphism to any open U gives the identity on the restricted open: 𝟙 X|_U = 𝟙.

Русский

Ограничение тождества к любому открытому U даёт тождественный морфизм на ограниченном открытом: 𝟙 X|_U = 𝟙.

LaTeX

$$$\mathrm{morphismRestrict}(\mathrm{id}_X, U) = \mathrm{id}_{X|_U}$$$

Lean4

@[simp]
theorem morphismRestrict_id {X : Scheme.{u}} (U : X.Opens) : 𝟙 X ∣_ U = 𝟙 _ :=
  by
  rw [← cancel_mono U.ι, morphismRestrict_ι, Category.comp_id, Category.id_comp]
  rfl

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