Module

HenselianSeparableAutContinuous.lean

Nyll.ValuedFieldTheory.Valuation.Completion.HenselianSeparableAutContinuous

1 declaration indexed from sourceView source ↗

Module documentation

Continuity of restriction across Henselian completion

A finite separable intermediate field has a primitive element. The open stabilizer of its image is sent into the subgroup fixing that intermediate field, proving continuity for the Krull topologies at the identity.

Imports4

Nyll.ValuedFieldTheory.Valuation.Completion.HenselianSeparableAutEquiv
Mathlib.FieldTheory.KrullTopology
Mathlib.FieldTheory.PrimitiveElement
Mathlib.Topology.Algebra.Group.Basic

Imported by2

theorem

continuous_separableClosedAutEquiv_symm

L32 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.continuous_separableClosedAutEquiv_symm

Documentation

Restriction through the chosen embedding is continuous for the Krull topologies on both automorphism groups.

Source context 3 commands

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

namespace ValuationTheory.DiscreteValuationField.HenselianDVF
open scoped Topology
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]

Lean source · statement

theorem continuous_separableClosedAutEquiv_symm (i : S →ₐ[K] E) :
    Continuous (base.separableClosedAutEquiv i).symm

Module documentation

Continuity of restriction across Henselian completion

Declarations

continuous_separableClosedAutEquiv_symm