NYLL
Module

FiniteGaloisRealization.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.FiniteGaloisRealization
24 declarations indexed from sourceView source ↗

Module documentation

Reciprocity for a realized finite Galois number-field tower

This module equips the compatible fixed-field realization of L / K with the finite-dimensional and number-field instances needed by global class formation, then transports abstract reciprocity back to the original tower.

Imports3
Imported by3

Declarations

def

realizedTowerIdeleClassCommGroup

L36 ↗
GlobalClassFieldTheory.Reciprocity.realizedTowerIdeleClassCommGroup
Documentation

Fix the canonical class-group structure before forming norm quotients.

Source context 9 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 AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
Lean source · statement
def realizedTowerIdeleClassCommGroup
    (F : Type) [Field F] [NumberField F] :
    CommGroup (IdeleClassGroup F)
theorem

realizedTowerIdeleClassIsMulCommutative

L43 ↗
GlobalClassFieldTheory.Reciprocity.realizedTowerIdeleClassIsMulCommutative
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 AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] realizedTowerIdeleClassCommGroup
Lean source · statement
theorem realizedTowerIdeleClassIsMulCommutative
    (F : Type) [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)
theorem

numberFieldTowerAbstractBaseFiniteDimensional

L56 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerAbstractBaseFiniteDimensional
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 AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] realizedTowerIdeleClassCommGroup
attribute [local instance] realizedTowerIdeleClassIsMulCommutative
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 numberFieldTowerAbstractBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L))
theorem

numberFieldTowerAbstractRelativeFiniteDimensional

L65 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerAbstractRelativeFiniteDimensional
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 AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] realizedTowerIdeleClassCommGroup
attribute [local instance] realizedTowerIdeleClassIsMulCommutative
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem numberFieldTowerAbstractRelativeFiniteDimensional :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L))
      (abstractRelativeFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerTopSubgroup_le_baseSubgroup K L))
theorem

numberFieldTowerAbstractScalarTower

L80 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerAbstractScalarTower
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 AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] realizedTowerIdeleClassCommGroup
attribute [local instance] realizedTowerIdeleClassIsMulCommutative
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 numberFieldTowerAbstractScalarTower :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L))
      (abstractRelativeFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerTopSubgroup_le_baseSubgroup K L))
theorem

numberFieldTowerAbstractTopFiniteDimensional

L88 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerAbstractTopFiniteDimensional
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 AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] realizedTowerIdeleClassCommGroup
attribute [local instance] realizedTowerIdeleClassIsMulCommutative
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem numberFieldTowerAbstractTopFiniteDimensional :
    FiniteDimensional ℚ
      (abstractRelativeFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerTopSubgroup_le_baseSubgroup K L))
theorem

numberFieldTowerAbstractBaseNumberField

L102 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerAbstractBaseNumberField
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 AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] realizedTowerIdeleClassCommGroup
attribute [local instance] realizedTowerIdeleClassIsMulCommutative
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 numberFieldTowerAbstractBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L))
theorem

numberFieldTowerAbstractTopNumberField

L109 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerAbstractTopNumberField
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 AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] realizedTowerIdeleClassCommGroup
attribute [local instance] realizedTowerIdeleClassIsMulCommutative
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem numberFieldTowerAbstractTopNumberField :
    NumberField
      (abstractRelativeFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerTopSubgroup_le_baseSubgroup K L))
theorem

numberFieldTowerRestrictedTopFiniteDimensional

L116 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerRestrictedTopFiniteDimensional
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 AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] realizedTowerIdeleClassCommGroup
attribute [local instance] realizedTowerIdeleClassIsMulCommutative
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem numberFieldTowerRestrictedTopFiniteDimensional :
    FiniteDimensional ℚ
      ((abstractRelativeFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).restrictScalars ℚ)
theorem

numberFieldTowerRestrictedTopNumberField

L129 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerRestrictedTopNumberField
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 AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] realizedTowerIdeleClassCommGroup
attribute [local instance] realizedTowerIdeleClassIsMulCommutative
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem numberFieldTowerRestrictedTopNumberField :
    NumberField
      ((abstractRelativeFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).restrictScalars ℚ)
def

numberFieldTowerRestrictedTopAlgebra

L136 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerRestrictedTopAlgebra
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 AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] realizedTowerIdeleClassCommGroup
attribute [local instance] realizedTowerIdeleClassIsMulCommutative
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 numberFieldTowerRestrictedTopAlgebra :
    Algebra
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L))
      ((abstractRelativeFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).restrictScalars ℚ)
theorem

numberFieldTowerAbstractRelativeIsGalois

L146 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerAbstractRelativeIsGalois
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 AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] realizedTowerIdeleClassCommGroup
attribute [local instance] realizedTowerIdeleClassIsMulCommutative
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem numberFieldTowerAbstractRelativeIsGalois :
    IsGalois
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L))
      (abstractRelativeFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerTopSubgroup_le_baseSubgroup K L))
theorem

ordinaryIdeleClassNormQuotientCongrOfAlgEquiv_symm_mk

L159 ↗
GlobalClassFieldTheory.Reciprocity.ordinaryIdeleClassNormQuotientCongrOfAlgEquiv_symm_mk
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 AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] realizedTowerIdeleClassCommGroup
attribute [local instance] realizedTowerIdeleClassIsMulCommutative
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem ordinaryIdeleClassNormQuotientCongrOfAlgEquiv_symm_mk
    {K₀ L₀ K₁ L₁ : Type}
    [Field K₀] [NumberField K₀]
    [Field L₀] [NumberField L₀] [Algebra K₀ L₀]
    [Field K₁] [NumberField K₁]
    [Field L₁] [NumberField L₁] [Algebra K₁ L₁]
    (eK : K₀ ≃ₐ[ℚ] K₁)
    (eL : L₀ ≃ₐ[ℚ] L₁)
    (h : ∀ x : K₀,
      eL (algebraMap K₀ L₀ x) =
        algebraMap K₁ L₁ (eK x))
    (c : IdeleClassGroup K₁) :
    (ordinaryIdeleClassNormQuotientCongrOfAlgEquiv eK eL h).symm
        (QuotientGroup.mk'
          (_root_.ideleClassNorm K₁ L₁).range c) =
      QuotientGroup.mk'
        (_root_.ideleClassNorm K₀ L₀).range
        ((ideleClassCongr eK).symm c)
def

numberFieldTowerFiniteNormClassPublicValue

L183 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFiniteNormClassPublicValue
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 AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] realizedTowerIdeleClassCommGroup
attribute [local instance] realizedTowerIdeleClassIsMulCommutative
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 numberFieldTowerFiniteNormClassPublicValue
    (a : KummerTheory.ambientFixedAddSubgroup
      rationalIdeleClassRepresentation
      (numberFieldTowerBaseSubgroup K L)) :
    Additive
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range)
def

numberFieldTowerFiniteNormClassExpectedValue

L196 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFiniteNormClassExpectedValue
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 AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] realizedTowerIdeleClassCommGroup
attribute [local instance] realizedTowerIdeleClassIsMulCommutative
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 numberFieldTowerFiniteNormClassExpectedValue
    (a : KummerTheory.ambientFixedAddSubgroup
      rationalIdeleClassRepresentation
      (numberFieldTowerBaseSubgroup K L)) :
    Additive
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range)
def

numberFieldTowerFiniteNormClassDirectComparisonValue

L209 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFiniteNormClassDirectComparisonValue
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 AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] realizedTowerIdeleClassCommGroup
attribute [local instance] realizedTowerIdeleClassIsMulCommutative
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 numberFieldTowerFiniteNormClassDirectComparisonValue
    (a : KummerTheory.ambientFixedAddSubgroup
      rationalIdeleClassRepresentation
      (numberFieldTowerBaseSubgroup K L)) :
    Additive
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range)
theorem

numberFieldTowerFiniteNormClassPublicValue_eq_directComparison

L244 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFiniteNormClassPublicValue_eq_directComparison
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 AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] realizedTowerIdeleClassCommGroup
attribute [local instance] realizedTowerIdeleClassIsMulCommutative
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem numberFieldTowerFiniteNormClassPublicValue_eq_directComparison
    (a : KummerTheory.ambientFixedAddSubgroup
      rationalIdeleClassRepresentation
      (numberFieldTowerBaseSubgroup K L)) :
    numberFieldTowerFiniteNormClassPublicValue K L a =
      numberFieldTowerFiniteNormClassDirectComparisonValue K L a
def

numberFieldTowerActualNormClassRepresentativeValue

L255 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerActualNormClassRepresentativeValue
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 AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] realizedTowerIdeleClassCommGroup
attribute [local instance] realizedTowerIdeleClassIsMulCommutative
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 numberFieldTowerActualNormClassRepresentativeValue
    (a : KummerTheory.ambientFixedAddSubgroup
      rationalIdeleClassRepresentation
      (numberFieldTowerBaseSubgroup K L)) :
    Additive
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range)
theorem

numberFieldTowerFiniteNormClassDirectComparison_eq_actualValue

L288 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFiniteNormClassDirectComparison_eq_actualValue
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 AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] realizedTowerIdeleClassCommGroup
attribute [local instance] realizedTowerIdeleClassIsMulCommutative
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem numberFieldTowerFiniteNormClassDirectComparison_eq_actualValue
    (a : KummerTheory.ambientFixedAddSubgroup
      rationalIdeleClassRepresentation
      (numberFieldTowerBaseSubgroup K L)) :
    numberFieldTowerFiniteNormClassDirectComparisonValue K L a =
      numberFieldTowerActualNormClassRepresentativeValue K L a
theorem

numberFieldTowerActualNormClassRepresentativeValue_eq_expected

L338 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerActualNormClassRepresentativeValue_eq_expected
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 AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] realizedTowerIdeleClassCommGroup
attribute [local instance] realizedTowerIdeleClassIsMulCommutative
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem numberFieldTowerActualNormClassRepresentativeValue_eq_expected
    (a : KummerTheory.ambientFixedAddSubgroup
      rationalIdeleClassRepresentation
      (numberFieldTowerBaseSubgroup K L)) :
    numberFieldTowerActualNormClassRepresentativeValue K L a =
      numberFieldTowerFiniteNormClassExpectedValue K L a
theorem

numberFieldTowerFiniteNormQuotientEquivIdeleClassNormQuotient_finiteNormClass

L384 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFiniteNormQuotientEquivIdeleClassNormQuotient_finiteNormClass
Documentation

On a finite norm-class representative, the comparison with the original number-field tower is the ordinary class map applied after transporting the fixed-field idele class back to K.

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 AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] realizedTowerIdeleClassCommGroup
attribute [local instance] realizedTowerIdeleClassIsMulCommutative
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem
    numberFieldTowerFiniteNormQuotientEquivIdeleClassNormQuotient_finiteNormClass
    (a : KummerTheory.ambientFixedAddSubgroup
      rationalIdeleClassRepresentation
      (numberFieldTowerBaseSubgroup K L)) :
    numberFieldTowerFiniteNormQuotientEquivIdeleClassNormQuotient K L
        (finiteNormClass rationalIdeleClassRepresentation
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L) a) =
      Additive.ofMul
        (QuotientGroup.mk'
          (_root_.ideleClassNorm K L).range
          (Additive.toMul
            ((numberFieldTowerIdeleClassEquivAmbientFixed K L).symm
              a)))
theorem

numberFieldTowerFiniteNormQuotientEquivIdeleClassNormQuotient_ideleClass

L414 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFiniteNormQuotientEquivIdeleClassNormQuotient_ideleClass
Documentation

On an idele class of the original base field, the fixed-part realization followed by the abstract finite norm-class map is exactly the genuine quotient class modulo the ordinary idele-class norm.

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 AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] realizedTowerIdeleClassCommGroup
attribute [local instance] realizedTowerIdeleClassIsMulCommutative
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem
    numberFieldTowerFiniteNormQuotientEquivIdeleClassNormQuotient_ideleClass
    (c : IdeleClassGroup K) :
    numberFieldTowerFiniteNormQuotientEquivIdeleClassNormQuotient K L
        (finiteNormClass rationalIdeleClassRepresentation
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)
          (numberFieldTowerIdeleClassEquivAmbientFixed K L
            (Additive.ofMul c))) =
      Additive.ofMul
        (QuotientGroup.mk'
          (_root_.ideleClassNorm K L).range c)
theorem

map_numberFieldTowerFiniteNormSubgroup_eq_ordinaryIdeleClassNormRange

L438 ↗
GlobalClassFieldTheory.Reciprocity.map_numberFieldTowerFiniteNormSubgroup_eq_ordinaryIdeleClassNormRange
Documentation

Under the compatible rational-separable-closure realization of a finite Galois number-field extension, the abstract finite norm subgroup is exactly the ordinary idele-class norm subgroup of the original extension.

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 AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] realizedTowerIdeleClassCommGroup
attribute [local instance] realizedTowerIdeleClassIsMulCommutative
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · full declaration
theorem
    map_numberFieldTowerFiniteNormSubgroup_eq_ordinaryIdeleClassNormRange :
    letI := (numberFieldTowerFiniteAbstractField K L).finite
    letI := numberFieldTowerExtensionSubgroup_normal K L
    letI := numberFieldTowerExtensionQuotient_finite K L
    (finiteNormSubgroup rationalIdeleClassRepresentation
        (numberFieldTowerBaseSubgroup K L)
        (numberFieldTowerTopSubgroup L)
        (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).map
        (numberFieldTowerIdeleClassEquivAmbientFixed
          K L).symm.toAddMonoidHom =
      (_root_.ideleClassNorm K L).range.toAddSubgroup := by
  let E :=
    numberFieldTowerIdeleClassEquivAmbientFixed K L
  let Q :=
    numberFieldTowerFiniteNormQuotientEquivIdeleClassNormQuotient
      K L
  ext c
  constructor
  · rintro ⟨a, ha, rfl⟩
    have haZero :
        finiteNormClass rationalIdeleClassRepresentation
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L) a =
          0 :=
      (finiteNormClass_eq_zero_iff
        rationalIdeleClassRepresentation
        (numberFieldTowerBaseSubgroup K L)
        (numberFieldTowerTopSubgroup L)
        (numberFieldTowerTopSubgroup_le_baseSubgroup K L) a).2 ha
    have hclass :=
      numberFieldTowerFiniteNormQuotientEquivIdeleClassNormQuotient_ideleClass
        K L (Additive.toMul (E.symm a))
    have hmk :
        QuotientGroup.mk'
            (_root_.ideleClassNorm K L).range
            (Additive.toMul (E.symm a)) =
          1 := by
      have hzero :
          (0 : Additive
            (IdeleClassGroup K ⧸
              (_root_.ideleClassNorm K L).range)) =
            Additive.ofMul
              (QuotientGroup.mk'
                (_root_.ideleClassNorm K L).range
                (Additive.toMul (E.symm a))) := by
        simpa only [E, ofMul_toMul,
          AddEquiv.apply_symm_apply, haZero, map_zero] using hclass
      exact congrArg Additive.toMul hzero.symm
    exact
      (QuotientGroup.eq_one_iff
        (Additive.toMul (E.symm a))).1 hmk
  · intro hc
    refine ⟨E c, ?_, E.symm_apply_apply c⟩
    apply
      (finiteNormClass_eq_zero_iff
        rationalIdeleClassRepresentation
        (numberFieldTowerBaseSubgroup K L)
        (numberFieldTowerTopSubgroup L)
        (numberFieldTowerTopSubgroup_le_baseSubgroup K L)
        (E c)).1
    apply Q.injective
    have hmk :
        QuotientGroup.mk'
            (_root_.ideleClassNorm K L).range
            (Additive.toMul c) =
          1 :=
      (QuotientGroup.eq_one_iff
        (Additive.toMul c)).2 hc
    have hclass :=
      numberFieldTowerFiniteNormQuotientEquivIdeleClassNormQuotient_ideleClass
        K L (Additive.toMul c)
    simpa only [E, ofMul_toMul,
      hmk, ofMul_one, map_zero] using hclass
theorem

numberFieldTowerTransport_isNormOpen_of_normRange_le

L517 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerTransport_isNormOpen_of_normRange_le
Documentation

If an ordinary subgroup contains the norm subgroup of a finite Galois number-field extension, then its transport to the compatible rational absolute fixed part is open for the genuine norm topology.

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 AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
attribute [local instance] realizedTowerIdeleClassCommGroup
attribute [local instance] realizedTowerIdeleClassIsMulCommutative
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · full declaration
theorem numberFieldTowerTransport_isNormOpen_of_normRange_le
    (H : Subgroup (IdeleClassGroup K))
    (hLH : (_root_.ideleClassNorm K L).range ≤ H) :
    letI := (numberFieldTowerFiniteAbstractField K L).finite
    IsNormOpen rationalIdeleClassRepresentation
      (numberFieldTowerBaseSubgroup K L)
      ((H.toAddSubgroup).map
        (numberFieldTowerIdeleClassEquivAmbientFixed
          K L).toAddMonoidHom :
        AddSubgroup
          (KummerTheory.ambientFixedAddSubgroup
            rationalIdeleClassRepresentation
            (numberFieldTowerBaseSubgroup K L))) := by
  let E :=
    numberFieldTowerIdeleClassEquivAmbientFixed K L
  rw [normTopology_addSubgroup_isOpen_iff]
  refine
    ⟨numberFieldTowerFiniteGaloisSubextension K L, ?_⟩
  intro a ha
  have hback :
      E.symm a ∈
        (finiteNormSubgroup rationalIdeleClassRepresentation
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).map
            E.symm.toAddMonoidHom :=
    ⟨a, ha, rfl⟩
  have hnorm :
      Additive.toMul (E.symm a) ∈
        (_root_.ideleClassNorm K L).range := by
    rw [
      map_numberFieldTowerFiniteNormSubgroup_eq_ordinaryIdeleClassNormRange
        K L] at hback
    exact hback
  exact
    ⟨E.symm a, hLH hnorm, E.apply_symm_apply a⟩

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