Module

FiniteGeneratorEvaluation.lean

Nyll.EtaleFundamentalGroups.Kummer.Completions.MaximalAdic.FiniteGeneratorEvaluation

2 declarations indexed from sourceView source ↗

Module documentation

Finite-generator presentations of maximal-adic completions

If a finite family generates the maximal ideal of a Noetherian local ring, evaluation of multivariate formal power series at the images of that family surjects onto the maximal-adic completion. This works for an arbitrary finite number of generators and does not use regularity.

The remaining step from this presentation to Noetherianity is precisely the multivariate formal-power-series Hilbert basis theorem for a finite variable type. Mathlib currently supplies that theorem only for the univariate PowerSeries specialization.

Imports5

Mathlib.RingTheory.AdicCompletion.Functoriality
Mathlib.RingTheory.AdicCompletion.LocalRing
Mathlib.RingTheory.AdicCompletion.Noetherian
Mathlib.RingTheory.AdicCompletion.Topology
Mathlib.RingTheory.MvPowerSeries.Evaluation

Imported by2

theorem

mvPowerSeries_surjective_maximalAdicCompletion_of_generators

L39 ↗

EtaleFundamentalGroups.Kummer.mvPowerSeries_surjective_maximalAdicCompletion_of_generators

Documentation

Evaluation at any finite generating family of the closed point is a surjection from the corresponding multivariate power-series ring onto the maximal-adic completion.

Source context 5 commands

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

noncomputable section
open IsLocalRing
open scoped MvPowerSeries.WithPiTopology
namespace EtaleFundamentalGroups.Kummer
universe u v

Lean source · statement

theorem mvPowerSeries_surjective_maximalAdicCompletion_of_generators
    {B : Type u} [CommRing B] [IsLocalRing B] [IsNoetherianRing B]
    {ι : Type v} [Finite ι]
    (t : ι → B)
    (hgen : Ideal.span (Set.range t) = maximalIdeal B) :
    ∃ f : MvPowerSeries ι B →+*
        AdicCompletion (maximalIdeal B) B,
      Function.Surjective f

theorem

mvPowerSeries_fin_surjective_maximalAdicCompletion_of_generators

L144 ↗

EtaleFundamentalGroups.Kummer.mvPowerSeries_fin_surjective_maximalAdicCompletion_of_generators