Module

ResidueClassification.lean

Nyll.EtaleFundamentalGroups.Completions.FiniteEtale.ResidueClassification

4 declarations indexed from sourceView source ↗

Module documentation

Finite étale local algebras over a complete local ring

Over a Noetherian complete local base, a finite étale local algebra is complete, hence Henselian, for its own maximal ideal. Two such algebras with isomorphic residue extensions are isomorphic over the base. This is the finite-residue replacement for imposing a separably closed residue field in the strict-Henselian splitting argument.

Imports2

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

Imported by2

theorem

isAdicComplete_maximalIdeal_of_finiteEtale_local

L31 ↗

EtaleFundamentalGroups.isAdicComplete_maximalIdeal_of_finiteEtale_local

Documentation

A finite étale local algebra over a Noetherian complete local ring is complete for its maximal ideal.

Source context 5 commands

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

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

Lean source · statement

theorem isAdicComplete_maximalIdeal_of_finiteEtale_local
    {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
    [IsLocalRing R] [IsLocalRing S] [IsNoetherianRing R]
    [IsAdicComplete (IsLocalRing.maximalIdeal R) R]
    [Module.Finite R S] [FaithfulSMul R S] [Algebra.Etale R S] :
    IsAdicComplete (IsLocalRing.maximalIdeal S) S

theorem

henselianLocalRing_of_finiteEtale_of_isAdicComplete

L50 ↗

EtaleFundamentalGroups.henselianLocalRing_of_finiteEtale_of_isAdicComplete

Documentation

A finite étale local algebra over a Noetherian complete local ring is Henselian local.

Source context 5 commands

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

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

Lean source · statement

theorem henselianLocalRing_of_finiteEtale_of_isAdicComplete
    {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
    [IsLocalRing R] [IsLocalRing S] [IsNoetherianRing R]
    [IsAdicComplete (IsLocalRing.maximalIdeal R) R]
    [Module.Finite R S] [FaithfulSMul R S] [Algebra.Etale R S] :
    HenselianLocalRing S

theorem

exists_finiteEtaleLocalAlgEquivOfResidueAlgEquiv

L66 ↗

EtaleFundamentalGroups.exists_finiteEtaleLocalAlgEquivOfResidueAlgEquiv

Documentation

Finite étale local algebras over a Noetherian complete local ring with isomorphic residue-field extensions are isomorphic over the base.

Source context 5 commands

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

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

Lean source · statement

theorem exists_finiteEtaleLocalAlgEquivOfResidueAlgEquiv
    {R S T : Type u} [CommRing R] [CommRing S] [CommRing T]
    [Algebra R S] [Algebra R T]
    [IsLocalRing R] [IsLocalRing S] [IsLocalRing T]
    [IsNoetherianRing R]
    [IsAdicComplete (IsLocalRing.maximalIdeal R) R]
    [Module.Finite R S] [FaithfulSMul R S] [Algebra.Etale R S]
    [Module.Finite R T] [FaithfulSMul R T] [Algebra.Etale R T]
    (e : IsLocalRing.ResidueField S ≃ₐ[IsLocalRing.ResidueField R]
      IsLocalRing.ResidueField T) :
    Nonempty (S ≃ₐ[R] T)

def

finiteEtaleLocalAlgEquivOfResidueAlgEquiv

L186 ↗

EtaleFundamentalGroups.finiteEtaleLocalAlgEquivOfResidueAlgEquiv

Documentation

A chosen algebra equivalence realizing the complete-local finite étale residue classification.

Source context 5 commands

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

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

Lean source · statement

def finiteEtaleLocalAlgEquivOfResidueAlgEquiv
    {R S T : Type u} [CommRing R] [CommRing S] [CommRing T]
    [Algebra R S] [Algebra R T]
    [IsLocalRing R] [IsLocalRing S] [IsLocalRing T]
    [IsNoetherianRing R]
    [IsAdicComplete (IsLocalRing.maximalIdeal R) R]
    [Module.Finite R S] [FaithfulSMul R S] [Algebra.Etale R S]
    [Module.Finite R T] [FaithfulSMul R T] [Algebra.Etale R T]
    (e : IsLocalRing.ResidueField S ≃ₐ[IsLocalRing.ResidueField R]
      IsLocalRing.ResidueField T) :
    S ≃ₐ[R] T

Module documentation

Finite étale local algebras over a complete local ring

Declarations

isAdicComplete_maximalIdeal_of_finiteEtale_local

henselianLocalRing_of_finiteEtale_of_isAdicComplete

exists_finiteEtaleLocalAlgEquivOfResidueAlgEquiv

finiteEtaleLocalAlgEquivOfResidueAlgEquiv