NYLL
Module

FiniteGaloisRealizationNormQuotient.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.FiniteGaloisRealizationNormQuotient
19 declarations indexed from sourceView source ↗

Module documentation

Norm quotients in the compatible Galois realization

This module identifies the abstract fixed fields with the embedded copies of K and L, and transports the resulting idèle-class norm quotient and reciprocity data to the original finite Galois extension.

Imports1
Imported by2

Declarations

def

towerNormIdeleClassCommGroup

L35 ↗
GlobalClassFieldTheory.Reciprocity.towerNormIdeleClassCommGroup
Documentation

The canonical quotient group structure, fixed before forming another quotient.

Source context 10 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
Lean source · statement
def towerNormIdeleClassCommGroup
    (F : Type) [Field F] [NumberField F] :
    CommGroup (IdeleClassGroup F)
theorem

numberFieldTowerAbstractBaseField_eq

L50 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerAbstractBaseField_eq
Documentation

The fixed field of the lower subgroup is the compatible embedded copy of K.

Source context 13 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] towerNormIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem numberFieldTowerAbstractBaseField_eq :
    abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L) =
      numberFieldTowerBaseField K L
def

numberFieldTowerAbstractBaseFieldEquiv

L59 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerAbstractBaseFieldEquiv
Documentation

The original base field is canonically equivalent to the actual fixed field used by the rational class formation.

Source context 12 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] towerNormIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def numberFieldTowerAbstractBaseFieldEquiv :
    K ≃ₐ[ℚ]
      abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)
theorem

numberFieldTowerAbstractTopField_restrictScalars_eq

L70 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerAbstractTopField_restrictScalars_eq
Documentation

After restriction of scalars to ℚ, the upper relative fixed field is the chosen embedded copy of L.

Source context 13 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] towerNormIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem numberFieldTowerAbstractTopField_restrictScalars_eq :
    (abstractRelativeFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).restrictScalars ℚ =
      numberFieldInRationalSeparableClosure L
def

numberFieldTowerAbstractTopFieldEquiv

L79 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerAbstractTopFieldEquiv
Documentation

The original top field is canonically equivalent over ℚ to the actual relative fixed field used by the rational class formation.

Source context 12 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] towerNormIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def numberFieldTowerAbstractTopFieldEquiv :
    L ≃ₐ[ℚ]
      (abstractRelativeFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).restrictScalars ℚ
theorem

numberFieldTowerAbstractFieldEquiv_algebraMap

L91 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerAbstractFieldEquiv_algebraMap
Documentation

The equivalences from the original number-field tower to its two abstract fixed fields commute with the tower algebra maps.

Source context 13 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] towerNormIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem numberFieldTowerAbstractFieldEquiv_algebraMap
    (x : K) :
    numberFieldTowerAbstractTopFieldEquiv K L
        (algebraMap K L x) =
      algebraMap
        (abstractFixedField ℚ (SeparableClosure ℚ)
          (numberFieldTowerBaseSubgroup K L))
        (abstractRelativeFixedField ℚ (SeparableClosure ℚ)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L))
        (numberFieldTowerAbstractBaseFieldEquiv K L x)
theorem

numberFieldTowerBaseSubgroup_absoluteQuotient_finite

L128 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerBaseSubgroup_absoluteQuotient_finite
Documentation

The compatible lower subgroup has finite absolute index in the rational absolute Galois group. This opaque theorem keeps consumers from unfolding the bundled finite-abstract-field witness.

Source context 13 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] towerNormIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem numberFieldTowerBaseSubgroup_absoluteQuotient_finite :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          (numberFieldTowerBaseSubgroup K L)
          (le_baseField (numberFieldTowerBaseSubgroup K L)))
instance

numberFieldTowerBaseSubgroupAbsoluteQuotientFinite

L143 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerBaseSubgroupAbsoluteQuotientFinite
Documentation

The absolute-index witness used by the tower realization, registered at its precise quotient type so downstream declarations need not normalize the bundled finite-abstract-field construction.

Source context 12 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] towerNormIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
instance
    numberFieldTowerBaseSubgroupAbsoluteQuotientFinite :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          (numberFieldTowerBaseSubgroup K L)
          (le_baseField (numberFieldTowerBaseSubgroup K L)))
instance

numberFieldTowerExtensionSubgroupNormal

L157 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerExtensionSubgroupNormal
Documentation

The normality witness for the tower realization, registered only at the specialized extension subgroup.

Source context 12 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] towerNormIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
instance
    numberFieldTowerExtensionSubgroupNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal
instance

numberFieldTowerExtensionQuotientFinite

L167 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerExtensionQuotientFinite
Documentation

The relative-index witness for the tower realization, registered only at the specialized quotient consumed by FiniteNormQuotient.

Source context 12 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] towerNormIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
instance
    numberFieldTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L))
theorem

towerNormAbstractBaseNumberField

L178 ↗
GlobalClassFieldTheory.Reciprocity.towerNormAbstractBaseNumberField
Source context 13 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] towerNormIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem towerNormAbstractBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L))
theorem

towerNormAbstractTopNumberField

L190 ↗
GlobalClassFieldTheory.Reciprocity.towerNormAbstractTopNumberField
Source context 14 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] towerNormIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
attribute [local instance] towerNormAbstractBaseNumberField
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem towerNormAbstractTopNumberField :
    NumberField
      (abstractRelativeFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerTopSubgroup_le_baseSubgroup K L))
def

towerNormAbstractNormQuotientCommGroup

L204 ↗
GlobalClassFieldTheory.Reciprocity.towerNormAbstractNormQuotientCommGroup
Documentation

The fixed tower uses one canonical quotient dictionary throughout its three comparison boundaries.

Source context 14 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] towerNormIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
attribute [local instance] towerNormAbstractBaseNumberField
attribute [local instance] towerNormAbstractTopNumberField
Lean source · statement
def towerNormAbstractNormQuotientCommGroup :
    CommGroup
      (IdeleClassGroup
          (abstractFixedField ℚ (SeparableClosure ℚ)
            (numberFieldTowerBaseSubgroup K L)) ⧸
        (_root_.ideleClassNorm
          (abstractFixedField ℚ (SeparableClosure ℚ)
            (numberFieldTowerBaseSubgroup K L))
          (abstractRelativeFixedField ℚ (SeparableClosure ℚ)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L))).range)
def

numberFieldTowerIdeleClassEquivAmbientFixed

L226 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerIdeleClassEquivAmbientFixed
Documentation

The ordinary idele class group of the original base field, transported to the fixed part of the rational absolute idele-class representation used by abstract reciprocity.

Source context 15 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] towerNormIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
attribute [local instance] towerNormAbstractBaseNumberField
attribute [local instance] towerNormAbstractTopNumberField
attribute [local instance] towerNormAbstractNormQuotientCommGroup
Lean source · statement
def numberFieldTowerIdeleClassEquivAmbientFixed :
    Additive (IdeleClassGroup K) ≃+
      KummerTheory.ambientFixedAddSubgroup
        rationalIdeleClassRepresentation
        (numberFieldTowerBaseSubgroup K L)
def

numberFieldTowerFixedFieldNormQuotient

L242 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFixedFieldNormQuotient
Documentation

The ordinary norm quotient of the two fixed fields, kept behind a small type boundary so the two comparison steps can be elaborated in separate declarations.

Source context 15 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] towerNormIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
attribute [local instance] towerNormAbstractBaseNumberField
attribute [local instance] towerNormAbstractTopNumberField
attribute [local instance] towerNormAbstractNormQuotientCommGroup
Lean source · statement
def numberFieldTowerFixedFieldNormQuotient : Type
instance

numberFieldTowerFixedFieldNormQuotientAddCommGroup

L253 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFixedFieldNormQuotientAddCommGroup
Source context 15 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] towerNormIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
attribute [local instance] towerNormAbstractBaseNumberField
attribute [local instance] towerNormAbstractTopNumberField
attribute [local instance] towerNormAbstractNormQuotientCommGroup
Lean source · statement
instance
    numberFieldTowerFixedFieldNormQuotientAddCommGroup :
    AddCommGroup (numberFieldTowerFixedFieldNormQuotient K L)
def

numberFieldTowerFiniteNormQuotientEquivFixedFieldNormQuotient

L268 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFiniteNormQuotientEquivFixedFieldNormQuotient
Documentation

First comparison step: abstract finite norms to the ordinary norm quotient of the realized fixed fields.

Source context 15 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] towerNormIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
attribute [local instance] towerNormAbstractBaseNumberField
attribute [local instance] towerNormAbstractTopNumberField
attribute [local instance] towerNormAbstractNormQuotientCommGroup
Lean source · statement
def
    numberFieldTowerFiniteNormQuotientEquivFixedFieldNormQuotient :
    FiniteNormQuotient rationalIdeleClassRepresentation
        (numberFieldTowerBaseSubgroup K L)
        (numberFieldTowerTopSubgroup L)
        (numberFieldTowerTopSubgroup_le_baseSubgroup K L) ≃+
      numberFieldTowerFixedFieldNormQuotient K L
def

numberFieldTowerFixedFieldNormQuotientEquivActualNormQuotient

L297 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFixedFieldNormQuotientEquivActualNormQuotient
Documentation

Second comparison step: transport the realized fixed-field norm quotient back to the original number-field tower.

Source context 15 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] towerNormIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
attribute [local instance] towerNormAbstractBaseNumberField
attribute [local instance] towerNormAbstractTopNumberField
attribute [local instance] towerNormAbstractNormQuotientCommGroup
Lean source · statement
def
    numberFieldTowerFixedFieldNormQuotientEquivActualNormQuotient :
    numberFieldTowerFixedFieldNormQuotient K L ≃+
      Additive
        (IdeleClassGroup K ⧸
          (_root_.ideleClassNorm K L).range)
def

numberFieldTowerFiniteNormQuotientEquivIdeleClassNormQuotient

L335 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFiniteNormQuotientEquivIdeleClassNormQuotient
Documentation

The abstract finite norm quotient attached to the compatible fixed-field realization of L / K is the ordinary idele-class norm quotient of the original extension.

Source context 15 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] towerNormIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
attribute [local instance] towerNormAbstractBaseNumberField
attribute [local instance] towerNormAbstractTopNumberField
attribute [local instance] towerNormAbstractNormQuotientCommGroup
Lean source · statement
def
    numberFieldTowerFiniteNormQuotientEquivIdeleClassNormQuotient :
    FiniteNormQuotient rationalIdeleClassRepresentation
        (numberFieldTowerBaseSubgroup K L)
        (numberFieldTowerTopSubgroup L)
        (numberFieldTowerTopSubgroup_le_baseSubgroup K L) ≃+
      Additive
        (IdeleClassGroup K ⧸
          (_root_.ideleClassNorm K L).range)

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