locallyRingedSpaceMap_id — Mathlib

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

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