Module

HenselianSeparableClosureTopology.lean

Nyll.ValuedFieldTheory.Valuation.Completion.HenselianSeparableClosureTopology

3 declarations indexed from sourceView source ↗

Module documentation

The Krull topology on separable closures across completion

Restriction is continuous. The source of restriction is the compact Galois group of a separable closure, and the target is Hausdorff, so its inverse is continuous as well. Both maps retain the chosen embedding.

Imports4

Nyll.ValuedFieldTheory.Valuation.Completion.HenselianSeparableAutContinuous
Mathlib.FieldTheory.Galois.Profinite
Mathlib.Topology.Algebra.ContinuousMonoidHom
Mathlib.Topology.Homeomorph.Lemmas

Imported by2

def

separableClosureAutContinuousEquiv

L32 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.separableClosureAutContinuousEquiv

Documentation

Completing a Henselian DVF identifies the Krull topological groups of the two separable closures, for the specified embedding between them.

Source context 3 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.HenselianDVF
variable {K : Type*} [Field K] (base : HenselianDVF K)
  {S E : Type*} [Field S] [Field E] [Algebra K S]
  [Algebra base.valuation.Completion E] [Algebra K E]
  [IsScalarTower K base.valuation.Completion E] [Algebra.IsSeparable K S]
  [IsSepClosed S] [Algebra.IsSeparable base.valuation.Completion E] [IsSepClosed E]

Lean source · statement

def separableClosureAutContinuousEquiv (i : S →ₐ[K] E) :
    (S ≃ₐ[K] S) ≃ₜ* (E ≃ₐ[base.valuation.Completion] E)

theorem

separableClosureAutContinuousEquiv_apply

L47 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.separableClosureAutContinuousEquiv_apply

Documentation

The continuous group isomorphism preserves the original action on every element of the embedded separable closure.

Source context 3 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.HenselianDVF
variable {K : Type*} [Field K] (base : HenselianDVF K)
  {S E : Type*} [Field S] [Field E] [Algebra K S]
  [Algebra base.valuation.Completion E] [Algebra K E]
  [IsScalarTower K base.valuation.Completion E] [Algebra.IsSeparable K S]
  [IsSepClosed S] [Algebra.IsSeparable base.valuation.Completion E] [IsSepClosed E]

Lean source · statement

theorem separableClosureAutContinuousEquiv_apply
    (i : S →ₐ[K] E) (σ : S ≃ₐ[K] S) (s : S) :
    base.separableClosureAutContinuousEquiv i σ (i s) = i (σ s)

theorem

separableClosureAutContinuousEquiv_symm_apply

L53 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.separableClosureAutContinuousEquiv_symm_apply

Documentation

The inverse homeomorphism is the same restriction of field actions.

Source context 3 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.HenselianDVF
variable {K : Type*} [Field K] (base : HenselianDVF K)
  {S E : Type*} [Field S] [Field E] [Algebra K S]
  [Algebra base.valuation.Completion E] [Algebra K E]
  [IsScalarTower K base.valuation.Completion E] [Algebra.IsSeparable K S]
  [IsSepClosed S] [Algebra.IsSeparable base.valuation.Completion E] [IsSepClosed E]

Lean source · statement

theorem separableClosureAutContinuousEquiv_symm_apply
    (i : S →ₐ[K] E) (σ : E ≃ₐ[base.valuation.Completion] E) (s : S) :
    i ((base.separableClosureAutContinuousEquiv i).symm σ s) = σ (i s)

Module documentation

The Krull topology on separable closures across completion

Declarations

separableClosureAutContinuousEquiv

separableClosureAutContinuousEquiv_apply

separableClosureAutContinuousEquiv_symm_apply