Module

ResidueTrivialFiniteEtale.lean

Nyll.SchemeTheory.FiniteEtale.Henselian.ResidueTrivialFiniteEtale

2 declarations indexed from sourceView source ↗

Module documentation

Residue-trivial finite etale local algebras over a Henselian base

A finite etale local algebra over a Henselian local ring is the base ring as soon as its residue-field map is bijective. This is the pointed form of the usual strict-Henselian splitting argument: instead of assuming that the base residue field is separably closed, we use the actual residue-field isomorphism of the selected factor.

Imports2

Mathlib.RingTheory.Henselian
Mathlib.RingTheory.LocalRing.Etale

Imported by2

theorem

algebraMap_bijective_of_henselian_of_residueFieldMap_bijective_of_finiteEtale_local

L34 ↗

EtaleFundamentalGroups.algebraMap_bijective_of_henselian_of_residueFieldMap_bijective_of_finiteEtale_local

Documentation

A residue-trivial finite etale local algebra over a Henselian local ring is trivial.

FaithfulSMul R S is only the injectivity input. Surjectivity is obtained by lifting the residue of a monogenic generator with Hensel's lemma and then using uniqueness of a simple root in the local target.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe u

Lean source · statement

theorem algebraMap_bijective_of_henselian_of_residueFieldMap_bijective_of_finiteEtale_local
    {R S : Type u} [CommRing R] [CommRing S]
    [Algebra R S] [HenselianLocalRing R] [IsLocalRing S]
    [Module.Finite R S] [FaithfulSMul R S] [Algebra.Etale R S]
    (hres : Function.Bijective
      (IsLocalRing.ResidueField.map (algebraMap R S))) :
    Function.Bijective (algebraMap R S)

def

henselianResidueTrivialFiniteEtaleAlgEquiv

L143 ↗

EtaleFundamentalGroups.henselianResidueTrivialFiniteEtaleAlgEquiv