NYLL
Module

AssociatedPrime.lean

Nyll.EtaleFundamentalGroups.Purity.SpecialLocal.AssociatedPrime
6 declarations indexed from sourceView source ↗

Module documentation

Minimal cotangent support and associated primes

For a finite module over a Noetherian ring, a minimal point of its support is an associated prime. Applying this to the two finite cotangent modules turns a minimal point of the non-etale cotangent support into an associated prime of one of those modules. The codimension-one hypothesis from SpecialLocalPuritySupport simultaneously shows that this prime does not have height one.

This is the exact interface at which a depth or branch-locus theorem must enter; no height bound or purity conclusion is assumed here.

Imports2
Imported by2

Declarations

theorem

mem_minimalPrimes_annihilator_of_minimal_mem_support

L32 ↗
EtaleFundamentalGroups.SpecialLocalPurity.mem_minimalPrimes_annihilator_of_minimal_mem_support
Documentation

A minimal point of the support of a finite module is a minimal prime over its annihilator.

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 mem_minimalPrimes_annihilator_of_minimal_mem_support
    {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M]
    [Module.Finite R M] (P : PrimeSpectrum R)
    (hP : Minimal (· ∈ Module.support R M) P) :
    P.asIdeal ∈ (Module.annihilator R M).minimalPrimes
theorem

mem_associatedPrimes_of_minimal_mem_support

L46 ↗
EtaleFundamentalGroups.SpecialLocalPurity.mem_associatedPrimes_of_minimal_mem_support
Documentation

A minimal point of the support of a finite module over a Noetherian ring is an associated prime.

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 mem_associatedPrimes_of_minimal_mem_support
    {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M]
    [IsNoetherianRing R] [Module.Finite R M] (P : PrimeSpectrum R)
    (hP : Minimal (· ∈ Module.support R M) P) :
    P.asIdeal ∈ associatedPrimes R M
theorem

exists_minimal_nonEtaleCotangentSupport_of_not_formallyEtale

L58 ↗
EtaleFundamentalGroups.SpecialLocalPurity.exists_minimal_nonEtaleCotangentSupport_of_not_formallyEtale
Documentation

If a finite algebra is not formally etale, the union of its two cotangent supports has a minimal point. The point is obtained from a minimal prime over the intersection of the two annihilator ideals, so no Noetherian topological choice is hidden in the statement.

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_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 S,
      Minimal
        (· ∈ Module.support S Ω[S⁄R] ∪
          Module.support S (Algebra.H1Cotangent R S)) P
theorem

isEtaleAt_of_lt_minimal_nonEtaleCotangentSupport

L127 ↗
EtaleFundamentalGroups.SpecialLocalPurity.isEtaleAt_of_lt_minimal_nonEtaleCotangentSupport
Documentation

Every prime strictly below a minimal point of the non-etale cotangent support lies in the etale locus.

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_lt_minimal_nonEtaleCotangentSupport
    {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    [Algebra R S]
    (P : PrimeSpectrum S)
    (hP : Minimal
      (· ∈ Module.support S Ω[S⁄R] ∪
        Module.support S (Algebra.H1Cotangent R S)) P)
    (Q : PrimeSpectrum S) (hQP : Q < P) :
    Algebra.IsEtaleAt R Q.asIdeal
theorem

minimal_nonEtaleCotangentSupport_associated_and_height_ne_one

L148 ↗
EtaleFundamentalGroups.SpecialLocalPurity.minimal_nonEtaleCotangentSupport_associated_and_height_ne_one
Documentation

Under height-one etaleness, a minimal point of the non-etale cotangent support is an associated prime of one cotangent module and is not height one. This packages the two production inputs without assuming the missing purity height bound.

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 minimal_nonEtaleCotangentSupport_associated_and_height_ne_one
    {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    [IsNoetherianRing R] [IsDomain R] [IsIntegrallyClosed R] [IsDomain S]
    [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree 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 S)
    (hP : Minimal
      (· ∈ Module.support S Ω[S⁄R] ∪
        Module.support S (Algebra.H1Cotangent R S)) P) :
    P.asIdeal ∈ associatedPrimes S Ω[S⁄R] ∪
        associatedPrimes S (Algebra.H1Cotangent R S) ∧
      P.asIdeal.height ≠ 1
theorem

exists_nonEtaleCotangentSupport_associated_and_height_ne_one_of_isEtaleAt_heightOne

L183 ↗
EtaleFundamentalGroups.SpecialLocalPurity.exists_nonEtaleCotangentSupport_associated_and_height_ne_one_of_isEtaleAt_heightOne
Documentation

A non-formally-etale finite torsion-free domain extension which is etale over every height-one prime has a higher-codimension associated cotangent prime. This is the contradiction witness used by the minimal-bad-point branch-locus argument.

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_nonEtaleCotangentSupport_associated_and_height_ne_one_of_isEtaleAt_heightOne
    {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    [IsNoetherianRing R] [IsDomain R] [IsIntegrallyClosed R] [IsDomain S]
    [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree 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 S,
      P.asIdeal ∈ associatedPrimes S Ω[S⁄R] ∪
          associatedPrimes S (Algebra.H1Cotangent R S) ∧
        P.asIdeal.height ≠ 1

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