Module

MaximalAdicCompletion.lean

Nyll.EtaleFundamentalGroups.Purity.Local.MaximalAdicCompletion

8 declarations indexed from sourceView source ↗

Module documentation

Regular local geometry of the maximal-adic completion

The maximal-adic completion of a Noetherian local ring is flat and local, hence faithfully flat. Once Noetherianity of the completed ring has been produced, going down and the explicit description of its maximal ideal show that completion preserves Krull dimension. The cotangent-space comparison then shows that regularity is preserved as well.

The Noetherianity hypothesis on the completed ring is deliberately visible: Mathlib currently supplies flatness of a Noetherian adic completion, but not Noetherianity of the completed ring itself. Separate source-producing results can discharge that hypothesis without changing these statements.

Imports6

Mathlib.RingTheory.AdicCompletion.AsTensorProduct
Mathlib.RingTheory.AdicCompletion.LocalRing
Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Mathlib.RingTheory.RegularLocalRing.Defs
Nyll.EtaleFundamentalGroups.Kummer.Completions.MaximalAdic.MvPowerSeriesNoetherian
Nyll.SchemeTheory.RingTheory.Descent.FaithfullyFlatModuleEqualizer

Imported by6

theorem

maximalAdicCompletion_faithfullyFlat

L40 ↗

EtaleFundamentalGroups.maximalAdicCompletion_faithfullyFlat

Documentation

The maximal-adic completion of a Noetherian local ring is faithfully flat over the original ring.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v

Lean source · statement

theorem maximalAdicCompletion_faithfullyFlat
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] :
    Module.FaithfullyFlat R
      (AdicCompletion (maximalIdeal R) R)

def

maximalAdicCompletionModuleEqualizerEquiv

L50 ↗

EtaleFundamentalGroups.maximalAdicCompletionModuleEqualizerEquiv

Documentation

Every module over a Noetherian local ring is recovered as the equalizer of its two pullbacks from the maximal-adic completion to the double completion. This is the faithfully-flat equalizer input for formal gluing; it does not assume that the source ring is complete.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v

Lean source · statement

def maximalAdicCompletionModuleEqualizerEquiv
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (M : Type v) [AddCommGroup M] [Module R M] :
    M ≃ₗ[R] LinearMap.eqLocus
      (tensorProductDescentLeft
        (R := R) (S := AdicCompletion (maximalIdeal R) R) (M := M))
      (tensorProductDescentRight
        (R := R) (S := AdicCompletion (maximalIdeal R) R) (M := M))

theorem

maximalAdicCompletionModuleEqualizerEquiv_apply

L64 ↗

EtaleFundamentalGroups.maximalAdicCompletionModuleEqualizerEquiv_apply

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v

Lean source · statement

theorem maximalAdicCompletionModuleEqualizerEquiv_apply
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (M : Type v) [AddCommGroup M] [Module R M] (m : M) :
    (maximalAdicCompletionModuleEqualizerEquiv R M m :
        (AdicCompletion (maximalIdeal R) R) ⊗[R] M) =
      1 ⊗ₜ[R] m

theorem

maximalAdicCompletionModuleEqualizer_finite

L74 ↗

EtaleFundamentalGroups.maximalAdicCompletionModuleEqualizer_finite

Documentation

If the original module is finite, then its explicit maximal-adic completion equalizer is finite as an R-module.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v

Lean source · statement

theorem maximalAdicCompletionModuleEqualizer_finite
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] :
    Module.Finite R (LinearMap.eqLocus
      (tensorProductDescentLeft
        (R := R) (S := AdicCompletion (maximalIdeal R) R) (M := M))
      (tensorProductDescentRight
        (R := R) (S := AdicCompletion (maximalIdeal R) R) (M := M)))

theorem

maximalAdicCompletion_ringKrullDim_eq_of_isNoetherianRing

L88 ↗

EtaleFundamentalGroups.maximalAdicCompletion_ringKrullDim_eq_of_isNoetherianRing

Documentation

A Noetherian maximal-adic completion has the same Krull dimension as its source. The proof uses faithful flatness only through going down; the closed fibre has height zero because the source maximal ideal maps onto the target maximal ideal.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v

Lean source · statement

theorem maximalAdicCompletion_ringKrullDim_eq_of_isNoetherianRing
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    [IsNoetherianRing (AdicCompletion (maximalIdeal R) R)] :
    ringKrullDim (AdicCompletion (maximalIdeal R) R) =
      ringKrullDim R

theorem

maximalAdicCompletion_isRegularLocalRing_of_isNoetherianRing

L120 ↗

EtaleFundamentalGroups.maximalAdicCompletion_isRegularLocalRing_of_isNoetherianRing

Documentation

If the maximal-adic completion has been shown Noetherian, regularity of a Noetherian local source ascends to its completion.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v

Lean source · statement

theorem maximalAdicCompletion_isRegularLocalRing_of_isNoetherianRing
    (R : Type u) [CommRing R] [IsRegularLocalRing R]
    [IsNoetherianRing (AdicCompletion (maximalIdeal R) R)] :
    IsRegularLocalRing (AdicCompletion (maximalIdeal R) R)

theorem

maximalAdicCompletion_ringKrullDim_eq

L138 ↗

EtaleFundamentalGroups.maximalAdicCompletion_ringKrullDim_eq

Documentation

Maximal-adic completion preserves the Krull dimension of every Noetherian local ring.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v

Lean source · statement

theorem maximalAdicCompletion_ringKrullDim_eq
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] :
    ringKrullDim (AdicCompletion (maximalIdeal R) R) =
      ringKrullDim R

theorem

maximalAdicCompletion_isRegularLocalRing

L145 ↗

EtaleFundamentalGroups.maximalAdicCompletion_isRegularLocalRing

Documentation

The maximal-adic completion of a regular local ring is regular local.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v

Lean source · statement

theorem maximalAdicCompletion_isRegularLocalRing
    (R : Type u) [CommRing R] [IsRegularLocalRing R] :
    IsRegularLocalRing (AdicCompletion (maximalIdeal R) R)

Module documentation

Regular local geometry of the maximal-adic completion

Declarations