comap_residue — Mathlib

English

The topological Krull dimension of Spec(R) equals the ring Krull dimension of R.

Русский

Топологическая размерность Крюля спектра Spec(R) равна размерности кольца R.

LaTeX

$$$\\mathrm{topologicalKrullDim}(\\mathrm{Spec}(R)) = \\mathrm{ringKrullDim}(R)$$$

Lean4

@[simp]
theorem comap_residue (T : Type u) [CommRing T] [IsLocalRing T] (x : PrimeSpectrum (ResidueField T)) :
    PrimeSpectrum.comap (residue T) x = closedPoint T :=
  by
  rw [Subsingleton.elim x ⊥]
  ext1
  exact Ideal.mk_ker

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