Module

IntegrallyClosed.lean

Nyll.EtaleFundamentalGroups.LocalGeometry.RegularPair.IntegrallyClosed

4 declarations indexed from sourceView source ↗

Module documentation

Integral closedness from a regular parameter pair

For a Noetherian local domain whose maximal ideal is generated by a regular pair, this file proves integral closedness directly. The proof avoids a factoriality detour.

For an integral fraction z, consider the conductor of the finite algebra A[z] into A. A common denominator for finitely many module generators makes this conductor nonzero. The regular pair remains regular on the conductor, so dimension-two freeness makes it a free ideal. Its rank is at most one, hence it is principal. Stability under z and cancellation of a nonzero generator then show that z already lies in A.

Imports7

Mathlib.Algebra.Module.LocalizedModule.Int
Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Mathlib.RingTheory.Ideal.Colon
Mathlib.RingTheory.Ideal.IsPrincipal
Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Mathlib.RingTheory.Regular.RegularSequence
Nyll.EtaleFundamentalGroups.Purity.SpecialLocal.DimensionTwoFlatness

Imported by6

def

conductorIdeal

L44 ↗

EtaleFundamentalGroups.SpecialLocalPurity.conductorIdeal

Documentation

The conductor of a subalgebra of a fraction field into the base ring.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
open scoped Pointwise
open IsLocalRing
open Module
open nonZeroDivisors
open RingTheory.Sequence
universe u v

Lean source · statement

def conductorIdeal
    (A : Type u) (K : Type v) [CommRing A] [CommRing K] [Algebra A K]
    (S : Subalgebra A K) : Ideal A

theorem

conductorIdeal_ne_bot_of_finite

L51 ↗

EtaleFundamentalGroups.SpecialLocalPurity.conductorIdeal_ne_bot_of_finite

Documentation

A finite subalgebra of a fraction field has nonzero conductor into the base domain: clear the denominators of a finite set of module generators.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
open scoped Pointwise
open IsLocalRing
open Module
open nonZeroDivisors
open RingTheory.Sequence
universe u v

Lean source · statement

theorem conductorIdeal_ne_bot_of_finite
    (A : Type u) (K : Type v) [CommRing A] [IsDomain A]
    [Field K] [Algebra A K] [IsFractionRing A K]
    (S : Subalgebra A K) [Module.Finite A S] :
    conductorIdeal A K S ≠ ⊥

theorem

conductorIdeal_isWeaklyRegular_pair

L87 ↗

EtaleFundamentalGroups.SpecialLocalPurity.conductorIdeal_isWeaklyRegular_pair

Documentation

A regular pair on the base remains weakly regular on every conductor ideal inside a fraction field.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
open scoped Pointwise
open IsLocalRing
open Module
open nonZeroDivisors
open RingTheory.Sequence
universe u v

Lean source · statement

theorem conductorIdeal_isWeaklyRegular_pair
    (A : Type u) (K : Type v) [CommRing A] [IsDomain A]
    [Field K] [Algebra A K] [IsFractionRing A K]
    (S : Subalgebra A K) {x y : A} (hregular : IsRegular A [x, y]) :
    IsWeaklyRegular (conductorIdeal A K S) [x, y]

theorem

isIntegrallyClosed_of_isRegular_pair_of_span_eq_maximalIdeal

L184 ↗

EtaleFundamentalGroups.SpecialLocalPurity.isIntegrallyClosed_of_isRegular_pair_of_span_eq_maximalIdeal

Documentation

A Noetherian local domain whose maximal ideal is generated by a regular pair is integrally closed.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
open scoped Pointwise
open IsLocalRing
open Module
open nonZeroDivisors
open RingTheory.Sequence
universe u v

Lean source · statement

theorem isIntegrallyClosed_of_isRegular_pair_of_span_eq_maximalIdeal
    (A : Type u) [CommRing A] [IsDomain A] [IsLocalRing A]
    [IsNoetherianRing A] (x y : A) (hregular : IsRegular A [x, y])
    (hspan : Ideal.ofList [x, y] = maximalIdeal A) :
    IsIntegrallyClosed A

Module documentation

Integral closedness from a regular parameter pair

Declarations

conductorIdeal

conductorIdeal_ne_bot_of_finite

conductorIdeal_isWeaklyRegular_pair

isIntegrallyClosed_of_isRegular_pair_of_span_eq_maximalIdeal