Module

UnshrinkFiniteAbelianFields.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.Existence.UnshrinkFiniteAbelianFields

4 declarations indexed from sourceView source ↗

Module documentation

Returning finite abelian intermediate fields from the small base

The converse to the small-base transport: an intermediate field over Shrink K in the original separable closure remains finite abelian over K.

Imports1

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.Existence.ShrinkFiniteAbelianFields

Imported by2

def

unshrinkIntermediateFieldRingEquiv

L26 ↗

LocalFieldTheory.unshrinkIntermediateFieldRingEquiv

Documentation

The same underlying field after undoing the small base change.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory
universe u
variable (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]

Lean source · full declaration

def unshrinkIntermediateFieldRingEquiv :
    letI : Small.{0} K := nonarchimedeanLocalField_small K
    letI : Algebra (Shrink.{0} K) (SeparableClosure K) :=
      shrinkSeparableClosureAlgebra K
    (F : IntermediateField (Shrink.{0} K) (SeparableClosure K)) →
      F ≃+* unshrinkIntermediateField K F := by
  let : Small.{0} K := nonarchimedeanLocalField_small K
  let : Algebra (Shrink.{0} K) (SeparableClosure K) :=
    shrinkSeparableClosureAlgebra K
  intro F
  exact RingEquiv.refl F

theorem

unshrinkIntermediateFieldRingEquiv_commutes

L40 ↗

LocalFieldTheory.unshrinkIntermediateFieldRingEquiv_commutes

Documentation

The inverse intermediate-field equivalence commutes with the base-field embeddings.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory
universe u
variable (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]

Lean source · full declaration

theorem unshrinkIntermediateFieldRingEquiv_commutes :
    letI : Small.{0} K := nonarchimedeanLocalField_small K
    letI : Algebra (Shrink.{0} K) (SeparableClosure K) :=
      shrinkSeparableClosureAlgebra K
    ∀ F : IntermediateField (Shrink.{0} K) (SeparableClosure K),
      (algebraMap K (unshrinkIntermediateField K F)).comp
          (Shrink.ringEquiv K).toRingHom =
        (unshrinkIntermediateFieldRingEquiv K F).toRingHom.comp
          (algebraMap (Shrink.{0} K) F) := by
  let : Small.{0} K := nonarchimedeanLocalField_small K
  let : Algebra (Shrink.{0} K) (SeparableClosure K) :=
    shrinkSeparableClosureAlgebra K
  intro F
  ext x
  have hbase :
      algebraMap K (SeparableClosure K) (Shrink.ringEquiv K x) =
        algebraMap (Shrink.{0} K) (SeparableClosure K) x := by
    rfl
  have hfieldK :
      ((algebraMap K (unshrinkIntermediateField K F)
        (Shrink.ringEquiv K x) : unshrinkIntermediateField K F) :
          SeparableClosure K) =
        algebraMap K (SeparableClosure K) (Shrink.ringEquiv K x) :=
    IntermediateField.coe_algebraMap_apply (unshrinkIntermediateField K F) _
  have hfieldS :
      algebraMap (Shrink.{0} K) (SeparableClosure K) x =
        ((algebraMap (Shrink.{0} K) F x : F) : SeparableClosure K) :=
    (IntermediateField.coe_algebraMap_apply F x).symm
  exact congrArg (fun y : SeparableClosure K => (y : AlgebraicClosure K))
    (hfieldK.trans (hbase.trans hfieldS))

theorem

unshrinkIntermediateField_finiteDimensional

L72 ↗

LocalFieldTheory.unshrinkIntermediateField_finiteDimensional

Documentation

Finite-dimensionality is preserved when returning to K.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory
universe u
variable (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]

Lean source · full declaration

theorem unshrinkIntermediateField_finiteDimensional :
    letI : Small.{0} K := nonarchimedeanLocalField_small K
    letI : Algebra (Shrink.{0} K) (SeparableClosure K) :=
      shrinkSeparableClosureAlgebra K
    ∀ F : IntermediateField (Shrink.{0} K) (SeparableClosure K),
      FiniteDimensional (Shrink.{0} K) F →
        FiniteDimensional K (unshrinkIntermediateField K F) := by
  let : Small.{0} K := nonarchimedeanLocalField_small K
  let : Algebra (Shrink.{0} K) (SeparableClosure K) :=
    shrinkSeparableClosureAlgebra K
  intro F hF
  let : FiniteDimensional (Shrink.{0} K) F := hF
  exact Module.Finite.of_equiv_equiv
    (Shrink.ringEquiv K) (unshrinkIntermediateFieldRingEquiv K F)
    (unshrinkIntermediateFieldRingEquiv_commutes K F)

theorem

unshrinkIntermediateField_isAbelianGalois

L89 ↗

LocalFieldTheory.unshrinkIntermediateField_isAbelianGalois

Documentation

The abelian Galois property is preserved when returning to K.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory
universe u
variable (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]

Lean source · full declaration

theorem unshrinkIntermediateField_isAbelianGalois :
    letI : Small.{0} K := nonarchimedeanLocalField_small K
    letI : Algebra (Shrink.{0} K) (SeparableClosure K) :=
      shrinkSeparableClosureAlgebra K
    ∀ F : IntermediateField (Shrink.{0} K) (SeparableClosure K),
      IsAbelianGalois (Shrink.{0} K) F →
        IsAbelianGalois K (unshrinkIntermediateField K F) := by
  let : Small.{0} K := nonarchimedeanLocalField_small K
  let : Algebra (Shrink.{0} K) (SeparableClosure K) :=
    shrinkSeparableClosureAlgebra K
  intro F hF
  let : IsAbelianGalois (Shrink.{0} K) F := hF
  exact ClassFieldTheory.isAbelianGalois_of_equiv_equiv
    (Shrink.ringEquiv K) (unshrinkIntermediateFieldRingEquiv K F)
    (unshrinkIntermediateFieldRingEquiv_commutes K F)

Module documentation

Returning finite abelian intermediate fields from the small base

Declarations

unshrinkIntermediateFieldRingEquiv

unshrinkIntermediateFieldRingEquiv_commutes

unshrinkIntermediateField_finiteDimensional

unshrinkIntermediateField_isAbelianGalois