Module

SeparableClosureAutomorphisms.lean

Nyll.EtaleFundamentalGroups.Inertia.SeparableClosureAutomorphisms

4 declarations indexed from sourceView source ↗

Module documentation

Automorphisms of a normal extension and its relative separable closure

Restriction is surjective by normality. It is injective because a purely inseparable extension admits at most one extension of a field embedding. For an algebraic closure this is the residue-automorphism identification in Stacks Project, Tag 0BUB.

Reference: https://stacks.math.columbia.edu/tag/0BUB

Imports2

Mathlib.FieldTheory.IsSepClosed
Mathlib.FieldTheory.PurelyInseparable.Basic

Imported by3

theorem

algEquiv_eq_of_agree_on_purelyInseparable_base

L30 ↗

EtaleFundamentalGroups.Inertia.algEquiv_eq_of_agree_on_purelyInseparable_base

Documentation

Equality over a purely inseparable subfield is checked on the actual underlying field maps. The lower automorphism base is independent of that subfield, so this owner needs no scalar tower through it.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w

Lean source · statement

theorem algEquiv_eq_of_agree_on_purelyInseparable_base
    {k : Type u} {E : Type v} (F : Type w)
    [Field k] [Field E] [Field F] [Algebra k E] [Algebra F E]
    [IsPurelyInseparable F E]
    (σ τ : Gal(E/k))
    (h : ∀ x : F, σ (algebraMap F E x) = τ (algebraMap F E x)) : σ = τ

theorem

separableClosure_restrictNormal_coefficient

L44 ↗

EtaleFundamentalGroups.Inertia.separableClosure_restrictNormal_coefficient

Documentation

Restriction to the actual relative separable closure retains the ambient coefficient. This field-only computation owns the scalar tower.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w

Lean source · statement

theorem separableClosure_restrictNormal_coefficient
    (k : Type u) (E : Type v) [Field k] [Field E] [Algebra k E] [Normal k E]
    (σ : E ≃ₐ[k] E) (z : separableClosure k E) :
    ((σ.restrictNormal (separableClosure k E)).toRingHom.toFun z).val =
      σ.toRingHom.toFun z.val

theorem

separableClosure_restrictNormalHom_injective

L53 ↗

EtaleFundamentalGroups.Inertia.separableClosure_restrictNormalHom_injective

Documentation

Restriction to the relative separable closure is injective, including in positive characteristic and without a perfectness hypothesis.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w

Lean source · statement

theorem separableClosure_restrictNormalHom_injective
    (k : Type u) (E : Type v) [Field k] [Field E] [Algebra k E] [Normal k E] :
    Function.Injective (AlgEquiv.restrictNormalHom (separableClosure k E) :
      Gal(E/k) →* Gal(separableClosure k E/k))

def

separableClosureAutEquiv

L66 ↗

EtaleFundamentalGroups.Inertia.separableClosureAutEquiv

Documentation

The canonical restriction isomorphism used to replace automorphisms of the algebraic residue closure by its separable Galois group.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w

Lean source · statement

def separableClosureAutEquiv
    (k : Type u) (E : Type v) [Field k] [Field E] [Algebra k E] [Normal k E] :
    Gal(E/k) ≃* Gal(separableClosure k E/k)

Module documentation

Automorphisms of a normal extension and its relative separable closure

Declarations

algEquiv_eq_of_agree_on_purelyInseparable_base

separableClosure_restrictNormal_coefficient

separableClosure_restrictNormalHom_injective

separableClosureAutEquiv