Module

GenericPoint.lean

Nyll.EtaleFundamentalGroups.Purity.SpecialLocal.GenericPoint

3 declarations indexed from sourceView source ↗

Module documentation

Generic etaleness of a finite separable normalization

The localization of an integral closure at its zero prime is its fraction field. Identifying that fraction field with the supplied finite separable extension transports formal etaleness back to the literal localization used by Algebra.IsEtaleAt.

Imports3

Nyll.EtaleFundamentalGroups.Normalization.IntegralClosure.Localization.FractionFieldComparison
Nyll.EtaleFundamentalGroups.Purity.SpecialLocal.BaseMinimalPrime
Mathlib.RingTheory.Etale.Field

Imported by2

theorem

integralClosure_isEtaleAt_bot_of_finite_separable

L28 ↗

EtaleFundamentalGroups.SpecialLocalPurity.integralClosure_isEtaleAt_bot_of_finite_separable

Documentation

The normalization in a finite separable extension is etale at its generic point.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u v w

Lean source · statement

theorem integralClosure_isEtaleAt_bot_of_finite_separable
    {R : Type u} {K : Type v} {L : Type w}
    [CommRing R] [IsDomain R]
    [Field K] [Algebra R K] [IsFractionRing R K]
    [Field L] [Algebra R L] [Algebra K L] [IsScalarTower R K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L] :
    Algebra.IsEtaleAt R (⊥ : Ideal (integralClosure R L))

theorem

exists_minimal_integralClosure_base_nonEtaleCotangentSupport_codim_ge_two

L58 ↗

EtaleFundamentalGroups.SpecialLocalPurity.exists_minimal_integralClosure_base_nonEtaleCotangentSupport_codim_ge_two

Documentation

If a finite separable normalization is not formally etale but is etale above every height-one base prime, its base cotangent support has a minimal point of neither height zero nor height one.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u v w

Lean source · statement

theorem
    exists_minimal_integralClosure_base_nonEtaleCotangentSupport_codim_ge_two
    {R : Type u} {K : Type v} {L : Type w}
    [CommRing R] [IsDomain R] [IsNoetherianRing R]
    [Field K] [Algebra R K] [IsFractionRing R K]
    [Field L] [Algebra R L] [Algebra K L] [IsScalarTower R K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [Module.Finite R (integralClosure R L)]
    (hetale :
      ∀ (p : Ideal R) [p.IsPrime], p.height = 1 →
        ∀ (P : Ideal (integralClosure R L)) [P.IsPrime] [P.LiesOver p],
          Algebra.IsEtaleAt R P)
    (hne : ¬ Algebra.FormallyEtale R (integralClosure R L)) :
    ∃ p : PrimeSpectrum R,
      Minimal
        (· ∈ Module.support R Ω[(integralClosure R L)⁄R] ∪
          Module.support R
            (Algebra.H1Cotangent R (integralClosure R L))) p ∧
      p.asIdeal.height ≠ 0 ∧ p.asIdeal.height ≠ 1

theorem

exists_minimal_integralClosure_base_nonEtaleCotangentSupport_height_two_le

L90 ↗

EtaleFundamentalGroups.SpecialLocalPurity.exists_minimal_integralClosure_base_nonEtaleCotangentSupport_height_two_le

Documentation

Numerical form of the preceding minimal-branch-point theorem: the bad base point has height at least two.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u v w

Lean source · statement

theorem
    exists_minimal_integralClosure_base_nonEtaleCotangentSupport_height_two_le
    {R : Type u} {K : Type v} {L : Type w}
    [CommRing R] [IsDomain R] [IsNoetherianRing R]
    [Field K] [Algebra R K] [IsFractionRing R K]
    [Field L] [Algebra R L] [Algebra K L] [IsScalarTower R K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [Module.Finite R (integralClosure R L)]
    (hetale :
      ∀ (p : Ideal R) [p.IsPrime], p.height = 1 →
        ∀ (P : Ideal (integralClosure R L)) [P.IsPrime] [P.LiesOver p],
          Algebra.IsEtaleAt R P)
    (hne : ¬ Algebra.FormallyEtale R (integralClosure R L)) :
    ∃ p : PrimeSpectrum R,
      Minimal
        (· ∈ Module.support R Ω[(integralClosure R L)⁄R] ∪
          Module.support R
            (Algebra.H1Cotangent R (integralClosure R L))) p ∧
      (2 : ℕ∞) ≤ p.asIdeal.height

Module documentation

Generic etaleness of a finite separable normalization

Declarations

integralClosure_isEtaleAt_bot_of_finite_separable

exists_minimal_integralClosure_base_nonEtaleCotangentSupport_codim_ge_two

exists_minimal_integralClosure_base_nonEtaleCotangentSupport_height_two_le