Module

BaseMinimalPrimePuncturedPurity.lean

Nyll.EtaleFundamentalGroups.Purity.SpecialLocal.BaseMinimalPrimePuncturedPurity

16 declarations indexed from sourceView source ↗

Module documentation

The punctured cover at a minimal non-etale base point

A finite algebra over a local ring which is etale at every target prime away from the closed point restricts to a finite-etale cover of the punctured spectrum. Applying this to the localization at a minimal base cotangent- support point packages the prime-local result of BaseMinimalPrimeLocalization as the cover needed by punctured purity.

Imports7

Imported by3

theorem

eqToHom_stalk_eq_stalkCongr

L35 ↗

EtaleFundamentalGroups.SpecialLocalPurity.eqToHom_stalk_eq_stalkCongr

Source context 6 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u

Lean source · full declaration

theorem eqToHom_stalk_eq_stalkCongr
    (Z : Scheme.{u}) {z z' : Z} (h : z = z') :
    eqToHom (congrArg (fun w ↦ Z.presheaf.stalk w) h) =
      (Z.presheaf.stalkCongr (.of_eq h)).hom := by
  subst z'
  simp

theorem

functionFieldMap_eq_of_eq

L42 ↗

EtaleFundamentalGroups.SpecialLocalPurity.functionFieldMap_eq_of_eq

Source context 6 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u

Lean source · statement

theorem functionFieldMap_eq_of_eq
    {T S : Scheme.{u}} [IsIntegral T] [IsIntegral S]
    (a b : S ⟶ T) (hab : a = b)
    (ha : DenseRange a) (hb : DenseRange b) :
    a.functionFieldMap ha = b.functionFieldMap hb

theorem

specFunctionField_algebraMap_ΓSpecIso_hom

L50 ↗

EtaleFundamentalGroups.SpecialLocalPurity.specFunctionField_algebraMap_ΓSpecIso_hom

Source context 6 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u

Lean source · full declaration

theorem specFunctionField_algebraMap_ΓSpecIso_hom
    (R : Type u) [CommRing R] [IsDomain R]
    (r : Γ(Spec (.of R), ⊤)) :
    let X := Spec (.of R)
    letI : Nonempty (⊤ : X.Opens) :=
      ⟨⟨genericPoint X, by trivial⟩⟩
    letI : Algebra R X.functionField :=
      AlgebraicGeometry.instAlgebraCarrierFunctionFieldSpec (.of R)
    algebraMap R X.functionField ((Scheme.ΓSpecIso (.of R)).hom r) =
      X.germToFunctionField ⊤ r := by
  dsimp only
  let X := Spec (.of R)
  let : Nonempty (⊤ : X.Opens) :=
    ⟨⟨genericPoint X, by trivial⟩⟩
  change X.presheaf.germ ⊤ (genericPoint X) (by trivial)
      ((Scheme.ΓSpecIso (.of R)).inv
        ((Scheme.ΓSpecIso (.of R)).hom r)) =
    X.presheaf.germ ⊤ (genericPoint X) (by trivial) r
  exact congrArg (fun s ↦
    X.presheaf.germ ⊤ (genericPoint X) (by trivial) s)
      (Iso.hom_inv_id_apply (Scheme.ΓSpecIso (.of R)) r)

theorem

puncturedRestriction_nonempty_of_injective

L75 ↗

EtaleFundamentalGroups.SpecialLocalPurity.puncturedRestriction_nonempty_of_injective

Documentation

If the finite algebra map is injective and the local base has positive dimension, the inverse image of its puncture is nonempty: it contains the generic point of the target spectrum.

Source context 6 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u

Lean source · full declaration

theorem puncturedRestriction_nonempty_of_injective
    {A B : Type u} [CommRing A] [IsDomain A] [IsLocalRing A]
    [CommRing B] [IsDomain B] [Algebra A B]
    (hinj : Function.Injective (algebraMap A B))
    (hpos : (1 : WithBot ℕ∞) ≤ ringKrullDim A) :
    let f : Spec (.of B) ⟶ Spec (.of A) :=
      Spec.map (CommRingCat.ofHom (algebraMap A B))
    Nonempty (f ⁻¹ᵁ Scheme.puncturedSpectrumOpen A) := by
  dsimp only
  let f : Spec (.of B) ⟶ Spec (.of A) :=
    Spec.map (CommRingCat.ofHom (algebraMap A B))
  let etaA : PrimeSpectrum A := ⟨⊥, inferInstance⟩
  let etaB : PrimeSpectrum B := ⟨⊥, inferInstance⟩
  have hmap : f etaB = etaA := by
    apply PrimeSpectrum.ext
    change Ideal.comap (algebraMap A B) ⊥ = ⊥
    exact Ideal.comap_bot_of_injective (algebraMap A B) hinj
  have hmaximal : maximalIdeal A ≠ ⊥ := by
    intro hmaximal
    have hdimZero : ringKrullDim A = 0 := by
      rw [← maximalIdeal_height_eq_ringKrullDim, hmaximal,
        Ideal.height_bot]
      simp
    rw [hdimZero] at hpos
    exact (not_le_of_gt (by norm_num : (0 : WithBot ℕ∞) < 1)) hpos
  have heta : etaA ∈ Scheme.puncturedSpectrumOpen A := by
    rw [Scheme.mem_puncturedSpectrumOpen_iff]
    intro h
    apply hmaximal
    exact (congrArg PrimeSpectrum.asIdeal h).symm
  refine ⟨⟨etaB, ?_⟩⟩
  change f etaB ∈ Scheme.puncturedSpectrumOpen A
  rw [hmap]
  exact heta

theorem

puncturedRestriction_connectedSpace_of_injective

L113 ↗

EtaleFundamentalGroups.SpecialLocalPurity.puncturedRestriction_connectedSpace_of_injective

Documentation

Under the same hypotheses, the inverse image of the puncture is connected, since it is a nonempty open subscheme of an integral affine scheme.

Source context 6 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u

Lean source · full declaration

theorem puncturedRestriction_connectedSpace_of_injective
    {A B : Type u} [CommRing A] [IsDomain A] [IsLocalRing A]
    [CommRing B] [IsDomain B] [Algebra A B]
    (hinj : Function.Injective (algebraMap A B))
    (hpos : (1 : WithBot ℕ∞) ≤ ringKrullDim A) :
    let f : Spec (.of B) ⟶ Spec (.of A) :=
      Spec.map (CommRingCat.ofHom (algebraMap A B))
    ConnectedSpace (f ⁻¹ᵁ Scheme.puncturedSpectrumOpen A) := by
  dsimp only
  let f : Spec (.of B) ⟶ Spec (.of A) :=
    Spec.map (CommRingCat.ofHom (algebraMap A B))
  let V : (Spec (.of B)).Opens :=
    f ⁻¹ᵁ Scheme.puncturedSpectrumOpen A
  let : Nonempty V :=
    puncturedRestriction_nonempty_of_injective hinj hpos
  let : IsIntegral (V : Scheme) := inferInstance
  exact inferInstance

theorem

puncturedRestriction_isFiniteEtale_of_isEtaleAt_away_from_closedPoint

L134 ↗

EtaleFundamentalGroups.SpecialLocalPurity.puncturedRestriction_isFiniteEtale_of_isEtaleAt_away_from_closedPoint

Documentation

A finite algebra which is etale at every target prime away from the closed point gives a finite-etale cover after restricting its spectrum to the punctured spectrum of the base.

Source context 6 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u

Lean source · full declaration

theorem puncturedRestriction_isFiniteEtale_of_isEtaleAt_away_from_closedPoint
    {A B : Type u} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    [CommRing B] [Algebra A B] [Module.Finite A B]
    (haway :
      ∀ Q : PrimeSpectrum B,
        PrimeSpectrum.comap (algebraMap A B) Q ≠
          ⟨maximalIdeal A, inferInstance⟩ →
        Algebra.IsEtaleAt A Q.asIdeal) :
    let f : Spec (.of B) ⟶ Spec (.of A) :=
      Spec.map (CommRingCat.ofHom (algebraMap A B))
    IsFiniteEtale (f ∣_ Scheme.puncturedSpectrumOpen A) := by
  dsimp only
  let f : Spec (.of B) ⟶ Spec (.of A) :=
    Spec.map (CommRingCat.ofHom (algebraMap A B))
  let U : (Spec (.of A)).Opens := Scheme.puncturedSpectrumOpen A
  have hf : IsFinite f := by
    rw [IsFinite.SpecMap_iff]
    change (algebraMap A B).Finite
    exact RingHom.finite_algebraMap.mpr inferInstance
  have hwFinite : IsFinite (f ∣_ U) :=
    MorphismProperty.of_isPullback
      (isPullback_morphismRestrict f U).flip hf
  let : IsFinite (f ∣_ U) := hwFinite
  have hwEtale : Etale (f ∣_ U) := by
    apply EtaleFundamentalGroups.etale_of_stalkMap_formallyEtale
    intro y
    let Q : PrimeSpectrum B := y.1
    have hQaway :
        PrimeSpectrum.comap (algebraMap A B) Q ≠
          ⟨maximalIdeal A, inferInstance⟩ := by
      have hy : f Q ∈ Scheme.puncturedSpectrumOpen A := y.2
      have hne : f Q ≠ closedPoint (CommRingCat.of A) :=
        (Scheme.mem_puncturedSpectrumOpen_iff A (f Q)).mp hy
      change PrimeSpectrum.comap (algebraMap A B) Q ≠
        ⟨maximalIdeal A, inferInstance⟩ at hne
      exact hne
    have hEtale : Algebra.IsEtaleAt A Q.asIdeal := haway Q hQaway
    let q : Ideal A := Q.asIdeal.under A
    let : q.IsPrime := inferInstance
    let : Q.asIdeal.LiesOver q := inferInstance
    let : Algebra (Localization.AtPrime q)
        (Localization.AtPrime Q.asIdeal) :=
      Localization.AtPrime.algebraOfLiesOver q Q.asIdeal
    have hlocal : Algebra.FormallyEtale (Localization.AtPrime q)
        (Localization.AtPrime Q.asIdeal) := by
      let : Algebra.FormallyEtale A (Localization.AtPrime Q.asIdeal) :=
        hEtale
      exact Algebra.FormallyEtale.localization_base q.primeCompl
    have hSpec : (f.stalkMap Q).hom.FormallyEtale := by
      apply
        (EtaleFundamentalGroups.RingHom.FormallyEtale.respectsIso.arrow_mk_iso_iff
          (Scheme.arrowStalkMapSpecIso
            (CommRingCat.ofHom (algebraMap A B)) Q)).mpr
      change (Localization.localRingHom q Q.asIdeal
        (algebraMap A B) rfl).FormallyEtale
      exact hlocal
    exact
      (EtaleFundamentalGroups.RingHom.FormallyEtale.respectsIso.arrow_mk_iso_iff
        (morphismRestrictStalkMap f U y)).mpr hSpec
  let : Etale (f ∣_ U) := hwEtale
  exact ⟨⟩

def

puncturedRestrictionFiniteEtale

L198 ↗

EtaleFundamentalGroups.SpecialLocalPurity.puncturedRestrictionFiniteEtale

Documentation

The finite-etale cover of the puncture obtained from a finite algebra which is etale away from the closed point.

Source context 6 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u

Lean source · statement

def puncturedRestrictionFiniteEtale
    {A B : Type u} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    [CommRing B] [Algebra A B] [Module.Finite A B]
    (haway :
      ∀ Q : PrimeSpectrum B,
        PrimeSpectrum.comap (algebraMap A B) Q ≠
          ⟨maximalIdeal A, inferInstance⟩ →
        Algebra.IsEtaleAt A Q.asIdeal) :
    FiniteEtale (Scheme.puncturedSpectrum A)

theorem

puncturedRestrictionFiniteEtale_isConnected

L216 ↗

EtaleFundamentalGroups.SpecialLocalPurity.puncturedRestrictionFiniteEtale_isConnected

Documentation

If both rings are domains, the cover above is connected whenever the base map is injective and the local base has positive dimension.

Source context 6 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u

Lean source · statement

theorem puncturedRestrictionFiniteEtale_isConnected
    {A B : Type u} [CommRing A] [IsDomain A] [IsLocalRing A]
    [IsNoetherianRing A] [CommRing B] [IsDomain B]
    [Algebra A B] [Module.Finite A B]
    (haway :
      ∀ Q : PrimeSpectrum B,
        PrimeSpectrum.comap (algebraMap A B) Q ≠
          ⟨maximalIdeal A, inferInstance⟩ →
        Algebra.IsEtaleAt A Q.asIdeal)
    (hinj : Function.Injective (algebraMap A B))
    (hpos : (1 : WithBot ℕ∞) ≤ ringKrullDim A) :
    CategoryTheory.PreGaloisCategory.IsConnected
      (puncturedRestrictionFiniteEtale haway)

theorem

finiteNormalDomainAlgebra_etale_of_hasPuncturedPurity_of_isEtaleAt_away_from_closedPoint

L247 ↗

EtaleFundamentalGroups.SpecialLocalPurity.finiteNormalDomainAlgebra_etale_of_hasPuncturedPurity_of_isEtaleAt_away_from_closedPoint

Documentation

Punctured purity removes the only possible closed-point ramification of a finite normal domain algebra.

Source context 6 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u

Lean source · statement

theorem finiteNormalDomainAlgebra_etale_of_hasPuncturedPurity_of_isEtaleAt_away_from_closedPoint
    {A B : Type u}
    [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
    [IsLocalRing A] [IsNoetherianRing A]
    [CommRing B] [IsDomain B] [IsIntegrallyClosed B]
    [Algebra A B] [Module.Finite A B]
    (hpos : (1 : WithBot ℕ∞) ≤ ringKrullDim A)
    (hpurity : AlgebraicGeometry.FiniteEtale.HasPuncturedPurity A)
    (haway :
      ∀ Q : PrimeSpectrum B,
        PrimeSpectrum.comap (algebraMap A B) Q ≠
          ⟨maximalIdeal A, inferInstance⟩ →
        Algebra.IsEtaleAt A Q.asIdeal)
    (hinj : Function.Injective (algebraMap A B)) :
    Algebra.Etale A B

theorem

localizedFiniteAlgebra_puncturedRestriction_isFiniteEtale_of_minimal_base_nonEtaleCotangentSupport

L459 ↗

EtaleFundamentalGroups.SpecialLocalPurity.localizedFiniteAlgebra_puncturedRestriction_isFiniteEtale_of_minimal_base_nonEtaleCotangentSupport

Documentation

At a minimal base cotangent-support point, the localized finite algebra restricts to a finite-etale cover of the punctured local spectrum.

Source context 6 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u

Lean source · full declaration

theorem
localizedFiniteAlgebra_puncturedRestriction_isFiniteEtale_of_minimal_base_nonEtaleCotangentSupport
    {R S : Type u} [CommRing R] [IsNoetherianRing R]
    [CommRing S] [Algebra R S] [Module.Finite R S]
    (p : PrimeSpectrum R)
    (hp : Minimal
      (· ∈ Module.support R Ω[S⁄R] ∪
        Module.support R (Algebra.H1Cotangent R S)) p) :
    let A := Localization.AtPrime p.asIdeal
    let B := Localization
      (Algebra.algebraMapSubmonoid S p.asIdeal.primeCompl)
    let f : Spec (.of B) ⟶ Spec (.of A) :=
      Spec.map (CommRingCat.ofHom (algebraMap A B))
    IsFiniteEtale (f ∣_ Scheme.puncturedSpectrumOpen A) := by
  dsimp only
  apply puncturedRestriction_isFiniteEtale_of_isEtaleAt_away_from_closedPoint
  intro Q hQ
  exact
    localizedFiniteAlgebra_isEtaleAt_away_from_closedPoint_of_minimal_base_nonEtaleCotangentSupport
      p hp Q hQ

theorem

localizedFiniteNormalDomainAlgebra_etale_of_minimalBadPuncturedPurity

L482 ↗

EtaleFundamentalGroups.SpecialLocalPurity.localizedFiniteNormalDomainAlgebra_etale_of_minimalBadPuncturedPurity

Documentation

Punctured purity at a minimal base cotangent-support point upgrades the localized finite normal-domain algebra from punctured etale to etale.

Source context 6 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u

Lean source · statement

theorem
    localizedFiniteNormalDomainAlgebra_etale_of_minimalBadPuncturedPurity
    {R S : Type u}
    [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    [IsNoetherianRing R]
    [CommRing S] [IsDomain S] [IsIntegrallyClosed S]
    [Algebra R S] [Module.Finite R S]
    (hinj : Function.Injective (algebraMap R S))
    (p : PrimeSpectrum R)
    (hp : Minimal
      (· ∈ Module.support R Ω[S⁄R] ∪
        Module.support R (Algebra.H1Cotangent R S)) p)
    (hpos : (1 : WithBot ℕ∞) ≤
      ringKrullDim (Localization.AtPrime p.asIdeal))
    (hpurity : AlgebraicGeometry.FiniteEtale.HasPuncturedPurity
      (Localization.AtPrime p.asIdeal)) :
    Algebra.Etale (Localization.AtPrime p.asIdeal)
      (Localization
        (Algebra.algebraMapSubmonoid S p.asIdeal.primeCompl))

theorem

isEtaleAt_under_of_localizedAlgebra_etale

L529 ↗

EtaleFundamentalGroups.SpecialLocalPurity.isEtaleAt_under_of_localizedAlgebra_etale

Documentation

Etaleness of the simultaneous localization at a base prime descends, after localizing once more, to the original map at the prime below a target prime.

Source context 6 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u

Lean source · statement

theorem isEtaleAt_under_of_localizedAlgebra_etale
    {R S : Type u} [CommRing R] [CommRing S]
    [Algebra R S]
    (p : PrimeSpectrum R)
    (hEtale : Algebra.Etale (Localization.AtPrime p.asIdeal)
      (Localization
        (Algebra.algebraMapSubmonoid S p.asIdeal.primeCompl)))
    (Q : PrimeSpectrum
      (Localization
        (Algebra.algebraMapSubmonoid S p.asIdeal.primeCompl))) :
    Algebra.IsEtaleAt R
      (PrimeSpectrum.comap
        (algebraMap S
          (Localization
            (Algebra.algebraMapSubmonoid S p.asIdeal.primeCompl))) Q).asIdeal

theorem

isEtaleAt_of_localizedAlgebra_etale

L549 ↗

EtaleFundamentalGroups.SpecialLocalPurity.isEtaleAt_of_localizedAlgebra_etale

Documentation

If a target prime lies over p, etaleness of the simultaneous localization at p implies etaleness of the original algebra at that target prime.

Source context 6 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u

Lean source · statement

theorem isEtaleAt_of_localizedAlgebra_etale
    {R S : Type u} [CommRing R] [CommRing S]
    [Algebra R S]
    (p : PrimeSpectrum R)
    (hEtale : Algebra.Etale (Localization.AtPrime p.asIdeal)
      (Localization
        (Algebra.algebraMapSubmonoid S p.asIdeal.primeCompl)))
    (P : PrimeSpectrum S)
    (hPp : PrimeSpectrum.comap (algebraMap R S) P = p) :
    Algebra.IsEtaleAt R P.asIdeal

theorem

not_minimal_base_nonEtaleCotangentSupport_of_hasPuncturedPurity

L563 ↗

EtaleFundamentalGroups.SpecialLocalPurity.not_minimal_base_nonEtaleCotangentSupport_of_hasPuncturedPurity

Documentation

A minimal point of the two cotangent supports cannot persist when its positive-dimensional local ring has punctured purity.

Source context 6 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u

Lean source · statement

theorem not_minimal_base_nonEtaleCotangentSupport_of_hasPuncturedPurity
    {R S : Type u}
    [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    [IsNoetherianRing R]
    [CommRing S] [IsDomain S] [IsIntegrallyClosed S]
    [Algebra R S] [Module.Finite R S]
    (hinj : Function.Injective (algebraMap R S))
    (p : PrimeSpectrum R)
    (hp : Minimal
      (· ∈ Module.support R Ω[S⁄R] ∪
        Module.support R (Algebra.H1Cotangent R S)) p)
    (hpos : (1 : WithBot ℕ∞) ≤
      ringKrullDim (Localization.AtPrime p.asIdeal))
    (hpurity : AlgebraicGeometry.FiniteEtale.HasPuncturedPurity
      (Localization.AtPrime p.asIdeal)) : False

theorem

finiteNormalDomainAlgebra_formallyEtale_of_minimalBadPuncturedPurity

L613 ↗

EtaleFundamentalGroups.SpecialLocalPurity.finiteNormalDomainAlgebra_formallyEtale_of_minimalBadPuncturedPurity

Documentation

A finite normal-domain algebra is formally etale if punctured purity and positive local dimension hold at every hypothetical minimal cotangent-support point.

Source context 6 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u

Lean source · statement

theorem
    finiteNormalDomainAlgebra_formallyEtale_of_minimalBadPuncturedPurity
    {R S : Type u}
    [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    [IsNoetherianRing R]
    [CommRing S] [IsDomain S] [IsIntegrallyClosed S]
    [Algebra R S] [Module.Finite R S]
    (hinj : Function.Injective (algebraMap R S))
    (hpos : ∀ (p : PrimeSpectrum R),
      Minimal
        (· ∈ Module.support R Ω[S⁄R] ∪
          Module.support R (Algebra.H1Cotangent R S)) p →
      (1 : WithBot ℕ∞) ≤ ringKrullDim (Localization.AtPrime p.asIdeal))
    (hpurity : ∀ (p : PrimeSpectrum R),
      Minimal
        (· ∈ Module.support R Ω[S⁄R] ∪
          Module.support R (Algebra.H1Cotangent R S)) p →
      AlgebraicGeometry.FiniteEtale.HasPuncturedPurity
        (Localization.AtPrime p.asIdeal)) :
    Algebra.FormallyEtale R S

theorem

finiteNormalDomainAlgebra_etale_of_hasPuncturedPurity_at_minimal_base_nonEtaleCotangentSupport

L642 ↗

EtaleFundamentalGroups.SpecialLocalPurity.finiteNormalDomainAlgebra_etale_of_hasPuncturedPurity_at_minimal_base_nonEtaleCotangentSupport

Documentation

Under the same hypotheses, module-finiteness over the Noetherian base supplies finite presentation, so the algebra is etale.

Source context 6 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u

Lean source · statement

theorem
    finiteNormalDomainAlgebra_etale_of_hasPuncturedPurity_at_minimal_base_nonEtaleCotangentSupport
    {R S : Type u}
    [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    [IsNoetherianRing R]
    [CommRing S] [IsDomain S] [IsIntegrallyClosed S]
    [Algebra R S] [Module.Finite R S]
    (hinj : Function.Injective (algebraMap R S))
    (hpos : ∀ (p : PrimeSpectrum R),
      Minimal
        (· ∈ Module.support R Ω[S⁄R] ∪
          Module.support R (Algebra.H1Cotangent R S)) p →
      (1 : WithBot ℕ∞) ≤ ringKrullDim (Localization.AtPrime p.asIdeal))
    (hpurity : ∀ (p : PrimeSpectrum R),
      Minimal
        (· ∈ Module.support R Ω[S⁄R] ∪
          Module.support R (Algebra.H1Cotangent R S)) p →
      AlgebraicGeometry.FiniteEtale.HasPuncturedPurity
        (Localization.AtPrime p.asIdeal)) :
    Algebra.Etale R S

Module documentation

The punctured cover at a minimal non-etale base point

Declarations