Module

DimensionTwoFlatness.lean

Nyll.EtaleFundamentalGroups.Purity.SpecialLocal.DimensionTwoFlatness

3 declarations indexed from sourceView source ↗

Module documentation

The two-parameter freeness input to dimension-two purity

A finite module over a Noetherian local ring is free when a pair generating the maximal ideal is a regular sequence on the module. Freeness is lifted twice from the residue-field quotient using Module.free_quotSMulTop_iff_free.

For a finite normal algebra over a two-dimensional regular local ring, the remaining algebraic input is therefore exactly that a regular parameter pair is regular on the algebra (the S₂ consequence of normality).

Imports4

Mathlib.LinearAlgebra.Basis.VectorSpace
Mathlib.RingTheory.LocalRing.Quotient
Mathlib.RingTheory.Regular.Free
Mathlib.RingTheory.Regular.RegularSequence

Imported by3

theorem

free_of_free_quotSMulTop

L34 ↗

EtaleFundamentalGroups.SpecialLocalPurity.free_of_free_quotSMulTop

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
open IsLocalRing
open RingTheory.Sequence
universe u v

Lean source · statement

theorem free_of_free_quotSMulTop
    {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M]
    [Module.FinitePresentation R M] {x : R}
    (hx : x ∈ (⊥ : Ideal R).jacobson) (hregular : IsSMulRegular M x)
    (hfree : Module.Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) :
    Module.Free R M

theorem

module_free_of_isSMulRegular_of_span_eq_maximalIdeal

L44 ↗

EtaleFundamentalGroups.SpecialLocalPurity.module_free_of_isSMulRegular_of_span_eq_maximalIdeal

Documentation

A finite module is free if an element generating the maximal ideal acts regularly. This is the one-step lifting used for the second parameter below.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
open IsLocalRing
open RingTheory.Sequence
universe u v

Lean source · statement

theorem module_free_of_isSMulRegular_of_span_eq_maximalIdeal
    {R : Type u} {M : Type v} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    [AddCommGroup M] [Module R M] [Module.Finite R M]
    (x : R) (hregular : IsSMulRegular M x)
    (hspan : Ideal.span {x} = maximalIdeal R) :
    Module.Free R M

theorem

module_free_of_isRegular_pair_of_span_eq_maximalIdeal

L62 ↗

EtaleFundamentalGroups.SpecialLocalPurity.module_free_of_isRegular_pair_of_span_eq_maximalIdeal

Documentation

A finite module is free if two elements generate the maximal ideal and form a regular sequence on the module.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
open IsLocalRing
open RingTheory.Sequence
universe u v

Lean source · statement

theorem module_free_of_isRegular_pair_of_span_eq_maximalIdeal
    {R : Type u} {M : Type v} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    [AddCommGroup M] [Module R M] [Module.Finite R M]
    (x y : R) (hregular : IsRegular M [x, y])
    (hspan : Ideal.ofList [x, y] = maximalIdeal R) :
    Module.Free R M

Module documentation

The two-parameter freeness input to dimension-two purity

Declarations

free_of_free_quotSMulTop

module_free_of_isSMulRegular_of_span_eq_maximalIdeal

module_free_of_isRegular_pair_of_span_eq_maximalIdeal