NYLL
Module

BaseMinimalPrime.lean

Nyll.EtaleFundamentalGroups.Purity.SpecialLocal.BaseMinimalPrime
5 declarations indexed from sourceView source ↗

Module documentation

Minimal non-etale points on the base

For a finite algebra, the image of each target cotangent support is its support after restriction of scalars to the base. Hence a non-etale algebra has a minimal bad point on the base which is the contraction of an actual bad point upstairs. Every target prime contracting strictly below that base point is etale. This is the local input needed before applying punctured purity at a minimal branch point.

Imports1
Imported by4

Declarations

theorem

exists_minimal_base_nonEtaleCotangentSupport_of_not_formallyEtale

L28 ↗
EtaleFundamentalGroups.SpecialLocalPurity.exists_minimal_base_nonEtaleCotangentSupport_of_not_formallyEtale
Documentation

A non-formally-etale finite algebra has a minimal bad point on the base, and that point is the contraction of an actual bad point upstairs.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u v
Lean source · statement
theorem exists_minimal_base_nonEtaleCotangentSupport_of_not_formallyEtale
    {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    [IsNoetherianRing R] [Algebra R S] [Module.Finite R S]
    (hne : ¬ Algebra.FormallyEtale R S) :
    ∃ p : PrimeSpectrum R,
      Minimal
        (· ∈ Module.support R Ω[S⁄R] ∪
          Module.support R (Algebra.H1Cotangent R S)) p ∧
      ∃ P : PrimeSpectrum S,
        PrimeSpectrum.comap (algebraMap R S) P = p ∧
        P ∈ Module.support S Ω[S⁄R] ∪
          Module.support S (Algebra.H1Cotangent R S)
theorem

isEtaleAt_of_comap_lt_minimal_base_nonEtaleCotangentSupport

L100 ↗
EtaleFundamentalGroups.SpecialLocalPurity.isEtaleAt_of_comap_lt_minimal_base_nonEtaleCotangentSupport
Documentation

Above a base prime strictly below a minimal bad base point, every target prime is etale.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u v
Lean source · statement
theorem isEtaleAt_of_comap_lt_minimal_base_nonEtaleCotangentSupport
    {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    [Algebra R S]
    (p : PrimeSpectrum R)
    (hp : Minimal
      (· ∈ Module.support R Ω[S⁄R] ∪
        Module.support R (Algebra.H1Cotangent R S)) p)
    (P : PrimeSpectrum S)
    (hPp : PrimeSpectrum.comap (algebraMap R S) P < p) :
    Algebra.IsEtaleAt R P.asIdeal
theorem

base_height_ne_one_of_nonEtaleCotangentSupport_of_isEtaleAt_heightOne

L131 ↗
EtaleFundamentalGroups.SpecialLocalPurity.base_height_ne_one_of_nonEtaleCotangentSupport_of_isEtaleAt_heightOne
Documentation

The contraction of an actual non-etale cotangent-support point cannot have height one when every target prime above a height-one base prime is etale.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u v
Lean source · statement
theorem
    base_height_ne_one_of_nonEtaleCotangentSupport_of_isEtaleAt_heightOne
    {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    [Algebra R S]
    (hetale :
      ∀ (p : Ideal R) [p.IsPrime], p.height = 1 →
        ∀ (P : Ideal S) [P.IsPrime] [P.LiesOver p],
          Algebra.IsEtaleAt R P)
    (p : PrimeSpectrum R) (P : PrimeSpectrum S)
    (hPp : PrimeSpectrum.comap (algebraMap R S) P = p)
    (hP : P ∈ Module.support S Ω[S⁄R] ∪
      Module.support S (Algebra.H1Cotangent R S)) :
    p.asIdeal.height ≠ 1
theorem

exists_minimal_base_nonEtaleCotangentSupport_height_ne_one

L156 ↗
EtaleFundamentalGroups.SpecialLocalPurity.exists_minimal_base_nonEtaleCotangentSupport_height_ne_one
Documentation

If a finite algebra is non-etale but etale above every height-one base prime, its base cotangent support has a minimal point away from height one.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u v
Lean source · statement
theorem exists_minimal_base_nonEtaleCotangentSupport_height_ne_one
    {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    [IsNoetherianRing R] [Algebra R S] [Module.Finite R S]
    (hetale :
      ∀ (p : Ideal R) [p.IsPrime], p.height = 1 →
        ∀ (P : Ideal S) [P.IsPrime] [P.LiesOver p],
          Algebra.IsEtaleAt R P)
    (hne : ¬ Algebra.FormallyEtale R S) :
    ∃ p : PrimeSpectrum R,
      Minimal
        (· ∈ Module.support R Ω[S⁄R] ∪
          Module.support R (Algebra.H1Cotangent R S)) p ∧
      p.asIdeal.height ≠ 1
theorem

base_height_ne_zero_of_nonEtaleCotangentSupport_of_isEtaleAt_bot

L177 ↗
EtaleFundamentalGroups.SpecialLocalPurity.base_height_ne_zero_of_nonEtaleCotangentSupport_of_isEtaleAt_bot
Documentation

The contraction of an actual non-etale cotangent-support point cannot have height zero when the integral domain extension is generically etale.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u v
Lean source · statement
theorem
    base_height_ne_zero_of_nonEtaleCotangentSupport_of_isEtaleAt_bot
    {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    [IsDomain R] [IsDomain S] [Algebra R S] [Algebra.IsIntegral R S]
    (hgeneric : Algebra.IsEtaleAt R (⊥ : Ideal S))
    (p : PrimeSpectrum R) (P : PrimeSpectrum S)
    (hPp : PrimeSpectrum.comap (algebraMap R S) P = p)
    (hP : P ∈ Module.support S Ω[S⁄R] ∪
      Module.support S (Algebra.H1Cotangent R S)) :
    p.asIdeal.height ≠ 0

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.