Module

RegularPairNoetherian.lean

Nyll.EtaleFundamentalGroups.Kummer.Completions.MaximalAdic.RegularPairNoetherian

3 declarations indexed from sourceView source ↗

Module documentation

Noetherianity of the maximal-adic completion of a regular pair

Mathlib constructs the maximal-adic completion of a Noetherian local ring as a complete local ring, but does not currently provide its Noetherian-ring instance. For the two-parameter situation used by one-point inertia, there is a concrete source for that missing finiteness.

If x, y is a regular system generating the closed point of B, evaluate the two variables of the iterated power-series ring B⟦X⟧⟦X⟧ at the images of x and y in B̂. The source is Noetherian by the univariate power-series Hilbert basis theorem. Surjectivity is proved one variable at a time. Modulo y, the completed quotient is a DVR, so the inner evaluation is separated; modulo its remaining uniformizer the map is the usual residue map of the completion. Adic completeness then lifts residue-level surjectivity first across x and then across y.

This supplies an actual Noetherian source and does not add Noetherianity of the completion as a hypothesis.

Imports5

Mathlib.RingTheory.AdicCompletion.Noetherian
Mathlib.RingTheory.AdicCompletion.Topology
Mathlib.RingTheory.PowerSeries.Evaluation
Mathlib.RingTheory.PowerSeries.Ideal
Nyll.EtaleFundamentalGroups.Kummer.Completions.RegularPair.ParameterQuotient

Imported by6

theorem

of_le_ideal

L46 ↗

EtaleFundamentalGroups.Kummer.IsHausdorff.of_le_ideal

Documentation

Hausdorffness for a larger ideal implies Hausdorffness for a smaller ideal. This elementary direction does not require a Noetherian ring.

Source context 6 commands

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

noncomputable section
open IsLocalRing
open RingTheory.Sequence
open scoped PowerSeries.WithPiTopology
namespace EtaleFundamentalGroups.Kummer
universe u

Lean source · statement

theorem IsHausdorff.of_le_ideal
    {R : Type u} [CommRing R] {I J : Ideal R}
    [IsHausdorff J R] (hIJ : I ≤ J) : IsHausdorff I R

theorem

iteratedPowerSeries_surjective_maximalAdicCompletion_of_regularPair

L57 ↗

EtaleFundamentalGroups.Kummer.iteratedPowerSeries_surjective_maximalAdicCompletion_of_regularPair

Documentation

Evaluation of two successive formal variables at a regular pair in the maximal-adic completion is surjective.

Source context 6 commands

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

noncomputable section
open IsLocalRing
open RingTheory.Sequence
open scoped PowerSeries.WithPiTopology
namespace EtaleFundamentalGroups.Kummer
universe u

Lean source · statement

theorem iteratedPowerSeries_surjective_maximalAdicCompletion_of_regularPair
    {B : Type u} [CommRing B] [IsLocalRing B] [IsNoetherianRing B]
    {x y : B}
    (hreg : IsRegular B [x, y])
    (hgen : Ideal.ofList [x, y] = maximalIdeal B) :
    ∃ f : PowerSeries (PowerSeries B) →+*
        AdicCompletion (maximalIdeal B) B,
      Function.Surjective f

theorem

maximalAdicCompletion_isNoetherianRing_of_regularPair

L196 ↗

EtaleFundamentalGroups.Kummer.maximalAdicCompletion_isNoetherianRing_of_regularPair

Documentation

The maximal-adic completion of a Noetherian local ring equipped with a two-element regular system of parameters is Noetherian.

Source context 6 commands

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

noncomputable section
open IsLocalRing
open RingTheory.Sequence
open scoped PowerSeries.WithPiTopology
namespace EtaleFundamentalGroups.Kummer
universe u

Lean source · statement

theorem maximalAdicCompletion_isNoetherianRing_of_regularPair
    {B : Type u} [CommRing B] [IsLocalRing B] [IsNoetherianRing B]
    {x y : B}
    (hreg : IsRegular B [x, y])
    (hgen : Ideal.ofList [x, y] = maximalIdeal B) :
    IsNoetherianRing (AdicCompletion (maximalIdeal B) B)

Module documentation

Noetherianity of the maximal-adic completion of a regular pair

Declarations

of_le_ideal

iteratedPowerSeries_surjective_maximalAdicCompletion_of_regularPair

maximalAdicCompletion_isNoetherianRing_of_regularPair