Module

MvPowerSeriesNoetherian.lean

Nyll.EtaleFundamentalGroups.Kummer.Completions.MaximalAdic.MvPowerSeriesNoetherian

15 declarations indexed from sourceView source ↗

Module documentation

Noetherian finite-variable power-series rings

Splitting a finite set of variables into one variable and the remaining variables identifies the corresponding multivariate power-series ring with an iterated univariate power-series ring. This gives the finite-variable Hilbert basis theorem for formal power series and, as an application, the Noetherianity of maximal-adic completions of Noetherian local rings.

Imports3

Mathlib.RingTheory.MvPowerSeries.Rename
Mathlib.RingTheory.PowerSeries.Ideal
Nyll.EtaleFundamentalGroups.Kummer.Completions.MaximalAdic.FiniteGeneratorEvaluation

Imported by2

def

splitIndex

L36 ↗

EtaleFundamentalGroups.Kummer.MvPowerSeriesFinite.splitIndex

Documentation

Split an exponent on Unit ⊕ σ into the exponent of the distinguished variable and the exponent vector on the remaining variables.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u v
open Finset
open IsLocalRing
namespace MvPowerSeriesFinite
variable {R : Type u} {σ : Type v}

Lean source · statement

def splitIndex :
    (Unit ⊕ σ →₀ ℕ) ≃ ℕ × (σ →₀ ℕ)

lemma

splitIndex_symm_apply

L42 ↗

EtaleFundamentalGroups.Kummer.MvPowerSeriesFinite.splitIndex_symm_apply

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u v
open Finset
open IsLocalRing
namespace MvPowerSeriesFinite
variable {R : Type u} {σ : Type v}

Lean source · statement

lemma splitIndex_symm_apply (n : ℕ) (d : σ →₀ ℕ) :
    (splitIndex (σ := σ)).symm (n, d) =
      (Finsupp.single () n).sumElim d

lemma

splitIndex_apply_sumElim

L47 ↗

EtaleFundamentalGroups.Kummer.MvPowerSeriesFinite.splitIndex_apply_sumElim

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u v
open Finset
open IsLocalRing
namespace MvPowerSeriesFinite
variable {R : Type u} {σ : Type v}

Lean source · statement

lemma splitIndex_apply_sumElim (n : ℕ) (d : σ →₀ ℕ) :
    splitIndex ((Finsupp.single () n).sumElim d) = (n, d)

def

curryFun

L54 ↗

EtaleFundamentalGroups.Kummer.MvPowerSeriesFinite.curryFun

Documentation

Curry the coefficient function of a power series in Unit ⊕ σ into a univariate power series whose coefficients are power series in σ.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u v
open Finset
open IsLocalRing
namespace MvPowerSeriesFinite
variable {R : Type u} {σ : Type v}

Lean source · statement

def curryFun [Semiring R] :
    MvPowerSeries (Unit ⊕ σ) R → PowerSeries (MvPowerSeries σ R)

def

uncurryFun

L60 ↗

EtaleFundamentalGroups.Kummer.MvPowerSeriesFinite.uncurryFun

Documentation

Undo curryFun by joining the two exponent vectors.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u v
open Finset
open IsLocalRing
namespace MvPowerSeriesFinite
variable {R : Type u} {σ : Type v}

Lean source · statement

def uncurryFun [Semiring R] :
    PowerSeries (MvPowerSeries σ R) → MvPowerSeries (Unit ⊕ σ) R

lemma

coeff_coeff_curryFun

L67 ↗

EtaleFundamentalGroups.Kummer.MvPowerSeriesFinite.coeff_coeff_curryFun

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u v
open Finset
open IsLocalRing
namespace MvPowerSeriesFinite
variable {R : Type u} {σ : Type v}

Lean source · statement

lemma coeff_coeff_curryFun [Semiring R]
    (p : MvPowerSeries (Unit ⊕ σ) R) (n : ℕ) (d : σ →₀ ℕ) :
    MvPowerSeries.coeff d (PowerSeries.coeff n (curryFun p)) =
      MvPowerSeries.coeff ((Finsupp.single () n).sumElim d) p

lemma

coeff_uncurryFun

L85 ↗

EtaleFundamentalGroups.Kummer.MvPowerSeriesFinite.coeff_uncurryFun

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u v
open Finset
open IsLocalRing
namespace MvPowerSeriesFinite
variable {R : Type u} {σ : Type v}

Lean source · statement

lemma coeff_uncurryFun [Semiring R]
    (p : PowerSeries (MvPowerSeries σ R)) (d : Unit ⊕ σ →₀ ℕ) :
    MvPowerSeries.coeff d (uncurryFun p) =
      MvPowerSeries.coeff ((splitIndex (σ := σ) d).2)
        (PowerSeries.coeff ((splitIndex (σ := σ) d).1) p)

lemma

curryFun_mul

L93 ↗

EtaleFundamentalGroups.Kummer.MvPowerSeriesFinite.curryFun_mul

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u v
open Finset
open IsLocalRing
namespace MvPowerSeriesFinite
variable {R : Type u} {σ : Type v}

Lean source · statement

lemma curryFun_mul [CommSemiring R]
    (p q : MvPowerSeries (Unit ⊕ σ) R) :
    curryFun (p * q) = curryFun p * curryFun q

def

sumUnitEquivPowerSeries

L140 ↗

EtaleFundamentalGroups.Kummer.MvPowerSeriesFinite.sumUnitEquivPowerSeries

Documentation

A finite-variable multivariate power-series ring with one distinguished variable is an iterated univariate power-series ring.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u v
open Finset
open IsLocalRing
namespace MvPowerSeriesFinite
variable {R : Type u} {σ : Type v}

Lean source · full declaration

def sumUnitEquivPowerSeries [CommSemiring R] :
    MvPowerSeries (Unit ⊕ σ) R ≃+* PowerSeries (MvPowerSeries σ R) where
  toFun := curryFun
  invFun := uncurryFun
  left_inv p := by
    apply MvPowerSeries.ext
    intro d
    rw [coeff_uncurryFun, coeff_coeff_curryFun]
    exact congr_arg (fun e ↦ MvPowerSeries.coeff e p)
      ((splitIndex (σ := σ)).symm_apply_apply d)
  right_inv p := by
    apply PowerSeries.ext
    intro n
    apply MvPowerSeries.ext
    intro d
    rw [coeff_coeff_curryFun, coeff_uncurryFun,
      splitIndex_apply_sumElim]
  map_mul' := curryFun_mul
  map_add' p q := by
    apply PowerSeries.ext
    intro n
    apply MvPowerSeries.ext
    intro d
    rw [coeff_coeff_curryFun, map_add, map_add, map_add,
      coeff_coeff_curryFun, coeff_coeff_curryFun]

theorem

isNoetherianRing_mvPowerSeries_fin

L170 ↗

EtaleFundamentalGroups.Kummer.isNoetherianRing_mvPowerSeries_fin

Documentation

Formal power series in n variables over a Noetherian coefficient ring form a Noetherian ring.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u v
open Finset
open IsLocalRing

Lean source · statement

theorem isNoetherianRing_mvPowerSeries_fin
    (R : Type u) [CommRing R] [IsNoetherianRing R] (n : ℕ) :
    IsNoetherianRing (MvPowerSeries (Fin n) R)

theorem

isNoetherianRing_mvPowerSeries_finite

L193 ↗

EtaleFundamentalGroups.Kummer.isNoetherianRing_mvPowerSeries_finite

Documentation

A multivariate formal-power-series ring over a Noetherian ring is Noetherian whenever its variable type is finite.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u v
open Finset
open IsLocalRing

Lean source · statement

theorem isNoetherianRing_mvPowerSeries_finite
    {R : Type u} {σ : Type v} [CommRing R] [IsNoetherianRing R] [Finite σ] :
    IsNoetherianRing (MvPowerSeries σ R)

instance

mvPowerSeries_isNoetherianRing_of_finite

L205 ↗

EtaleFundamentalGroups.Kummer.mvPowerSeries_isNoetherianRing_of_finite

Documentation

Typeclass form of the finite-variable formal-power-series Hilbert basis theorem.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u v
open Finset
open IsLocalRing

Lean source · statement

instance mvPowerSeries_isNoetherianRing_of_finite
    {R : Type u} {σ : Type v} [CommRing R] [IsNoetherianRing R] [Finite σ] :
    IsNoetherianRing (MvPowerSeries σ R)

theorem

maximalAdicCompletion_isNoetherianRing_of_generators

L212 ↗

EtaleFundamentalGroups.Kummer.maximalAdicCompletion_isNoetherianRing_of_generators

Documentation

A finite family generating the closed point presents the maximal-adic completion as a quotient of a Noetherian finite-variable power-series ring.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u v
open Finset
open IsLocalRing

Lean source · statement

theorem maximalAdicCompletion_isNoetherianRing_of_generators
    {B : Type u} [CommRing B] [IsLocalRing B] [IsNoetherianRing B]
    {ι : Type v} [Finite ι] (t : ι → B)
    (hgen : Ideal.span (Set.range t) = maximalIdeal B) :
    IsNoetherianRing (AdicCompletion (maximalIdeal B) B)

theorem

maximalAdicCompletion_isNoetherianRing

L225 ↗

EtaleFundamentalGroups.Kummer.maximalAdicCompletion_isNoetherianRing

Documentation

The maximal-adic completion of every Noetherian local ring is Noetherian. A finite generating family is obtained from Noetherianity, so no regular-system hypothesis or bound on the dimension is required.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u v
open Finset
open IsLocalRing

Lean source · statement

theorem maximalAdicCompletion_isNoetherianRing
    {B : Type u} [CommRing B] [IsLocalRing B] [IsNoetherianRing B] :
    IsNoetherianRing (AdicCompletion (maximalIdeal B) B)

instance

maximalAdicCompletion_isNoetherianRing_instance

L246 ↗

EtaleFundamentalGroups.Kummer.maximalAdicCompletion_isNoetherianRing_instance

Documentation

Typeclass form of Noetherianity of maximal-adic completion.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u v
open Finset
open IsLocalRing

Lean source · statement

instance maximalAdicCompletion_isNoetherianRing_instance
    {B : Type u} [CommRing B] [IsLocalRing B] [IsNoetherianRing B] :
    IsNoetherianRing (AdicCompletion (maximalIdeal B) B)

Module documentation

Noetherian finite-variable power-series rings

Declarations