NYLL
Module

ShrinkIntermediateFields.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.Existence.ShrinkIntermediateFields
5 declarations indexed from sourceView source ↗

Module documentation

Intermediate fields under a small change of base field

The base-field equivalence Shrink K ≃+* K does not change the subfields of the original separable closure. This file records that fact as an order isomorphism, with the actual underlying subfields unchanged.

Imports2
Imported by2

Declarations

def

shrinkIntermediateField

L29 ↗
LocalFieldTheory.shrinkIntermediateField
Documentation

An intermediate field of the original separable closure, viewed over the small representative of the base field.

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 shrinkIntermediateField
    (E : IntermediateField K (SeparableClosure K)) :
    letI : Small.{0} K := nonarchimedeanLocalField_small K
    letI : Algebra (Shrink.{0} K) (SeparableClosure K) :=
      shrinkSeparableClosureAlgebra K
    IntermediateField (Shrink.{0} K) (SeparableClosure K) := by
  let : Small.{0} K := nonarchimedeanLocalField_small K
  let : Algebra (Shrink.{0} K) (SeparableClosure K) :=
    shrinkSeparableClosureAlgebra K
  refine E.toSubfield.toIntermediateField ?_
  intro x
  change (algebraMap K (SeparableClosure K)) (Shrink.ringEquiv K x) ∈ E
  exact E.algebraMap_mem _
def

unshrinkIntermediateField

L44 ↗
LocalFieldTheory.unshrinkIntermediateField
Documentation

Undo the base-field change on an intermediate field.

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 unshrinkIntermediateField :
    letI : Small.{0} K := nonarchimedeanLocalField_small K
    letI : Algebra (Shrink.{0} K) (SeparableClosure K) :=
      shrinkSeparableClosureAlgebra K
    IntermediateField (Shrink.{0} K) (SeparableClosure K) →
      IntermediateField K (SeparableClosure K) := by
  let : Small.{0} K := nonarchimedeanLocalField_small K
  let : Algebra (Shrink.{0} K) (SeparableClosure K) :=
    shrinkSeparableClosureAlgebra K
  intro F
  refine F.toSubfield.toIntermediateField ?_
  intro x
  have hx := F.algebraMap_mem ((Shrink.ringEquiv K).symm x)
  change (algebraMap K (SeparableClosure K))
    (Shrink.ringEquiv K ((Shrink.ringEquiv K).symm x)) ∈ F at hx
  simpa using hx
theorem

unshrink_shrinkIntermediateField

L63 ↗
LocalFieldTheory.unshrink_shrinkIntermediateField
Documentation

Re-expressing an original intermediate field over Shrink K and back returns the same field.

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 · statement
theorem unshrink_shrinkIntermediateField
    (E : IntermediateField K (SeparableClosure K)) :
    unshrinkIntermediateField K (shrinkIntermediateField K E) = E
theorem

shrink_unshrinkIntermediateField

L71 ↗
LocalFieldTheory.shrink_unshrinkIntermediateField
Documentation

Re-expressing a small-base intermediate field over K and back returns the same field.

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 shrink_unshrinkIntermediateField :
    letI : Small.{0} K := nonarchimedeanLocalField_small K
    letI : Algebra (Shrink.{0} K) (SeparableClosure K) :=
      shrinkSeparableClosureAlgebra K
    ∀ F : IntermediateField (Shrink.{0} K) (SeparableClosure K),
      shrinkIntermediateField K (unshrinkIntermediateField K F) = F := by
  let : Small.{0} K := nonarchimedeanLocalField_small K
  let : Algebra (Shrink.{0} K) (SeparableClosure K) :=
    shrinkSeparableClosureAlgebra K
  intro F
  apply SetLike.coe_injective
  rfl
def

shrinkIntermediateFieldOrderIso

L86 ↗
LocalFieldTheory.shrinkIntermediateFieldOrderIso
Documentation

Intermediate fields of the two equivalent base-field presentations are order-isomorphic.

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 shrinkIntermediateFieldOrderIso :
    letI : Small.{0} K := nonarchimedeanLocalField_small K
    letI : Algebra (Shrink.{0} K) (SeparableClosure K) :=
      shrinkSeparableClosureAlgebra K
    IntermediateField K (SeparableClosure K) ≃o
      IntermediateField (Shrink.{0} K) (SeparableClosure K) := by
  let : Small.{0} K := nonarchimedeanLocalField_small K
  let : Algebra (Shrink.{0} K) (SeparableClosure K) :=
    shrinkSeparableClosureAlgebra K
  exact {
    toEquiv := {
      toFun := shrinkIntermediateField K
      invFun := unshrinkIntermediateField K
      left_inv := unshrink_shrinkIntermediateField K
      right_inv := shrink_unshrinkIntermediateField K
    }
    map_rel_iff' := by intro E F; rfl
  }

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