NYLL
Module

PuncturedHypersurfaceFaithful.lean

Nyll.EtaleFundamentalGroups.Purity.PuncturedHypersurfaceFaithful
2 declarations indexed from sourceView source ↗

Module documentation

Faithful restriction to a punctured hypersurface

If every minimal prime not containing the equation has quotient dimension at least two, every connected component of the punctured spectrum meets the hypersurface. Consequently finite étale restriction to its actual pullback is faithful. This proves the dimension case of Stacks 58.19.2 (0BLG); its component-intersection case is the general connected-component theorem.

Imports6
Imported by1

Declarations

theorem

exists_hypersurface_point_in_connectedComponent_of_minimalPrime_dimension

L34 ↗
AlgebraicGeometry.FiniteEtale.exists_hypersurface_point_in_connectedComponent_of_minimalPrime_dimension
Documentation

The dimension condition on minimal primes forces the hypersurface to meet each connected component of the puncture.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits IsLocalRing
namespace AlgebraicGeometry.FiniteEtale
Lean source · statement
theorem exists_hypersurface_point_in_connectedComponent_of_minimalPrime_dimension
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (f : R) (hf : f ∈ maximalIdeal R)
    (hdim : ∀ P ∈ minimalPrimes R, f ∉ P →
      (2 : WithBot ℕ∞) ≤ ringKrullDim (R ⧸ P))
    (x : Scheme.puncturedSpectrum R) :
    ∃ y : Scheme.puncturedSpectrum R,
      f ∈ y.1.asIdeal ∧ y ∈ connectedComponent x
theorem

pullback_faithful_punctured_hypersurface_of_minimalPrime_dimension

L49 ↗
AlgebraicGeometry.FiniteEtale.pullback_faithful_punctured_hypersurface_of_minimalPrime_dimension
Documentation

Finite étale restriction to the punctured hypersurface is faithful under the minimal-prime dimension condition of Stacks 58.19.2 (0BLG). The source of the restriction is the literal scheme pullback defining that hypersurface.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits IsLocalRing
namespace AlgebraicGeometry.FiniteEtale
Lean source · statement
theorem pullback_faithful_punctured_hypersurface_of_minimalPrime_dimension
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (f : R) (hf : f ∈ maximalIdeal R)
    (hdim : ∀ P ∈ minimalPrimes R, f ∉ P →
      (2 : WithBot ℕ∞) ≤ ringKrullDim (R ⧸ P)) :
    (FiniteEtale.pullback (pullback.fst (Scheme.puncturedSpectrumInclusion R)
      (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (Ideal.span {f})))))).Faithful

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