NYLL
Module

PuncturedSpectrumHartshorneLichtenbaumGeometry.lean

Nyll.EtaleFundamentalGroups.Purity.PuncturedSpectrumHartshorneLichtenbaumGeometry
3 declarations indexed from sourceView source ↗

Module documentation

Finite dimension and the geometric Hartshorne--Lichtenbaum frontier

Finite Krull dimension gives an actual natural-number dimension, rather than only a WithBot ENat value. We also record the geometric content of a proper radical support being different from the maximal ideal: its closed set contains a point of the punctured spectrum.

Imports3
Imported by2

Declarations

theorem

exists_nat_ringKrullDim_eq_of_finiteRingKrullDim

L31 ↗
AlgebraicGeometry.FiniteEtale.exists_nat_ringKrullDim_eq_of_finiteRingKrullDim
Documentation

The Krull dimension of a ring with finite Krull dimension is represented by a natural number. In particular this applies to every Noetherian local ring via Mathlib's FiniteRingKrullDim instance.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem exists_nat_ringKrullDim_eq_of_finiteRingKrullDim
    {R : Type u} [CommRing R] [FiniteRingKrullDim R] :
    ∃ d : ℕ, ringKrullDim R = (d : WithBot ℕ∞)
theorem

exists_nonmaximal_prime_over_of_isRadical

L50 ↗
AlgebraicGeometry.FiniteEtale.exists_nonmaximal_prime_over_of_isRadical
Documentation

A proper radical ideal different from the maximal ideal is contained in a nonmaximal prime. The explicit properness hypothesis is necessary: the unit ideal is radical and differs from the maximal ideal.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem exists_nonmaximal_prime_over_of_isRadical
    {R : Type u} [CommRing R] [IsLocalRing R]
    (J : Ideal R) (hJradical : J.IsRadical)
    (hJproper : J ≠ ⊤) (hJnonmax : J ≠ maximalIdeal R) :
    ∃ P : Ideal R,
      J ≤ P ∧ P.IsPrime ∧ P ≠ maximalIdeal R
theorem

zeroLocus_inter_puncture_nonempty_of_isRadical

L65 ↗
AlgebraicGeometry.FiniteEtale.zeroLocus_inter_puncture_nonempty_of_isRadical
Documentation

The zero locus of a proper radical nonmaximal ideal meets the punctured spectrum.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem zeroLocus_inter_puncture_nonempty_of_isRadical
    {R : Type u} [CommRing R] [IsLocalRing R]
    (J : Ideal R) (hJradical : J.IsRadical)
    (hJproper : J ≠ ⊤) (hJnonmax : J ≠ maximalIdeal R) :
    (PrimeSpectrum.zeroLocus J ∩
      ({closedPoint R}ᶜ : Set (PrimeSpectrum R))).Nonempty

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.