residueFieldMap_id — Mathlib

English

The residue field map of the identity morphism is the identity on the residue field.

Русский

Карта резидуума для тождественного отображения равна тождественному отображению на поле остатка.

LaTeX

$$$$ \operatorname{Hom.residueFieldMap}(\mathrm{Id}_X, x) = \operatorname{id}_{X.\mathrm{residueField}(x)}. $$$$

Lean4

@[simp]
theorem residueFieldMap_id (x : X) : Hom.residueFieldMap (𝟙 X) x = 𝟙 (X.residueField x) :=
  LocallyRingedSpace.residueFieldMap_id _

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