Module

BaseMinimalPrimeGenericEtalePurity.lean

Nyll.EtaleFundamentalGroups.Purity.SpecialLocal.BaseMinimalPrimeGenericEtalePurity

8 declarations indexed from sourceView source ↗

Module documentation

Generic etaleness supplies positive-dimensional minimal bad localizations

A minimal point of the base cotangent support of a finite domain algebra cannot have height zero when the algebra is etale at its generic point. Consequently its prime localization has positive Krull dimension. This removes the numerical hypothesis from the minimal-bad-point purity argument.

Imports1

Nyll.EtaleFundamentalGroups.Purity.SpecialLocal.BaseMinimalPrimePuncturedPurity

Imported by1

Nyll.EtaleFundamentalGroups.Purity.SpecialLocal.All

theorem

one_le_ringKrullDim_localizationAtPrime_of_height_ne_zero

L25 ↗

EtaleFundamentalGroups.SpecialLocalPurity.one_le_ringKrullDim_localizationAtPrime_of_height_ne_zero

Documentation

A prime of nonzero height has positive-dimensional prime localization.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u

Lean source · statement

theorem one_le_ringKrullDim_localizationAtPrime_of_height_ne_zero
    {R : Type u} [CommRing R]
    (p : PrimeSpectrum R) (hp : p.asIdeal.height ≠ 0) :
    (1 : WithBot ℕ∞) ≤
      ringKrullDim (Localization.AtPrime p.asIdeal)

theorem

minimal_base_nonEtaleCotangentSupport_height_ne_zero_of_isEtaleAt_bot

L37 ↗

EtaleFundamentalGroups.SpecialLocalPurity.minimal_base_nonEtaleCotangentSupport_height_ne_zero_of_isEtaleAt_bot

Documentation

Generic etaleness excludes height zero for every minimal point of the base cotangent support of a finite domain algebra.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u

Lean source · statement

theorem
    minimal_base_nonEtaleCotangentSupport_height_ne_zero_of_isEtaleAt_bot
    {R S : Type u}
    [CommRing R] [IsDomain R] [IsNoetherianRing R]
    [CommRing S] [IsDomain S]
    [Algebra R S] [Module.Finite R S]
    (hgeneric : Algebra.IsEtaleAt R (⊥ : Ideal S))
    (p : PrimeSpectrum R)
    (hp : Minimal
      (· ∈ Module.support R Ω[S⁄R] ∪
        Module.support R (Algebra.H1Cotangent R S)) p) :
    p.asIdeal.height ≠ 0

theorem

minimal_base_nonEtaleCotangentSupport_height_ne_one_of_isEtaleAt_heightOne

L75 ↗

EtaleFundamentalGroups.SpecialLocalPurity.minimal_base_nonEtaleCotangentSupport_height_ne_one_of_isEtaleAt_heightOne

Documentation

Etaleness over every height-one base prime excludes height one for every minimal point of the base cotangent support.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u

Lean source · statement

theorem
    minimal_base_nonEtaleCotangentSupport_height_ne_one_of_isEtaleAt_heightOne
    {R S : Type u}
    [CommRing R] [IsNoetherianRing R]
    [CommRing S]
    [Algebra R S] [Module.Finite R S]
    (hetale :
      ∀ (q : Ideal R) [q.IsPrime], q.height = 1 →
        ∀ (Q : Ideal S) [Q.IsPrime] [Q.LiesOver q],
          Algebra.IsEtaleAt R Q)
    (p : PrimeSpectrum R)
    (hp : Minimal
      (· ∈ Module.support R Ω[S⁄R] ∪
        Module.support R (Algebra.H1Cotangent R S)) p) :
    p.asIdeal.height ≠ 1

theorem

one_le_ringKrullDim_localizationAtPrime_of_minimal_base_nonEtaleCotangentSupport_of_isEtaleAt_bot

L115 ↗

EtaleFundamentalGroups.SpecialLocalPurity.one_le_ringKrullDim_localizationAtPrime_of_minimal_base_nonEtaleCotangentSupport_of_isEtaleAt_bot

Documentation

At a minimal bad base point of a generically etale finite domain algebra, the local base has positive Krull dimension.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u

Lean source · statement

theorem
one_le_ringKrullDim_localizationAtPrime_of_minimal_base_nonEtaleCotangentSupport_of_isEtaleAt_bot
    {R S : Type u}
    [CommRing R] [IsDomain R] [IsNoetherianRing R]
    [CommRing S] [IsDomain S]
    [Algebra R S] [Module.Finite R S]
    (hgeneric : Algebra.IsEtaleAt R (⊥ : Ideal S))
    (p : PrimeSpectrum R)
    (hp : Minimal
      (· ∈ Module.support R Ω[S⁄R] ∪
        Module.support R (Algebra.H1Cotangent R S)) p) :
    (1 : WithBot ℕ∞) ≤
      ringKrullDim (Localization.AtPrime p.asIdeal)

theorem

finiteNormalDomainAlgebra_formallyEtale_of_genericEtale_of_minimalBadPuncturedPurity

L135 ↗

EtaleFundamentalGroups.SpecialLocalPurity.finiteNormalDomainAlgebra_formallyEtale_of_genericEtale_of_minimalBadPuncturedPurity

Documentation

A generically etale finite normal-domain algebra is formally etale when the localizations at all hypothetical minimal bad base points have punctured purity.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u

Lean source · statement

theorem
    finiteNormalDomainAlgebra_formallyEtale_of_genericEtale_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))
    (hgeneric : Algebra.IsEtaleAt R (⊥ : Ideal S))
    (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_genericEtale_of_minimalBadPuncturedPurity

L161 ↗

EtaleFundamentalGroups.SpecialLocalPurity.finiteNormalDomainAlgebra_etale_of_genericEtale_of_minimalBadPuncturedPurity

Documentation

The finite-presentation consequence: under the preceding hypotheses the original finite normal-domain algebra is etale.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u

Lean source · statement

theorem
    finiteNormalDomainAlgebra_etale_of_genericEtale_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))
    (hgeneric : Algebra.IsEtaleAt R (⊥ : Ideal S))
    (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

theorem

finiteNormalDomainAlgebra_formallyEtale_of_genericAndHeightOneEtale_of_minimalBadPurity

L189 ↗

EtaleFundamentalGroups.SpecialLocalPurity.finiteNormalDomainAlgebra_formallyEtale_of_genericAndHeightOneEtale_of_minimalBadPurity

Documentation

In the geometric codimension-two form, punctured purity is needed only at minimal bad points which are not of height one. Generic etaleness supplies positive local dimension, while the height-one etaleness hypothesis shows that every hypothetical minimal bad point satisfies this restriction.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u

Lean source · statement

theorem
    finiteNormalDomainAlgebra_formallyEtale_of_genericAndHeightOneEtale_of_minimalBadPurity
    {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))
    (hgeneric : Algebra.IsEtaleAt R (⊥ : Ideal S))
    (hetale :
      ∀ (q : Ideal R) [q.IsPrime], q.height = 1 →
        ∀ (Q : Ideal S) [Q.IsPrime] [Q.LiesOver q],
          Algebra.IsEtaleAt R Q)
    (hpurity : ∀ (p : PrimeSpectrum R),
      (hp : Minimal
        (· ∈ Module.support R Ω[S⁄R] ∪
          Module.support R (Algebra.H1Cotangent R S)) p) →
      p.asIdeal.height ≠ 1 →
      AlgebraicGeometry.FiniteEtale.HasPuncturedPurity
        (Localization.AtPrime p.asIdeal)) :
    Algebra.FormallyEtale R S

theorem

finiteNormalDomainAlgebra_etale_of_genericAndHeightOneEtale_of_minimalBadPurity

L222 ↗

EtaleFundamentalGroups.SpecialLocalPurity.finiteNormalDomainAlgebra_etale_of_genericAndHeightOneEtale_of_minimalBadPurity

Documentation

Finite presentation upgrades the preceding codimension-two purity criterion to global etaleness.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u

Lean source · statement

theorem
    finiteNormalDomainAlgebra_etale_of_genericAndHeightOneEtale_of_minimalBadPurity
    {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))
    (hgeneric : Algebra.IsEtaleAt R (⊥ : Ideal S))
    (hetale :
      ∀ (q : Ideal R) [q.IsPrime], q.height = 1 →
        ∀ (Q : Ideal S) [Q.IsPrime] [Q.LiesOver q],
          Algebra.IsEtaleAt R Q)
    (hpurity : ∀ (p : PrimeSpectrum R),
      (hp : Minimal
        (· ∈ Module.support R Ω[S⁄R] ∪
          Module.support R (Algebra.H1Cotangent R S)) p) →
      p.asIdeal.height ≠ 1 →
      AlgebraicGeometry.FiniteEtale.HasPuncturedPurity
        (Localization.AtPrime p.asIdeal)) :
    Algebra.Etale R S

Module documentation

Generic etaleness supplies positive-dimensional minimal bad localizations

Declarations