Module

MathlibFieldClassification.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.Existence.MathlibFieldClassification

9 declarations indexed from sourceView source ↗

Module documentation

Mathlib intermediate fields and finite local class-field theory

The finite-existence theorem is formulated internally using closed subgroups of the absolute Galois group. Here we identify those objects with finite abelian intermediate fields of Mathlib's chosen separable closure.

Imports4

Imported by2

def

abstractExtensionOfFiniteAbelianField

L29 ↗

LocalClassFieldTheory.abstractExtensionOfFiniteAbelianField

Documentation

Regard a finite abelian intermediate field as an abstract subextension.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open ClassFormation RamificationTheory
variable (K : Type) [Field K]

Lean source · statement

def abstractExtensionOfFiniteAbelianField
    (E : ClassFieldTheory.FiniteAbelianLocalExtension K) :
    FiniteAbelianSubextension (intrinsicAbstractBase K)

def

finiteAbelianFieldOfAbstractExtension

L35 ↗

LocalClassFieldTheory.finiteAbelianFieldOfAbstractExtension

Documentation

Recover the intermediate field represented by an abstract finite abelian subextension.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open ClassFormation RamificationTheory
variable (K : Type) [Field K]

Lean source · statement

def finiteAbelianFieldOfAbstractExtension
    (L : FiniteAbelianSubextension (intrinsicAbstractBase K)) :
    ClassFieldTheory.FiniteAbelianLocalExtension K

theorem

finiteAbelianFieldOfAbstractExtension_ofField

L45 ↗

LocalClassFieldTheory.finiteAbelianFieldOfAbstractExtension_ofField

Documentation

The fixed field of the abstract package constructed from an intermediate field is the original field.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open ClassFormation RamificationTheory
variable (K : Type) [Field K]

Lean source · statement

theorem finiteAbelianFieldOfAbstractExtension_ofField
    (E : ClassFieldTheory.FiniteAbelianLocalExtension K) :
    finiteAbelianFieldOfAbstractExtension K
      (abstractExtensionOfFiniteAbelianField K E) = E

theorem

abstractExtensionOfFiniteAbelianField_ofAbstract

L58 ↗

LocalClassFieldTheory.abstractExtensionOfFiniteAbelianField_ofAbstract

Documentation

Abstracting the fixed field of an abstract extension recovers the same closed subgroup, hence the same finite abelian extension.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open ClassFormation RamificationTheory
variable (K : Type) [Field K]

Lean source · statement

theorem abstractExtensionOfFiniteAbelianField_ofAbstract
    (L : FiniteAbelianSubextension (intrinsicAbstractBase K)) :
    abstractExtensionOfFiniteAbelianField K
      (finiteAbelianFieldOfAbstractExtension K L) = L

def

finiteAbelianFieldAbstractOrderIso

L71 ↗

LocalClassFieldTheory.finiteAbelianFieldAbstractOrderIso

Documentation

Concrete finite abelian intermediate fields and the abstract extension objects used by the local-existence theorem have the same order.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open ClassFormation RamificationTheory
variable (K : Type) [Field K]

Lean source · full declaration

def finiteAbelianFieldAbstractOrderIso :
    ClassFieldTheory.FiniteAbelianLocalExtension K ≃o
      FiniteAbelianSubextension (intrinsicAbstractBase K) where
  toEquiv := {
    toFun := abstractExtensionOfFiniteAbelianField K
    invFun := finiteAbelianFieldOfAbstractExtension K
    left_inv := finiteAbelianFieldOfAbstractExtension_ofField K
    right_inv := abstractExtensionOfFiniteAbelianField_ofAbstract K
  }
  map_rel_iff' := by
    intro E F
    change
      (closedFixingSubgroup K (SeparableClosure K)
        (AlgHom.fieldRange F.1.val)).toSubgroup ≤
      (closedFixingSubgroup K (SeparableClosure K)
        (AlgHom.fieldRange E.1.val)).toSubgroup ↔ E.1 ≤ F.1
    simp only [IntermediateField.fieldRange_val]
    change F.1.fixingSubgroup ≤ E.1.fixingSubgroup ↔ E.1 ≤ F.1
    constructor
    · intro h
      have hf := IntermediateField.fixedField_le h
      simpa only [InfiniteGalois.fixedField_fixingSubgroup] using hf
    · intro h
      exact E.1.fixingSubgroup_le h

def

openFiniteIndexSubgroupMathlibOrderIso

L98 ↗

LocalClassFieldTheory.openFiniteIndexSubgroupMathlibOrderIso

Documentation

The internal open-subgroup structure and the Mathlib-facing subtype encode the same subgroup with the same inclusion order.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open ClassFormation RamificationTheory
variable (K : Type) [Field K]

Lean source · full declaration

def openFiniteIndexSubgroupMathlibOrderIso
    [TopologicalSpace K] :
    OpenFiniteIndexSubgroup K ≃o
      ClassFieldTheory.OpenFiniteIndexSubgroup K where
  toEquiv := {
    toFun := fun H => ⟨H.subgroup, H.isOpen, H.finiteIndex⟩
    invFun := fun H => ⟨H.1, H.2.1, H.2.2⟩
    left_inv := by intro H; cases H; rfl
    right_inv := by intro H; cases H; rfl
  }
  map_rel_iff' := by intro H J; rfl

theorem

finiteAbelianFieldOfAbstractExtension_normSubgroup

L112 ↗

LocalClassFieldTheory.finiteAbelianFieldOfAbstractExtension_normSubgroup

Documentation

The abstract norm subgroup is the actual field-norm subgroup after identifying an abstract extension with its concrete fixed field.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open ClassFormation RamificationTheory
variable (K : Type) [Field K]

Lean source · statement

theorem finiteAbelianFieldOfAbstractExtension_normSubgroup
    (L : FiniteAbelianSubextension (intrinsicAbstractBase K)) :
    (finiteAbelianFieldOfAbstractExtension K L).normSubgroup =
      finiteAbelianNormSubgroup K L

def

finiteAbelianFieldNormSubgroupOrderIso

L120 ↗

LocalClassFieldTheory.finiteAbelianFieldNormSubgroupOrderIso

Documentation

The internal order classification, expressed entirely using concrete finite abelian intermediate fields and Mathlib's subgroup subtype.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open ClassFormation RamificationTheory
variable (K : Type) [Field K]

Lean source · statement

def finiteAbelianFieldNormSubgroupOrderIso
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    ClassFieldTheory.FiniteAbelianLocalExtension K ≃o
      (ClassFieldTheory.OpenFiniteIndexSubgroup K)ᵒᵈ

theorem

finiteAbelianFieldNormSubgroupOrderIso_apply

L131 ↗

LocalClassFieldTheory.finiteAbelianFieldNormSubgroupOrderIso_apply

Documentation

The concrete classification sends each finite abelian extension to its field-norm subgroup.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open ClassFormation RamificationTheory
variable (K : Type) [Field K]

Lean source · statement

theorem finiteAbelianFieldNormSubgroupOrderIso_apply
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (E : ClassFieldTheory.FiniteAbelianLocalExtension K) :
    (OrderDual.ofDual (finiteAbelianFieldNormSubgroupOrderIso K E)).1 =
      E.normSubgroup

Module documentation

Mathlib intermediate fields and finite local class-field theory

Declarations