Nyll.ValuedFieldTheory.Valuation.Completion.HenselianFixingSubgroups

Module documentation

Fixing subgroups across Henselian completion

The field generated over the completion by the image of an intermediate field has exactly the corresponding fixing subgroup. The equality is for the actual constructed automorphism correspondence, and holds without requiring the intermediate field to be finite or normal.

theorem

separableClosedAutEquiv_comap_fixingSubgroup

L31 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.separableClosedAutEquiv_comap_fixingSubgroup

Documentation

Fixing the completed image is equivalent to fixing the original intermediate field under the actual completion correspondence.

Source context 2 commands

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

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]

Lean source · statement

theorem separableClosedAutEquiv_comap_fixingSubgroup
    (i : S →ₐ[K] E) (F : IntermediateField K S) :
    (IntermediateField.adjoin base.valuation.Completion (i '' (F : Set S))).fixingSubgroup.comap
      (base.separableClosedAutEquiv i).toMonoidHom = F.fixingSubgroup

Module documentation

Fixing subgroups across Henselian completion

Declarations

separableClosedAutEquiv_comap_fixingSubgroup