Module

Strict.lean

Nyll.SchemeTheory.FiniteEtale.Henselian.Strict

1 declaration indexed from sourceView source ↗

Module documentation

Finite étale local algebras over a strictly Henselian local ring

The connected splitting step in the strict-Henselian part of Abhyankar's lemma reduces to the following affine statement: a finite étale local algebra over a Henselian local ring with separably closed residue field is the base ring itself.

The proof is constructive at the level needed later. A monogenic generator has a residue already defined over the base residue field. Hensel lifting produces a base-ring root with the same residue, and uniqueness of a simple root in a local ring identifies the generator with its image from the base.

Imports3

Mathlib.FieldTheory.IsSepClosed
Mathlib.RingTheory.Henselian
Mathlib.RingTheory.LocalRing.Etale

Imported by3

theorem

algebraMap_bijective_of_henselian_of_isSepClosed_residue_of_finiteEtale_local

L38 ↗

EtaleFundamentalGroups.algebraMap_bijective_of_henselian_of_isSepClosed_residue_of_finiteEtale_local

Documentation

The algebra map to a finite étale local algebra over a Henselian local ring with separably closed residue field is bijective.

FaithfulSMul R S is the injectivity input naturally available for the finite normalization factors used in the one-point inertia argument.

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_isSepClosed_residue_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]
    [IsSepClosed (IsLocalRing.ResidueField R)] :
    Function.Bijective (algebraMap R S)

Module documentation

Finite étale local algebras over a strictly Henselian local ring

Declarations

algebraMap_bijective_of_henselian_of_isSepClosed_residue_of_finiteEtale_local