comap_closedPoint — Mathlib

English

For a local ring hom f, the contraction of the closed point of S equals the closed point of R: f^*(closedPoint(S)) = closedPoint(R).

Русский

Для локального гомоморфизма f сокращение максимальной идеала в S даёт максимальный идеал в R.

LaTeX

$$$\\mathrm{Spec}(f)^{*}(\\mathrm{closedPoint}(S)) = \\mathrm{closedPoint}(R)$$$

Lean4

@[simp]
theorem comap_closedPoint {S : Type v} [CommSemiring S] [IsLocalRing S] (f : R →+* S) [IsLocalHom f] :
    PrimeSpectrum.comap f (closedPoint S) = closedPoint R :=
  (isLocalHom_iff_comap_closedPoint f).mp inferInstance

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