English
The identity morphism on a ring induces the identity morphism on the corresponding locally ringed space; i.e., Spec.locallyRingedSpaceMap(1_R) is the identity.
Русский
Идентичный морфизм на кольцах порождает идентичный морфизм на соответствующем локально кольцевом пространстве; т.е. Spec.locallyRingedSpaceMap(1_R) — тождественный.
LaTeX
$$$\mathrm{Spec.locallyRingedSpaceMap}(\mathbf{1}_R) = \mathbf{1}_{\mathrm{Spec.locallyRingedSpaceObj R}}$$$
Lean4
@[simp]
theorem locallyRingedSpaceMap_id (R : CommRingCat.{u}) :
Spec.locallyRingedSpaceMap (𝟙 R) = 𝟙 (Spec.locallyRingedSpaceObj R) :=
LocallyRingedSpace.Hom.ext' <| by rw [Spec.locallyRingedSpaceMap_toShHom, Spec.sheafedSpaceMap_id]; rfl