NYLL
Module

FiniteEtaleChosenLocalization.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.FiniteEtaleChosenLocalization
2 declarations indexed from sourceView source ↗

Module documentation

A chosen closed factor of a finite etale algebra over a strict Henselian base

For a specified prime over the closed point, separable closedness makes the residue-field map bijective. The pointed Henselian theorem then identifies the corresponding localization with the base. Unlike an existence theorem, this keeps a prime selected by an independent component construction.

Imports2
Imported by1

Declarations

theorem

isSepClosed_of_ringEquiv_chosenLocalization

L27 ↗
EtaleFundamentalGroups.isSepClosed_of_ringEquiv_chosenLocalization
Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe u v
Lean source · statement
theorem isSepClosed_of_ringEquiv_chosenLocalization
    {k : Type u} {l : Type v} [Field k] [Field l] [IsSepClosed k]
    (e : k ≃+* l) : IsSepClosed l
theorem

strictHenselian_finiteEtale_localizationAlgEquiv_of_primesOver

L44 ↗
EtaleFundamentalGroups.strictHenselian_finiteEtale_localizationAlgEquiv_of_primesOver
Documentation

Every specified closed prime of an etale algebra over a strictly Henselian local ring gives a localization canonically isomorphic to the base. The prime is input data, while the residue-field bijection is produced internally from etaleness and separable closedness.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe u v
Lean source · statement
theorem strictHenselian_finiteEtale_localizationAlgEquiv_of_primesOver
    {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    [Algebra R S] [HenselianLocalRing R]
    [IsSepClosed (IsLocalRing.ResidueField R)] [Algebra.Etale R S]
    (q : (IsLocalRing.maximalIdeal R).primesOver S) :
    Nonempty (R ≃ₐ[R] Localization.AtPrime q.1)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.