NYLL
Module

Core.lean

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

Module documentation

Dimension-two purity for finite free algebras

For a finite free algebra, formal unramifiedness is detected by the trace discriminant. Over a Noetherian domain, a nonzero element whose image is a unit at every height-one localization is already a unit: otherwise a minimal prime over its principal ideal gives a height-one point where its image lies in the maximal ideal.

A regular pair generating the maximal ideal supplies a height-one prime, so the discriminant cannot vanish. Consequently, if every height-one localization of a finite free algebra is etale, its global discriminant is a unit and the algebra is etale over the base.

Imports5
Imported by2

Declarations

theorem

exists_height_one_prime_containing_of_nonzero_nonunit

L39 ↗
EtaleFundamentalGroups.SpecialLocalPurity.exists_height_one_prime_containing_of_nonzero_nonunit
Documentation

A nonzero nonunit in a Noetherian domain is contained in a height-one prime. The prime is chosen minimal over the element's principal ideal.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
open IsLocalRing Module
open RingTheory.Sequence
universe u v
Lean source · statement
theorem exists_height_one_prime_containing_of_nonzero_nonunit
    {A : Type u} [CommRing A] [IsDomain A] [IsNoetherianRing A]
    {d : A} (hd : d ≠ 0) (hdu : ¬ IsUnit d) :
    ∃ p : Ideal A, p.IsPrime ∧ p.height = 1 ∧ d ∈ p
theorem

isUnit_of_isUnit_localizationAtPrime_height_one

L62 ↗
EtaleFundamentalGroups.SpecialLocalPurity.isUnit_of_isUnit_localizationAtPrime_height_one
Documentation

In a Noetherian domain, a nonzero element which becomes a unit at every height-one localization is a unit.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
open IsLocalRing Module
open RingTheory.Sequence
universe u v
Lean source · statement
theorem isUnit_of_isUnit_localizationAtPrime_height_one
    {A : Type u} [CommRing A] [IsDomain A] [IsNoetherianRing A]
    {d : A} (hd : d ≠ 0)
    (hlocal : ∀ (p : Ideal A) [p.IsPrime], p.height = 1 →
      IsUnit (algebraMap A (Localization.AtPrime p) d)) :
    IsUnit d
theorem

exists_height_one_prime_of_regular_pair

L83 ↗
EtaleFundamentalGroups.SpecialLocalPurity.exists_height_one_prime_of_regular_pair
Documentation

A regular pair generating the maximal ideal of a Noetherian local domain produces a height-one prime.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
open IsLocalRing Module
open RingTheory.Sequence
universe u v
Lean source · statement
theorem exists_height_one_prime_of_regular_pair
    {A : Type u} [CommRing A] [IsDomain A] [IsNoetherianRing A]
    [IsLocalRing A]
    {x y : A} (hregular : IsRegular A [x, y])
    (hspan : Ideal.ofList [x, y] = maximalIdeal A) :
    ∃ p : Ideal A, p.IsPrime ∧ p.height = 1
theorem

etale_of_exists_height_one_prime_of_etale_localizationAtPrime

L105 ↗
EtaleFundamentalGroups.SpecialLocalPurity.etale_of_exists_height_one_prime_of_etale_localizationAtPrime
Documentation

A finite free algebra over a Noetherian domain is etale when a height-one prime exists and every height-one localization is etale.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
open IsLocalRing Module
open RingTheory.Sequence
universe u v
Lean source · statement
theorem etale_of_exists_height_one_prime_of_etale_localizationAtPrime
    {A : Type u} {S : Type v}
    [CommRing A] [IsDomain A] [IsNoetherianRing A]
    [CommRing S] [Algebra A S] [Module.Free A S] [Module.Finite A S]
    (hexists : ∃ p : Ideal A, p.IsPrime ∧ p.height = 1)
    (hlocal : ∀ (p : Ideal A) [p.IsPrime], p.height = 1 →
      Algebra.Etale (Localization.AtPrime p)
        (Localization (Algebra.algebraMapSubmonoid S p.primeCompl))) :
    Algebra.Etale A S
theorem

etale_of_regular_pair_of_etale_localizationAtPrime

L151 ↗
EtaleFundamentalGroups.SpecialLocalPurity.etale_of_regular_pair_of_etale_localizationAtPrime
Documentation

Dimension-two special local purity in regular-parameter form: if a regular pair generates the maximal ideal, a finite free algebra which is etale after localization at every height-one prime is globally etale.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
open IsLocalRing Module
open RingTheory.Sequence
universe u v
Lean source · statement
theorem etale_of_regular_pair_of_etale_localizationAtPrime
    {A : Type u} {S : Type v}
    [CommRing A] [IsDomain A] [IsNoetherianRing A]
    [IsLocalRing A]
    [CommRing S] [Algebra A S] [Module.Free A S] [Module.Finite A S]
    {x y : A} (hregular : IsRegular A [x, y])
    (hspan : Ideal.ofList [x, y] = maximalIdeal A)
    (hlocal : ∀ (p : Ideal A) [p.IsPrime], p.height = 1 →
      Algebra.Etale (Localization.AtPrime p)
        (Localization (Algebra.algebraMapSubmonoid S p.primeCompl))) :
    Algebra.Etale A S

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