isLocalHom_iff_comap_closedPoint — Mathlib

English

A ring hom f : R → S between commutative rings with IsLocalRing structure is local iff the induced map on prime spectra contracts the closed point of S to the closed point of R.

Русский

Гомоморфизм колец локален тогда и только тогда, когда соответствующее отображение спектров сохраняет замкнутые точки: лемма эквивалентности контрактов.

LaTeX

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

Lean4

theorem isLocalHom_iff_comap_closedPoint {S : Type v} [CommSemiring S] [IsLocalRing S] (f : R →+* S) :
    IsLocalHom f ↔ PrimeSpectrum.comap f (closedPoint S) = closedPoint R := by
  -- Porting note: inline `this` does **not** work

  have := (local_hom_TFAE f).out 0 4
  rw [this, PrimeSpectrum.ext_iff]
  rfl

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