NYLL
Module

PuncturedHypersurfaceNeighborhoodFaithful.lean

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

Module documentation

Faithful restriction from a neighbourhood of a punctured hypersurface

Let U be an open neighbourhood of the punctured hypersurface V(f) in the spectrum of a Noetherian local ring. Only minimal primes lying in U and outside V(f) need the quotient-dimension-at-least-two condition. Under that condition, each connected component of U meets the hypersurface, and the actual finite étale restriction functor is faithful.

This is the neighbourhood faithfulness implication of Stacks Project, Tag 0BLN. The existence of a suitable neighbourhood and the statement about the colimit of neighbourhood categories are separate assertions.

Imports9
Imported by3

Declarations

theorem

exists_hypersurface_point_in_neighborhood_connectedComponent

L43 ↗
AlgebraicGeometry.FiniteEtale.exists_hypersurface_point_in_neighborhood_connectedComponent
Documentation

Every component of the neighbourhood meets the hypersurface if its minimal primes outside the hypersurface have quotient dimension at least two. The open need not itself be contained in the punctured spectrum.

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

pullback_faithful_punctured_hypersurface_neighborhood_of_minimalPrime_dimension

L90 ↗
AlgebraicGeometry.FiniteEtale.pullback_faithful_punctured_hypersurface_neighborhood_of_minimalPrime_dimension
Documentation

Finite étale restriction from a neighbourhood of the punctured hypersurface is faithful under the minimal-prime dimension hypothesis of Stacks 58.22.1 (0BLN). The target is the literal pullback of V(f) to the chosen open. In particular this applies to opens inside 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 pullback_faithful_punctured_hypersurface_neighborhood_of_minimalPrime_dimension
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (f : R) (hf : f ∈ maximalIdeal R)
    (U : (Spec (.of R)).Opens)
    (hzero : ∀ p : PrimeSpectrum R,
      p ∈ Scheme.puncturedSpectrumOpen R → f ∈ p.asIdeal → p ∈ U)
    (hdim : ∀ (P : Ideal R) (hP : P ∈ minimalPrimes R),
      (⟨P, hP.isPrime⟩ : PrimeSpectrum R) ∈ U → f ∉ P →
        (2 : WithBot ℕ∞) ≤ ringKrullDim (R ⧸ P)) :
    (FiniteEtale.pullback (pullback.fst U.ι
      (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.