Nyll.EtaleFundamentalGroups.Purity.PuncturedHypersurfaceEventualEquality

Module documentation

Equality of finite étale morphisms after shrinking a neighbourhood

For a Noetherian local ring and an equation in its maximal ideal, any open containing the punctured hypersurface has a smaller such neighbourhood on which equality of finite étale morphisms is detected by the hypersurface. The smaller neighbourhood is the intersection with the faithful neighbourhood constructed by deleting the bad minimal components.

The proof compares the actual iterated pullbacks along the resulting commutative square. The shrinking neighbourhood works simultaneously for all covers and morphisms on the given open.

This is the eventual-equality assertion needed for faithfulness on germs in Stacks Project, Tag 0BLN. No category of germs or categorical colimit is constructed here.

theorem

exists_punctured_hypersurface_neighborhood_restriction_eq

L54 ↗

AlgebraicGeometry.FiniteEtale.exists_punctured_hypersurface_neighborhood_restriction_eq

Documentation

An open containing the punctured hypersurface admits one smaller open inside the puncture on which every two finite étale morphisms agreeing on the hypersurface become equal. The covers and the morphisms are arbitrary objects and morphisms over the original open W.

If W is itself contained in the puncture, its hypersurface pullback is precisely the punctured hypersurface occurring in the neighbourhood system.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits IsLocalRing
namespace AlgebraicGeometry.FiniteEtale
attribute [local instance] finiteEtaleOverCategoryCoherence
  finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence

Lean source · statement

theorem exists_punctured_hypersurface_neighborhood_restriction_eq
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (f : R) (hf : f ∈ maximalIdeal R)
    (W : (Spec (.of R)).Opens)
    (hWzero : ∀ p : PrimeSpectrum R,
      p ∈ Scheme.puncturedSpectrumOpen R → f ∈ p.asIdeal → p ∈ W) :
    ∃ (V : (Spec (.of R)).Opens) (hVW : V ≤ W),
      V ≤ Scheme.puncturedSpectrumOpen R ∧
      (∀ p : PrimeSpectrum R,
        p ∈ Scheme.puncturedSpectrumOpen R → f ∈ p.asIdeal → p ∈ V) ∧
      ∀ (A B : FiniteEtale W.toScheme) (α β : A ⟶ B),
        (FiniteEtale.pullback (Limits.pullback.fst W.ι
          (Spec.map (CommRingCat.ofHom
            (Ideal.Quotient.mk (Ideal.span {f})))))).map α =
        (FiniteEtale.pullback (Limits.pullback.fst W.ι
          (Spec.map (CommRingCat.ofHom
            (Ideal.Quotient.mk (Ideal.span {f})))))).map β →
        (FiniteEtale.pullback ((Spec (.of R)).homOfLE hVW)).map α =
          (FiniteEtale.pullback ((Spec (.of R)).homOfLE hVW)).map β

Module documentation

Equality of finite étale morphisms after shrinking a neighbourhood

Declarations

exists_punctured_hypersurface_neighborhood_restriction_eq