Module

NormSubgroupOrderEmbedding.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.Existence.NormSubgroupOrderEmbedding

15 declarations indexed from sourceView source ↗

Module documentation

Finite abelian subextensions and native norm subgroups

A finite abelian subextension of the fixed separable closure determines an ordinary norm subgroup of the local multiplicative group. This module proves that the resulting assignment is an order embedding into the opposite poset of native open finite-index subgroups. Surjectivity is the remaining local existence-theorem input.

Imports5

Imported by7

theorem

finiteAbelianSubextension_finite_over_absoluteBase

L36 ↗

LocalClassFieldTheory.finiteAbelianSubextension_finite_over_absoluteBase

Documentation

Finiteness over the concrete ground-field fixing group implies finiteness over the abstract class-formation baseField.

Source context 5 commands

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

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

Lean source · statement

theorem finiteAbelianSubextension_finite_over_absoluteBase
    (L : FiniteAbelianSubextension (intrinsicAbstractBase K)) :
    Finite ((baseField (intrinsicAbsoluteGalois K)).toSubgroup ⧸
      extensionSubgroup (baseField (intrinsicAbsoluteGalois K)) L.field
        (le_baseField L.field))

theorem

finiteAbelianSubextension_normal_over_absoluteBase

L50 ↗

LocalClassFieldTheory.finiteAbelianSubextension_normal_over_absoluteBase

Documentation

Normality over the concrete ground-field fixing group is normality over the abstract class-formation baseField.

Source context 5 commands

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

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

Lean source · statement

theorem finiteAbelianSubextension_normal_over_absoluteBase
    (L : FiniteAbelianSubextension (intrinsicAbstractBase K)) :
    (extensionSubgroup (baseField (intrinsicAbsoluteGalois K)) L.field
      (le_baseField L.field)).Normal

def

finiteAbelianNormSubgroup

L79 ↗

LocalClassFieldTheory.finiteAbelianNormSubgroup

Documentation

The actual norm subgroup of the fixed field represented by an abstract finite abelian extension.

Source context 5 commands

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

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

Lean source · statement

def finiteAbelianNormSubgroup
    (L : FiniteAbelianSubextension (intrinsicAbstractBase K)) : Subgroup Kˣ

theorem

finiteAbelianSubextension_fixedField_isAbelianGalois

L87 ↗

LocalClassFieldTheory.finiteAbelianSubextension_fixedField_isAbelianGalois

Documentation

The fixed field represented by an abstract finite abelian extension is an actual finite abelian extension of K. The commutativity assertion is transported across the concrete quotient--Galois-group equivalence, rather than being inferred merely from the name of the abstract package.

Source context 5 commands

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

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

Lean source · statement

theorem finiteAbelianSubextension_fixedField_isAbelianGalois
    (L : FiniteAbelianSubextension (intrinsicAbstractBase K)) :
    IsAbelianGalois K
      (abstractFixedField K (SeparableClosure K) L.field)

theorem

finiteAbelianSubextension_compositum_fixedField

L128 ↗

LocalClassFieldTheory.finiteAbelianSubextension_compositum_fixedField

Documentation

The concrete fixed field of an abstract compositum is the compositum of the two concrete fixed fields inside the chosen separable closure.

Source context 5 commands

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

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

Lean source · statement

theorem finiteAbelianSubextension_compositum_fixedField
    (U T : FiniteAbelianSubextension (intrinsicAbstractBase K)) :
    abstractFixedField K (SeparableClosure K) (U.compositum T).field =
      abstractFixedField K (SeparableClosure K) U.field ⊔
        abstractFixedField K (SeparableClosure K) T.field

theorem

relativeNorm_abstractFixedFieldUnit_val_of_isGalois

L149 ↗

LocalClassFieldTheory.relativeNorm_abstractFixedFieldUnit_val_of_isGalois

Documentation

The relative class-formation norm of a unit in an arbitrary abstract fixed field is the ordinary field norm, before identifying the base fixed units with Kˣ.

Source context 5 commands

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

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

Lean source · statement

theorem relativeNorm_abstractFixedFieldUnit_val_of_isGalois
    (H : ClosedSubgroup (intrinsicAbsoluteGalois K))
    (hH : H.toSubgroup ≤ (intrinsicAbstractBase K).toSubgroup)
    [Finite ((intrinsicAbstractBase K).toSubgroup ⧸
      extensionSubgroup (intrinsicAbstractBase K) H hH)]
    [FiniteDimensional K
      (abstractFixedField K (SeparableClosure K) H)]
    [IsGalois K (abstractFixedField K (SeparableClosure K) H)]
    (x : (abstractFixedField K (SeparableClosure K) H)ˣ) :
    ((Additive.toMul
      ((relativeNorm (intrinsicAbsoluteUnits K) (intrinsicAbstractBase K)
        H hH (abstractFixedFieldUnitsEquivGaloisFixed
          K (SeparableClosure K) H (Additive.ofMul x))).1 :
        Additive (SeparableClosure K)ˣ) : (SeparableClosure K)ˣ) :
      SeparableClosure K) =
      algebraMap K (SeparableClosure K)
        (Algebra.norm K
          (x : abstractFixedField K (SeparableClosure K) H))

theorem

baseUnitsEquivGaloisAmbientFixed_symm_relativeNorm_abstractFixedFieldUnit_eq_normUnits

L201 ↗

LocalClassFieldTheory.baseUnitsEquivGaloisAmbientFixed_symm_relativeNorm_abstractFixedFieldUnit_eq_normUnits

Documentation

The preceding norm identity after identifying the base fixed units with Additive Kˣ.

Source context 5 commands

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

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

Lean source · statement

theorem baseUnitsEquivGaloisAmbientFixed_symm_relativeNorm_abstractFixedFieldUnit_eq_normUnits
    (H : ClosedSubgroup (intrinsicAbsoluteGalois K))
    (hH : H.toSubgroup ≤ (intrinsicAbstractBase K).toSubgroup)
    [Finite ((intrinsicAbstractBase K).toSubgroup ⧸
      extensionSubgroup (intrinsicAbstractBase K) H hH)]
    [FiniteDimensional K
      (abstractFixedField K (SeparableClosure K) H)]
    [IsGalois K (abstractFixedField K (SeparableClosure K) H)]
    (x : (abstractFixedField K (SeparableClosure K) H)ˣ) :
    (baseUnitsEquivGaloisAmbientFixed K (SeparableClosure K)).symm
      (relativeNorm (intrinsicAbsoluteUnits K) (intrinsicAbstractBase K)
        H hH (abstractFixedFieldUnitsEquivGaloisFixed
          K (SeparableClosure K) H (Additive.ofMul x))) =
      Additive.ofMul
        (normUnits K (abstractFixedField K (SeparableClosure K) H) x)

theorem

map_finiteAbelianNormSubgroup_eq_additiveNormSubgroup

L236 ↗

LocalClassFieldTheory.map_finiteAbelianNormSubgroup_eq_additiveNormSubgroup

Documentation

Transporting the abstract finite norm subgroup back to Kˣ gives literally the ordinary norm subgroup of the represented fixed field.

Source context 5 commands

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

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

Lean source · statement

theorem map_finiteAbelianNormSubgroup_eq_additiveNormSubgroup
    (L : FiniteAbelianSubextension (intrinsicAbstractBase K)) :
    (L.normSubgroup (intrinsicAbsoluteUnits K)).map
        (baseUnitsEquivGaloisAmbientFixed K (SeparableClosure K)).symm.toAddMonoidHom =
      additiveNormSubgroup K
        (abstractFixedField K (SeparableClosure K) L.field)

theorem

finiteAbelianNormSubgroup_le_of_abstractNormSubgroup_le_map

L305 ↗

LocalClassFieldTheory.finiteAbelianNormSubgroup_le_of_abstractNormSubgroup_le_map

Documentation

An abstract fixed-coefficient norm containment transports back to the corresponding containment of ordinary norm subgroups in Kˣ.

Source context 5 commands

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

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

Lean source · statement

theorem finiteAbelianNormSubgroup_le_of_abstractNormSubgroup_le_map
    (L : FiniteAbelianSubextension (intrinsicAbstractBase K))
    (H : Subgroup Kˣ)
    (h :
      L.normSubgroup (intrinsicAbsoluteUnits K) ≤
        H.toAddSubgroup.map
          (baseUnitsEquivGaloisAmbientFixed K (SeparableClosure K)).toAddMonoidHom) :
    finiteAbelianNormSubgroup K L ≤ H

theorem

finiteAbelianNormSubgroup_isOpen

L337 ↗

LocalClassFieldTheory.finiteAbelianNormSubgroup_isOpen

Documentation

States the theorem finiteAbelianNormSubgroup_isOpen.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
variable (K : Type) [Field K]
section LocalField
variable [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]

Lean source · statement

theorem finiteAbelianNormSubgroup_isOpen
    (L : FiniteAbelianSubextension (intrinsicAbstractBase K)) :
    IsOpen (finiteAbelianNormSubgroup K L : Set Kˣ)

theorem

finiteAbelianNormSubgroup_finiteIndex

L354 ↗

LocalClassFieldTheory.finiteAbelianNormSubgroup_finiteIndex

Documentation

States the theorem finiteAbelianNormSubgroup_finiteIndex.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
variable (K : Type) [Field K]
section LocalField
variable [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]

Lean source · statement

theorem finiteAbelianNormSubgroup_finiteIndex
    (L : FiniteAbelianSubextension (intrinsicAbstractBase K)) :
    (finiteAbelianNormSubgroup K L).FiniteIndex

def

finiteAbelianNormSubgroupMap

L385 ↗

LocalClassFieldTheory.finiteAbelianNormSubgroupMap

Documentation

The norm-subgroup map, sending a finite abelian extension to its ordinary norm subgroup, with native openness and finite index recorded.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
variable (K : Type) [Field K]
section LocalField
variable [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]

Lean source · statement

def finiteAbelianNormSubgroupMap :
    FiniteAbelianSubextension (intrinsicAbstractBase K) →
      OpenFiniteIndexSubgroup K

theorem

finiteAbelianNormSubgroupMap_injective

L393 ↗

LocalClassFieldTheory.finiteAbelianNormSubgroupMap_injective

Documentation

States the theorem finiteAbelianNormSubgroupMap_injective.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
variable (K : Type) [Field K]
section LocalField
variable [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]

Lean source · statement

theorem finiteAbelianNormSubgroupMap_injective :
    Function.Injective (finiteAbelianNormSubgroupMap K)

theorem

finiteAbelianSubextension_le_iff_normSubgroup_le

L417 ↗

LocalClassFieldTheory.finiteAbelianSubextension_le_iff_normSubgroup_le

Documentation

The order reversal for finite abelian subextensions, expressed for the actual fixed fields and their ordinary norm subgroups.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
variable (K : Type) [Field K]
section LocalField
variable [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]

Lean source · statement

theorem finiteAbelianSubextension_le_iff_normSubgroup_le
    (L₁ L₂ : FiniteAbelianSubextension (intrinsicAbstractBase K)) :
    L₁ ≤ L₂ ↔
      finiteAbelianNormSubgroup K L₂ ≤
        finiteAbelianNormSubgroup K L₁

def

finiteAbelianNormSubgroupOrderEmbedding

L435 ↗

LocalClassFieldTheory.finiteAbelianNormSubgroupOrderEmbedding

Documentation

The ordinary norm-subgroup assignment is an order embedding into the opposite poset of native open finite-index subgroups.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
variable (K : Type) [Field K]
section LocalField
variable [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]

Lean source · full declaration

def finiteAbelianNormSubgroupOrderEmbedding :
    FiniteAbelianSubextension (intrinsicAbstractBase K) ↪o
      (OpenFiniteIndexSubgroup K)ᵒᵈ where
  toFun := finiteAbelianNormSubgroupMap K
  inj' := finiteAbelianNormSubgroupMap_injective K
  map_rel_iff' := by
    intro L₁ L₂
    change finiteAbelianNormSubgroup K L₂ ≤
        finiteAbelianNormSubgroup K L₁ ↔ L₁ ≤ L₂
    exact (finiteAbelianSubextension_le_iff_normSubgroup_le K L₁ L₂).symm

Module documentation

Finite abelian subextensions and native norm subgroups

Declarations