NYLL
Module

SeparableClosureAutTopology.lean

Nyll.ValuedFieldTheory.Valuation.Completion.SeparableClosureAutTopology
4 declarations indexed from sourceView source ↗

Module documentation

The Krull topology on algebraic and separable closures

Every element of the algebraic closure has an exponential-characteristic power in the separable closure. Stabilizers of those powers form finite intersections of open subgroups. Injectivity of Frobenius then controls the action on a finite linear basis, proving continuity of inverse restriction.

Imports7
Imported by15

Declarations

theorem

continuous_separableClosureAutEquiv_symm

L34 ↗
ValuationTheory.Completion.continuous_separableClosureAutEquiv_symm
Documentation

Extending automorphisms from the separable closure to the algebraic closure is continuous in every characteristic.

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.Completion
open scoped Topology
variable (K : Type*) [Field K]
Lean source · statement
theorem continuous_separableClosureAutEquiv_symm :
    Continuous (separableClosureAutEquiv K).symm
def

separableClosureAutContinuousEquiv

L80 ↗
ValuationTheory.Completion.separableClosureAutContinuousEquiv
Documentation

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

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.Completion
open scoped Topology
variable (K : Type*) [Field K]
Lean source · full declaration
def separableClosureAutContinuousEquiv :
    Gal(AlgebraicClosure K/K) ≃ₜ* Gal(SeparableClosure K/K) where
  toMulEquiv := separableClosureAutEquiv K
  continuous_toFun := continuous_separableClosureAutEquiv K
  continuous_invFun := continuous_separableClosureAutEquiv_symm K
theorem

separableClosureAutContinuousEquiv_apply

L87 ↗
ValuationTheory.Completion.separableClosureAutContinuousEquiv_apply
Documentation

The topological group isomorphism retains restriction on field elements.

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.Completion
open scoped Topology
variable (K : Type*) [Field K]
Lean source · statement
theorem separableClosureAutContinuousEquiv_apply
    (σ : Gal(AlgebraicClosure K/K)) (s : SeparableClosure K) :
    (separableClosureAutContinuousEquiv K σ s : AlgebraicClosure K) =
      σ (s : AlgebraicClosure K)
instance

algebraicClosureAut_compactSpace

L95 ↗
ValuationTheory.Completion.algebraicClosureAut_compactSpace
Documentation

The algebraic-closure Galois group is compact even when the base field is imperfect: restriction is a homeomorphism onto the separable-closure group.

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.Completion
open scoped Topology
variable (K : Type*) [Field K]
Lean source · statement
instance algebraicClosureAut_compactSpace : CompactSpace Gal(AlgebraicClosure K/K)

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