Module

PuncturedSpectrumParameterInduction.lean

Nyll.EtaleFundamentalGroups.Purity.PuncturedSpectrumParameterInduction

2 declarations indexed from sourceView source ↗

Module documentation

The categorical hypersurface step for punctured local purity

For a complete Noetherian local ring, finite-etale covers of a quotient lift uniquely to the ambient affine spectrum. If restriction from the ambient puncture to the quotient puncture is fully faithful, purity for the quotient therefore implies purity for the ambient ring. This isolates the genuine local Lefschetz input from the already formalized complete-quotient lifting.

Imports2

Imported by2

theorem

hasPuncturedPurity_of_complete_quotient_of_fullyFaithful

L36 ↗

EtaleFundamentalGroups.hasPuncturedPurity_of_complete_quotient_of_fullyFaithful

Documentation

The complete hypersurface induction step for local purity.

The first hypothesis is purity one dimension lower. The second is the substantive local-Lefschetz assertion that a finite-etale cover, and every map between such covers, is determined on the quotient puncture. The conclusion is obtained by lifting the lower-dimensional extension across the complete quotient and then reflecting its comparison isomorphism through that fully faithful restriction functor.

Source context 4 commands

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

noncomputable section
open CategoryTheory IsLocalRing
namespace EtaleFundamentalGroups
universe u

Lean source · full declaration

theorem hasPuncturedPurity_of_complete_quotient_of_fullyFaithful
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    [IsAdicComplete (maximalIdeal R) R]
    (I : Ideal R) (hI : I ≤ maximalIdeal R) :
    letI : Nontrivial (R ⧸ I) :=
      Ideal.Quotient.nontrivial_iff.mpr
        (ne_top_of_le_ne_top (maximalIdeal.isMaximal R).ne_top hI)
    letI : IsLocalRing (R ⧸ I) :=
      IsLocalRing.of_surjective' (Ideal.Quotient.mk I)
        Ideal.Quotient.mk_surjective
    AlgebraicGeometry.FiniteEtale.HasPuncturedPurity (R ⧸ I) →
      (AlgebraicGeometry.FiniteEtale.pullback
        (AlgebraicGeometry.Scheme.puncturedSpectrumQuotientMorphism
          R I hI)).FullyFaithful →
      AlgebraicGeometry.FiniteEtale.HasPuncturedPurity R := by
  let : Nontrivial (R ⧸ I) :=
    Ideal.Quotient.nontrivial_iff.mpr
      (ne_top_of_le_ne_top (maximalIdeal.isMaximal R).ne_top hI)
  let : IsLocalRing (R ⧸ I) :=
    IsLocalRing.of_surjective' (Ideal.Quotient.mk I)
      Ideal.Quotient.mk_surjective
  intro hquotient hlefschetz
  rw [AlgebraicGeometry.FiniteEtale.hasPuncturedPurity_iff] at hquotient ⊢
  intro W
  let j := AlgebraicGeometry.Scheme.puncturedSpectrumInclusion R
  let jI :=
    AlgebraicGeometry.Scheme.puncturedSpectrumInclusion (R ⧸ I)
  let q := AlgebraicGeometry.Spec.map
    (CommRingCat.ofHom (Ideal.Quotient.mk I))
  let g := AlgebraicGeometry.Scheme.puncturedSpectrumQuotientMorphism
    R I hI
  let Fj := AlgebraicGeometry.FiniteEtale.pullback j
  let FjI := AlgebraicGeometry.FiniteEtale.pullback jI
  let Fq := AlgebraicGeometry.FiniteEtale.pullback q
  let Fg := AlgebraicGeometry.FiniteEtale.pullback g
  let WI := Fg.obj W
  obtain ⟨ZI, ⟨eZI⟩⟩ := hquotient WI
  let : Fq.IsEquivalence := by
    dsimp only [Fq, q]
    exact finiteEtale_pullback_isEquivalence_of_complete_quotient I hI
  obtain ⟨Z, ⟨eZ⟩⟩ :=
    (inferInstance : Fq.EssSurj).mem_essImage ZI
  let eSquare : Fg.obj (Fj.obj Z) ≅ FjI.obj (Fq.obj Z) :=
    (AlgebraicGeometry.Scheme.puncturedSpectrumQuotientPullbackIso
      R I hI).app Z
  let eRestricted : Fg.obj (Fj.obj Z) ≅ Fg.obj W :=
    eSquare ≪≫ FjI.mapIso eZ ≪≫ eZI
  refine ⟨Z, ⟨?_⟩⟩
  exact hlefschetz.preimageIso eRestricted

theorem

hasPuncturedPurity_of_complete_quotient_of_preserves_connected

L93 ↗

EtaleFundamentalGroups.hasPuncturedPurity_of_complete_quotient_of_preserves_connected