Module

CompleteQuotient.lean

Nyll.EtaleFundamentalGroups.Purity.Local.CompleteQuotient

2 declarations indexed from sourceView source ↗

Module documentation

Quotients of complete local rings

A quotient of a Noetherian complete local ring by an ideal contained in the maximal ideal is again complete local, hence Henselian. Completeness is first proved for the extended maximal ideal; surjectivity of the quotient map then identifies this ideal with the maximal ideal of the quotient.

Imports2

Mathlib.RingTheory.LocalRing.Quotient
Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.HenselianFinite

Imported by3

theorem

isAdicComplete_map_maximalIdeal_quotient

L30 ↗

EtaleFundamentalGroups.isAdicComplete_map_maximalIdeal_quotient

Documentation

The quotient of a Noetherian adically complete ring is complete for the extension of the ideal of definition.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open ValuationTheory.DiscreteValuationField
universe u

Lean source · statement

theorem isAdicComplete_map_maximalIdeal_quotient
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    [IsAdicComplete (maximalIdeal R) R] (I : Ideal R) :
    IsAdicComplete
      ((maximalIdeal R).map (algebraMap R (R ⧸ I))) (R ⧸ I)

theorem

henselianLocalRing_quotient_of_isAdicComplete

L42 ↗

EtaleFundamentalGroups.henselianLocalRing_quotient_of_isAdicComplete