preimage_id — Mathlib

English

For any ring R, the preimage of the identity morphism on Spec R under Spec.map is the identity on R: Spec.preimage(𝟙(Spec R)) = 𝟙 R.

Русский

Для кольца R предобраз тождественного морфизма на Spec R через Spec.map равен тождественному морфизму на R: Spec.preimage(𝟙(Spec R)) = 𝟙 R.

LaTeX

$$$\mathrm{Spec.preimage}(\mathrm{Id}_{\mathrm{Spec}R}) = \mathrm{Id}_R$$$

Lean4

@[simp]
theorem preimage_id {R : CommRingCat} : Spec.preimage (𝟙 (Spec R)) = 𝟙 R :=
  Spec.map_injective (by simp)

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