Module

HenselianAscent.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.HenselianAscent

2 declarations indexed from sourceView source ↗

Module documentation

Henselian ascent for finite étale local algebras over a complete base

For the complete-local chosen-factor argument, Noetherianity is not needed to make a finite étale local factor Henselian. Such a factor is finite free over the base. Adic completion commutes with finite products, so completeness of the base transfers through a finite basis. Formal unramifiedness then identifies the extended base maximal ideal with the target maximal ideal.

This is intentionally a theorem, not a global instance: consumers install the result only for the chosen local factor in scope.

Imports3

Mathlib.RingTheory.AdicCompletion.Functoriality
Mathlib.RingTheory.LocalRing.Etale
Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.HenselianFinite

Imported by5

theorem

isAdicComplete_of_moduleFinite_of_moduleFree

L36 ↗

EtaleFundamentalGroups.isAdicComplete_of_moduleFinite_of_moduleFree

Documentation

A finite free module over an adically complete ring is adically complete, without a Noetherian hypothesis.

The proof writes the module as a finite product of copies of the base and uses the canonical equivalence between the completion of a finite product and the finite product of completions.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe u v

Lean source · statement

theorem isAdicComplete_of_moduleFinite_of_moduleFree
    {R : Type u} {M : Type v} [CommRing R]
    [AddCommGroup M] [Module R M]
    (I : Ideal R) [StrongRankCondition R]
    [Module.Finite R M] [Module.Free R M]
    [IsAdicComplete I R] :
    IsAdicComplete I M

theorem

henselianLocalRing_of_finiteEtale_local_of_isAdicComplete

L78 ↗

EtaleFundamentalGroups.henselianLocalRing_of_finiteEtale_local_of_isAdicComplete