NYLL
Module

PuncturedHypersurfaceNeighborhoodExistence.lean

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

Module documentation

Neighbourhoods with faithful restriction to the punctured hypersurface

Delete the closed sets of the minimal primes outside V(f) whose quotient dimension is less than two. There are finitely many such primes. None of those closed sets meets the punctured hypersurface: such an intersection would provide a strict chain of two primes in the corresponding quotient.

The remaining open inside the puncture contains the punctured hypersurface and satisfies the minimal-prime dimension condition. Every smaller open containing the same hypersurface also satisfies that condition, so finite étale restriction is faithful for all of them.

This proves the neighbourhood-existence assertion in Stacks Project, Tag 0BLN. The categorical-colimit assertion is a separate statement.

Imports7
Imported by3

Declarations

theorem

exists_punctured_hypersurface_neighborhood_minimalPrime_dimension

L45 ↗
AlgebraicGeometry.FiniteEtale.exists_punctured_hypersurface_neighborhood_minimalPrime_dimension
Documentation

There is an open neighbourhood of the punctured hypersurface, contained in the puncture, for which all minimal primes outside the hypersurface have quotient dimension at least two. It is obtained by deleting finitely many closed subsets belonging to the other minimal primes.

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_punctured_hypersurface_neighborhood_minimalPrime_dimension
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (f : R) :
    ∃ U : (Spec (.of R)).Opens,
      U ≤ Scheme.puncturedSpectrumOpen R ∧
      (∀ p : PrimeSpectrum R,
        p ∈ Scheme.puncturedSpectrumOpen R → f ∈ p.asIdeal → p ∈ U) ∧
      (∀ (P : Ideal R) (hP : P ∈ minimalPrimes R),
        (⟨P, hP.isPrime⟩ : PrimeSpectrum R) ∈ U → f ∉ P →
          (2 : WithBot ℕ∞) ≤ ringKrullDim (R ⧸ P))
theorem

exists_punctured_hypersurface_neighborhood_faithful

L106 ↗
AlgebraicGeometry.FiniteEtale.exists_punctured_hypersurface_neighborhood_faithful
Documentation

A punctured hypersurface admits a neighbourhood on which finite étale restriction is faithful, and faithfulness persists for every smaller open neighbourhood. This uses only the original Noetherian local hypotheses and an equation in the maximal ideal.

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_punctured_hypersurface_neighborhood_faithful
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (f : R) (hf : f ∈ maximalIdeal R) :
    ∃ U : (Spec (.of R)).Opens,
      U ≤ Scheme.puncturedSpectrumOpen R ∧
      (∀ p : PrimeSpectrum R,
        p ∈ Scheme.puncturedSpectrumOpen R → f ∈ p.asIdeal → p ∈ U) ∧
      (∀ V : (Spec (.of R)).Opens, V ≤ U →
        (∀ p : PrimeSpectrum R,
          p ∈ Scheme.puncturedSpectrumOpen R → f ∈ p.asIdeal → p ∈ V) →
        (FiniteEtale.pullback (pullback.fst V.ι
          (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.