Module

SeparableClosureAutEquiv.lean

Nyll.ValuedFieldTheory.Valuation.Completion.SeparableClosureAutEquiv

3 declarations indexed from sourceView source ↗

Module documentation

Restriction from an algebraic closure to its separable closure

The algebraic closure is purely inseparable over the separable closure, so an automorphism is uniquely determined by its restriction. Normality supplies extensions of automorphisms, and restriction is continuous for the Krull topology.

Imports4

Mathlib.FieldTheory.Galois.Profinite
Mathlib.FieldTheory.IsSepClosed
Mathlib.FieldTheory.Normal.Basic
Mathlib.FieldTheory.PurelyInseparable.Basic

Imported by3

def

separableClosureAutEquiv

L28 ↗

ValuationTheory.Completion.separableClosureAutEquiv

Documentation

Restriction identifies the automorphism groups of the algebraic and separable closures over an arbitrary field.

Source context 3 commands

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

noncomputable section
namespace ValuationTheory.Completion
variable (K : Type*) [Field K]

Lean source · statement

def separableClosureAutEquiv :
    Gal(AlgebraicClosure K/K) ≃* Gal(SeparableClosure K/K)

theorem

separableClosureAutEquiv_apply

L46 ↗

ValuationTheory.Completion.separableClosureAutEquiv_apply

Documentation

Restriction preserves the action on every element of the separable closure.

Source context 3 commands

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

noncomputable section
namespace ValuationTheory.Completion
variable (K : Type*) [Field K]

Lean source · statement

theorem separableClosureAutEquiv_apply (σ : Gal(AlgebraicClosure K/K))
    (s : SeparableClosure K) :
    (separableClosureAutEquiv K σ s : AlgebraicClosure K) = σ (s : AlgebraicClosure K)

theorem

continuous_separableClosureAutEquiv

L52 ↗

ValuationTheory.Completion.continuous_separableClosureAutEquiv

Documentation

Restriction to the separable closure is continuous for the Krull topologies.

Source context 3 commands

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

noncomputable section
namespace ValuationTheory.Completion
variable (K : Type*) [Field K]

Lean source · statement

theorem continuous_separableClosureAutEquiv : Continuous (separableClosureAutEquiv K)

Module documentation

Restriction from an algebraic closure to its separable closure

Declarations

separableClosureAutEquiv

separableClosureAutEquiv_apply

continuous_separableClosureAutEquiv