NYLL
Module

CyclotomicIdeleClassValuation.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.CyclotomicIdeleClassValuation
60 declarations indexed from sourceView source ↗

Module documentation

The cyclotomic valuation on idele classes

The cyclotomic idele value is trivial on principal ideles, so it descends to the ordinary idele class group. Its restriction to the compact norm-one idele class group still has dense image in ZHat; compactness therefore upgrades density to surjectivity.

For a number field K, the defining normalization gives the exact identity

f_K v_K(c) = v_ℚ(N_{K/ℚ} c).

Surjectivity of v_K then identifies the image of the actual idele-class norm with f_K ZHat. For the actual fixed field attached to a finite abstract field, the already constructed cyclotomic base-change theorem identifies f_K with the residue degree. This supplies the norm-range field of the concrete henselian valuation data.

Imports7
Imported by7

Declarations

def

cyclotomicValuationIdeleClassCommGroup

L50 ↗
GlobalClassFieldTheory.Reciprocity.cyclotomicValuationIdeleClassCommGroup
Documentation

Fix the canonical source-group dictionary before constructing the value maps and their additive ranges.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
Lean source · statement
def cyclotomicValuationIdeleClassCommGroup
    (F : Type) [Field F] [NumberField F] :
    CommGroup (IdeleClassGroup F)
def

ideleClassContinuousQuotientLift

L61 ↗
GlobalClassFieldTheory.Reciprocity.ideleClassContinuousQuotientLift
Documentation

Lift a continuous multiplicative map through a quotient group once its defining normal subgroup is contained in the kernel. Keeping the quotient-map argument here avoids repeating the same large continuity elaboration for the rational and number-field cyclotomic values.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
Lean source · statement
def ideleClassContinuousQuotientLift
    {A B : Type*} [Group A] [TopologicalSpace A]
    [Group B] [TopologicalSpace B]
    (N : Subgroup A) [N.Normal] (f : A →ₜ* B)
    (hN : N ≤ f.toMonoidHom.ker) : (A ⧸ N) →ₜ* B
theorem

ideleClassContinuousQuotientLift_mk

L79 ↗
GlobalClassFieldTheory.Reciprocity.ideleClassContinuousQuotientLift_mk
Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
Lean source · statement
theorem ideleClassContinuousQuotientLift_mk
    {A B : Type*} [Group A] [TopologicalSpace A]
    [Group B] [TopologicalSpace B]
    (N : Subgroup A) [N.Normal] (f : A →ₜ* B)
    (hN : N ≤ f.toMonoidHom.ker) (a : A) :
    ideleClassContinuousQuotientLift N f hN
        (QuotientGroup.mk' N a) =
      f a
theorem

rationalCyclotomicZHatIdeleValue_principalSubgroup_le_ker

L92 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatIdeleValue_principalSubgroup_le_ker
Documentation

Principal rational ideles lie in the kernel of the cyclotomic value.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
Lean source · statement
theorem rationalCyclotomicZHatIdeleValue_principalSubgroup_le_ker :
    IdeleGroup.principalSubgroup ℚ ≤
      rationalCyclotomicZHatIdeleValue.toMonoidHom.ker
def

rationalCyclotomicZHatIdeleClassValueContinuousMul

L100 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatIdeleClassValueContinuousMul
Documentation

The rational cyclotomic value descended continuously through C_ℚ = I_ℚ / ℚˣ.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
Lean source · statement
def rationalCyclotomicZHatIdeleClassValueContinuousMul :
    IdeleClassGroup ℚ →ₜ* Multiplicative ZHat
theorem

rationalCyclotomicZHatIdeleClassValueContinuousMul_mk

L110 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatIdeleClassValueContinuousMul_mk
Documentation

Evaluation of the descended rational value on an idele class represented by an idele.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
Lean source · statement
theorem rationalCyclotomicZHatIdeleClassValueContinuousMul_mk
    (a : IdeleGroup ℚ) :
    rationalCyclotomicZHatIdeleClassValueContinuousMul
        (QuotientGroup.mk'
          (IdeleGroup.principalSubgroup ℚ) a) =
      rationalCyclotomicZHatIdeleValue a
def

rationalCyclotomicZHatIdeleClassValueContinuous

L123 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatIdeleClassValueContinuous
Documentation

The rational cyclotomic value on idele classes, in continuous additive notation.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
Lean source · full declaration
def rationalCyclotomicZHatIdeleClassValueContinuous :
    Additive (IdeleClassGroup ℚ) →ₜ+ ZHat where
  __ := MonoidHom.toAdditiveLeft
    rationalCyclotomicZHatIdeleClassValueContinuousMul.toMonoidHom
  continuous_toFun := continuous_toAdd.comp
    (rationalCyclotomicZHatIdeleClassValueContinuousMul.continuous_toFun.comp
      continuous_toMul)
theorem

rationalCyclotomicZHatIdeleClassValueContinuous_mk

L133 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatIdeleClassValueContinuous_mk
Documentation

Evaluation of the additive rational class value on a representative.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
Lean source · statement
theorem rationalCyclotomicZHatIdeleClassValueContinuous_mk
    (a : IdeleGroup ℚ) :
    rationalCyclotomicZHatIdeleClassValueContinuous
        (Additive.ofMul
          (QuotientGroup.mk'
            (IdeleGroup.principalSubgroup ℚ) a)) =
      Multiplicative.toAdd
        (rationalCyclotomicZHatIdeleValue a)
theorem

normalizedCyclotomicZHatIdeleValue_principalSubgroup_le_ker

L153 ↗
GlobalClassFieldTheory.Reciprocity.normalizedCyclotomicZHatIdeleValue_principalSubgroup_le_ker
Documentation

Principal ideles lie in the kernel of the normalized cyclotomic value.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem
    normalizedCyclotomicZHatIdeleValue_principalSubgroup_le_ker :
    IdeleGroup.principalSubgroup K ≤
      (normalizedCyclotomicZHatIdeleValueContinuousMul K).toMonoidHom.ker
def

normalizedCyclotomicZHatIdeleClassValueContinuousMul

L166 ↗
GlobalClassFieldTheory.Reciprocity.normalizedCyclotomicZHatIdeleClassValueContinuousMul
Documentation

The normalized cyclotomic value descended continuously through C_K = I_K / Kˣ.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
def normalizedCyclotomicZHatIdeleClassValueContinuousMul :
    IdeleClassGroup K →ₜ* Multiplicative ZHat
theorem

normalizedCyclotomicZHatIdeleClassValueContinuousMul_mk

L175 ↗
GlobalClassFieldTheory.Reciprocity.normalizedCyclotomicZHatIdeleClassValueContinuousMul_mk
Documentation

Evaluation of the normalized class value on an idele representative.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem normalizedCyclotomicZHatIdeleClassValueContinuousMul_mk
    (a : IdeleGroup K) :
    normalizedCyclotomicZHatIdeleClassValueContinuousMul K
        (QuotientGroup.mk'
          (IdeleGroup.principalSubgroup K) a) =
      Multiplicative.ofAdd
        (normalizedCyclotomicZHatIdeleValue K
          (Additive.ofMul a))
def

normalizedCyclotomicZHatIdeleClassValueContinuous

L191 ↗
GlobalClassFieldTheory.Reciprocity.normalizedCyclotomicZHatIdeleClassValueContinuous
Documentation

The normalized cyclotomic value on idele classes, in continuous additive notation.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
Lean source · full declaration
def normalizedCyclotomicZHatIdeleClassValueContinuous :
    Additive (IdeleClassGroup K) →ₜ+ ZHat where
  __ := MonoidHom.toAdditiveLeft
    (normalizedCyclotomicZHatIdeleClassValueContinuousMul K).toMonoidHom
  continuous_toFun := continuous_toAdd.comp
    ((normalizedCyclotomicZHatIdeleClassValueContinuousMul K).continuous_toFun.comp
      continuous_toMul)
theorem

normalizedCyclotomicZHatIdeleClassValueContinuous_mk

L201 ↗
GlobalClassFieldTheory.Reciprocity.normalizedCyclotomicZHatIdeleClassValueContinuous_mk
Documentation

Evaluation of the normalized additive class value on a representative.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem normalizedCyclotomicZHatIdeleClassValueContinuous_mk
    (a : IdeleGroup K) :
    normalizedCyclotomicZHatIdeleClassValueContinuous K
        (Additive.ofMul
          (QuotientGroup.mk'
            (IdeleGroup.principalSubgroup K) a)) =
      normalizedCyclotomicZHatIdeleValue K
        (Additive.ofMul a)
theorem

infiniteGlobalArtinMonoidHom_numberFieldCyclotomicZHatCompositum_principalIdele

L227 ↗
GlobalClassFieldTheory.Reciprocity.infiniteGlobalArtinMonoidHom_numberFieldCyclotomicZHatCompositum_principalIdele
Documentation

The chosen local-factor product on the actual cyclotomic ZHat-compositum kills every principal idele. This is the number-field form of the cyclotomic principal-idele formula: after restricting to the rational cyclotomic factor, norm--restriction turns the assertion into the rational principal-idele product formula, and that restriction is injective.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem
    infiniteGlobalArtinMonoidHom_numberFieldCyclotomicZHatCompositum_principalIdele
    (x : Kˣ) :
    infiniteGlobalArtinMonoidHom K
        (numberFieldCyclotomicZHatCompositum K)
        (IdeleGroup.principalIdele K x) =
      1
def

numberFieldCyclotomicZHatCompositumIdeleClassArtinMonoidHom

L247 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldCyclotomicZHatCompositumIdeleClassArtinMonoidHom
Documentation

The genuine infinite Artin map of the cyclotomic ZHat-compositum, descended to the idele class group.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
def
    numberFieldCyclotomicZHatCompositumIdeleClassArtinMonoidHom :
    IdeleClassGroup K →*
      Gal(numberFieldCyclotomicZHatCompositum K / K)
theorem

numberFieldCyclotomicZHatCompositumIdeleClassArtinMonoidHom_mk

L264 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldCyclotomicZHatCompositumIdeleClassArtinMonoidHom_mk
Documentation

Evaluation of the descended compositum Artin map on an idele representative.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem
    numberFieldCyclotomicZHatCompositumIdeleClassArtinMonoidHom_mk
    (a : IdeleGroup K) :
    numberFieldCyclotomicZHatCompositumIdeleClassArtinMonoidHom K
        (QuotientGroup.mk'
          (IdeleGroup.principalSubgroup K) a) =
      infiniteGlobalArtinMonoidHom K
        (numberFieldCyclotomicZHatCompositum K) a
theorem

numberFieldCyclotomicZHatCompositumIdeleClassArtin_coordinate

L278 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldCyclotomicZHatCompositumIdeleClassArtin_coordinate
Documentation

In the rational cyclotomic Galois coordinate, the genuine idele-class Artin symbol over K is exactly f_K times the normalized cyclotomic valuation.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem
    numberFieldCyclotomicZHatCompositumIdeleClassArtin_coordinate
    (c : IdeleClassGroup K) :
    Multiplicative.toAdd
        (rationalCyclotomicZHatFieldGalEquivZHat
          (numberFieldCyclotomicZHatCompositumRestriction K
            (numberFieldCyclotomicZHatCompositumIdeleClassArtinMonoidHom
              K c))) =
      cyclotomicZHatIntersectionDegree K •
        normalizedCyclotomicZHatIdeleClassValueContinuous K
          (Additive.ofMul c)
theorem

numberFieldCyclotomicZHatCompositumIdeleClassArtin_eq_one_iff

L308 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldCyclotomicZHatCompositumIdeleClassArtin_eq_one_iff
Documentation

The kernel of the genuine Artin map to the cyclotomic ZHat-compositum is the zero fibre of the normalized cyclotomic idele-class valuation.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem
    numberFieldCyclotomicZHatCompositumIdeleClassArtin_eq_one_iff
    (c : IdeleClassGroup K) :
    numberFieldCyclotomicZHatCompositumIdeleClassArtinMonoidHom K c =
        1 ↔
      normalizedCyclotomicZHatIdeleClassValueContinuous K
          (Additive.ofMul c) =
        0
instance

cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra

L348 ↗
GlobalClassFieldTheory.Reciprocity.cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra
Documentation

Use the rational algebra structure expected by the imported finite-layer API throughout this block. Fixing it before the first finite-layer binder keeps the parameter and every restriction target definitionally aligned.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField
theorem

numberFieldCyclotomicZHatFiniteLayerNumberField

L356 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldCyclotomicZHatFiniteLayerNumberField
Documentation

The canonical number-field structure used by every finite-layer idele-class declaration below. Keeping this witness opaque prevents the module-finiteness construction from being rebuilt along distinct paths.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
Lean source · statement
theorem
    numberFieldCyclotomicZHatFiniteLayerNumberField
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    NumberField
      (numberFieldCyclotomicZHatFiniteLayerInCompositum K E)
structure

NumberFieldCyclotomicZHatFiniteLayerArtinData

L369 ↗
GlobalClassFieldTheory.Reciprocity.NumberFieldCyclotomicZHatFiniteLayerArtinData
Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · full declaration
structure NumberFieldCyclotomicZHatFiniteLayerArtinData
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    Type where
  toMonoidHom :
    IdeleGroup K →*
      Gal(numberFieldCyclotomicZHatFiniteLayerInCompositum K E / K)
  principal (x : Kˣ) :
    toMonoidHom (IdeleGroup.principalIdele K x) = 1
  restriction (a : IdeleGroup K) :
    AlgEquiv.restrictNormalHom
        (numberFieldCyclotomicZHatFiniteLayerInCompositum K E)
        (infiniteGlobalArtinMonoidHom K
          (numberFieldCyclotomicZHatCompositum K) a) =
      toMonoidHom a
theorem

rawGlobalArtinMonoidHom_numberFieldCyclotomicZHatFiniteLayer_principalIdele

L386 ↗
GlobalClassFieldTheory.Reciprocity.rawGlobalArtinMonoidHom_numberFieldCyclotomicZHatFiniteLayer_principalIdele
Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · statement
theorem
    rawGlobalArtinMonoidHom_numberFieldCyclotomicZHatFiniteLayer_principalIdele
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField)
    (x : Kˣ) :
    globalArtinMonoidHom
        (K := K)
        (L :=
          numberFieldCyclotomicZHatFiniteLayerInCompositum K E)
        (IdeleGroup.principalIdele K x) =
      1
theorem

rawGlobalArtinMonoidHom_numberFieldCyclotomicZHatFiniteLayer_restriction

L433 ↗
GlobalClassFieldTheory.Reciprocity.rawGlobalArtinMonoidHom_numberFieldCyclotomicZHatFiniteLayer_restriction
Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · statement
theorem
    rawGlobalArtinMonoidHom_numberFieldCyclotomicZHatFiniteLayer_restriction
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField)
    (a : IdeleGroup K) :
    AlgEquiv.restrictNormalHom
        (numberFieldCyclotomicZHatFiniteLayerInCompositum K E)
        (infiniteGlobalArtinMonoidHom K
          (numberFieldCyclotomicZHatCompositum K) a) =
      globalArtinMonoidHom
        (K := K)
        (L :=
          numberFieldCyclotomicZHatFiniteLayerInCompositum K E) a
def

numberFieldCyclotomicZHatFiniteLayerArtinData

L451 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldCyclotomicZHatFiniteLayerArtinData
Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · full declaration
def
    numberFieldCyclotomicZHatFiniteLayerArtinData
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    NumberFieldCyclotomicZHatFiniteLayerArtinData K E where
  toMonoidHom :=
    globalArtinMonoidHom
      (K := K)
      (L := numberFieldCyclotomicZHatFiniteLayerInCompositum K E)
  principal :=
    rawGlobalArtinMonoidHom_numberFieldCyclotomicZHatFiniteLayer_principalIdele
      K E
  restriction :=
    rawGlobalArtinMonoidHom_numberFieldCyclotomicZHatFiniteLayer_restriction
      K E
def

numberFieldCyclotomicZHatFiniteLayerGlobalArtinMonoidHom

L470 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldCyclotomicZHatFiniteLayerGlobalArtinMonoidHom
Documentation

The chosen finite-layer global Artin map, kept opaque so every descended idele-class declaration shares the same dependent instance data.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · statement
def
    numberFieldCyclotomicZHatFiniteLayerGlobalArtinMonoidHom
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    IdeleGroup K →*
      Gal(numberFieldCyclotomicZHatFiniteLayerInCompositum K E / K)
theorem

globalArtinMonoidHom_numberFieldCyclotomicZHatFiniteLayer_principalIdele

L483 ↗
GlobalClassFieldTheory.Reciprocity.globalArtinMonoidHom_numberFieldCyclotomicZHatFiniteLayer_principalIdele
Documentation

Every finite cyclotomic layer over a number field inherits the principal-idele product formula from the full cyclotomic ZHat-compositum.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · statement
theorem
    globalArtinMonoidHom_numberFieldCyclotomicZHatFiniteLayer_principalIdele
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField)
    (x : Kˣ) :
    numberFieldCyclotomicZHatFiniteLayerGlobalArtinMonoidHom K E
        (IdeleGroup.principalIdele K x) =
      1
theorem

numberFieldCyclotomicZHatFiniteLayer_principalSubgroup_le_ker

L495 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldCyclotomicZHatFiniteLayer_principalSubgroup_le_ker
Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · statement
theorem
    numberFieldCyclotomicZHatFiniteLayer_principalSubgroup_le_ker
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    IdeleGroup.principalSubgroup K ≤
      (numberFieldCyclotomicZHatFiniteLayerGlobalArtinMonoidHom K E).ker
def

numberFieldCyclotomicZHatFiniteLayerIdeleClassArtinMonoidHom

L509 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldCyclotomicZHatFiniteLayerIdeleClassArtinMonoidHom
Documentation

The actual chosen-local-factor Artin map of a finite cyclotomic layer, descended through C_K = I_K / Kˣ.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · statement
def
    numberFieldCyclotomicZHatFiniteLayerIdeleClassArtinMonoidHom
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    IdeleClassGroup K →*
      Gal(numberFieldCyclotomicZHatFiniteLayerInCompositum K E / K)
theorem

numberFieldCyclotomicZHatFiniteLayerIdeleClassArtinMonoidHom_mk

L525 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldCyclotomicZHatFiniteLayerIdeleClassArtinMonoidHom_mk
Documentation

Evaluation of the descended finite-layer Artin map on an idele representative.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · statement
theorem
    numberFieldCyclotomicZHatFiniteLayerIdeleClassArtinMonoidHom_mk
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField)
    (a : IdeleGroup K) :
    numberFieldCyclotomicZHatFiniteLayerIdeleClassArtinMonoidHom K E
        (QuotientGroup.mk'
          (IdeleGroup.principalSubgroup K) a) =
      numberFieldCyclotomicZHatFiniteLayerGlobalArtinMonoidHom K E a
theorem

numberFieldCyclotomicZHatCompositumIdeleClassArtinMonoidHom_restrict

L545 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldCyclotomicZHatCompositumIdeleClassArtinMonoidHom_restrict
Documentation

Restriction of the descended Artin map of the full cyclotomic compositum to a finite cyclotomic layer is the descended finite-layer chosen-local-factor Artin map.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · statement
theorem
    numberFieldCyclotomicZHatCompositumIdeleClassArtinMonoidHom_restrict
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    (AlgEquiv.restrictNormalHom
        (numberFieldCyclotomicZHatFiniteLayerInCompositum K E)).comp
        (numberFieldCyclotomicZHatCompositumIdeleClassArtinMonoidHom K) =
      numberFieldCyclotomicZHatFiniteLayerIdeleClassArtinMonoidHom K E
theorem

rationalCyclotomicZHatIdeleClassValue_normOne_denseRange

L568 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatIdeleClassValue_normOne_denseRange
Documentation

The descended rational class value has dense image already on the compact norm-one idele class group.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · full declaration
theorem
    rationalCyclotomicZHatIdeleClassValue_normOne_denseRange :
    DenseRange
      (fun c : IdeleClassGroup.normOneSubgroup (K := ℚ) =>
        rationalCyclotomicZHatIdeleClassValueContinuous
          (Additive.ofMul (c : IdeleClassGroup ℚ))) := by
  have hToAdd :
      Function.Surjective
        (Multiplicative.toAdd :
          Multiplicative ZHat → ZHat) :=
    fun z => ⟨Multiplicative.ofAdd z, rfl⟩
  have hidele :
      DenseRange
        (fun b : IdeleGroup.normOneSubgroup (K := ℚ) =>
          Multiplicative.toAdd
            (rationalCyclotomicZHatIdeleValue
              (b : IdeleGroup ℚ))) :=
    hToAdd.denseRange.comp
      rationalCyclotomicZHatIdeleValue_normOne_denseRange
      continuous_toAdd
  apply hidele.mono
  rintro z ⟨b, rfl⟩
  let c : IdeleClassGroup.normOneSubgroup (K := ℚ) :=
    ⟨QuotientGroup.mk'
        (IdeleGroup.principalSubgroup ℚ)
        (b : IdeleGroup ℚ),
      (IdeleClassGroup.mk_mem_normOneSubgroup_iff
        (b : IdeleGroup ℚ)).2 b.2⟩
  refine ⟨c, ?_⟩
  simp only [c,
    rationalCyclotomicZHatIdeleClassValueContinuous_mk]
theorem

rationalCyclotomicZHatIdeleClassValue_normOne_surjective

L602 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatIdeleClassValue_normOne_surjective
Documentation

Compactness upgrades the dense rational norm-one image to surjectivity.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · full declaration
theorem
    rationalCyclotomicZHatIdeleClassValue_normOne_surjective :
    Function.Surjective
      (fun c : IdeleClassGroup.normOneSubgroup (K := ℚ) =>
        rationalCyclotomicZHatIdeleClassValueContinuous
          (Additive.ofMul (c : IdeleClassGroup ℚ))) := by
  let f :=
    fun c : IdeleClassGroup.normOneSubgroup (K := ℚ) =>
      rationalCyclotomicZHatIdeleClassValueContinuous
        (Additive.ofMul (c : IdeleClassGroup ℚ))
  have hf : Continuous f := by
    exact
      (rationalCyclotomicZHatIdeleClassValueContinuous.continuous_toFun).comp
        (continuous_ofMul.comp continuous_subtype_val)
  have hclosed : IsClosed (Set.range f) :=
    (isCompact_range hf).isClosed
  have hdense : DenseRange f := by
    simpa only [f] using
      rationalCyclotomicZHatIdeleClassValue_normOne_denseRange
  intro z
  have hz : z ∈ closure (Set.range f) := by
    rw [hdense.closure_range]
    trivial
  rwa [hclosed.closure_eq] at hz
theorem

rationalCyclotomicZHatIdeleClassValue_surjective

L628 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatIdeleClassValue_surjective
Documentation

The rational cyclotomic idele-class value is surjective.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · statement
theorem rationalCyclotomicZHatIdeleClassValue_surjective :
    Function.Surjective
      rationalCyclotomicZHatIdeleClassValueContinuous
theorem

normalizedCyclotomicZHatIdeleClassValue_normOne_denseRange

L638 ↗
GlobalClassFieldTheory.Reciprocity.normalizedCyclotomicZHatIdeleClassValue_normOne_denseRange
Documentation

The normalized class value has dense image already on the compact norm-one idele class group.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · full declaration
theorem normalizedCyclotomicZHatIdeleClassValue_normOne_denseRange :
    DenseRange
      (fun c : IdeleClassGroup.normOneSubgroup (K := K) =>
        normalizedCyclotomicZHatIdeleClassValueContinuous K
          (Additive.ofMul (c : IdeleClassGroup K))) := by
  apply
    (normalizedCyclotomicZHatIdeleValue_normOne_denseRange K).mono
  rintro z ⟨b, rfl⟩
  let c : IdeleClassGroup.normOneSubgroup (K := K) :=
    ⟨QuotientGroup.mk'
        (IdeleGroup.principalSubgroup K)
        (b : IdeleGroup K),
      (IdeleClassGroup.mk_mem_normOneSubgroup_iff
        (b : IdeleGroup K)).2 b.2⟩
  refine ⟨c, ?_⟩
  simp only [c,
    normalizedCyclotomicZHatIdeleClassValueContinuous_mk]
theorem

normalizedCyclotomicZHatIdeleClassValue_normOne_surjective

L658 ↗
GlobalClassFieldTheory.Reciprocity.normalizedCyclotomicZHatIdeleClassValue_normOne_surjective
Documentation

Compactness upgrades the dense normalized norm-one image to surjectivity.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · full declaration
theorem normalizedCyclotomicZHatIdeleClassValue_normOne_surjective :
    Function.Surjective
      (fun c : IdeleClassGroup.normOneSubgroup (K := K) =>
        normalizedCyclotomicZHatIdeleClassValueContinuous K
          (Additive.ofMul (c : IdeleClassGroup K))) := by
  let f :=
    fun c : IdeleClassGroup.normOneSubgroup (K := K) =>
      normalizedCyclotomicZHatIdeleClassValueContinuous K
        (Additive.ofMul (c : IdeleClassGroup K))
  have hf : Continuous f := by
    exact
      (normalizedCyclotomicZHatIdeleClassValueContinuous K).continuous_toFun.comp
        (continuous_ofMul.comp continuous_subtype_val)
  have hclosed : IsClosed (Set.range f) :=
    (isCompact_range hf).isClosed
  have hdense : Dense (Set.range f) := by
    change DenseRange f
    simpa only [f] using
      (normalizedCyclotomicZHatIdeleClassValue_normOne_denseRange K)
  intro z
  have hz : z ∈ closure (Set.range f) := by
    rw [hdense.closure_eq]
    trivial
  rwa [hclosed.closure_eq] at hz
theorem

normalizedCyclotomicZHatIdeleClassValue_surjective

L684 ↗
GlobalClassFieldTheory.Reciprocity.normalizedCyclotomicZHatIdeleClassValue_surjective
Documentation

The normalized cyclotomic idele-class value is surjective.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · statement
theorem normalizedCyclotomicZHatIdeleClassValue_surjective :
    Function.Surjective
      (normalizedCyclotomicZHatIdeleClassValueContinuous K)
theorem

normalizedCyclotomicZHatIdeleClassValue_range

L694 ↗
GlobalClassFieldTheory.Reciprocity.normalizedCyclotomicZHatIdeleClassValue_range
Documentation

The normalized cyclotomic class value has full value group.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · statement
theorem normalizedCyclotomicZHatIdeleClassValue_range :
    (normalizedCyclotomicZHatIdeleClassValueContinuous K).toAddMonoidHom.range =
      (⊤ : AddSubgroup ZHat)
theorem

rationalCyclotomicZHatIdeleClassValue_range

L703 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatIdeleClassValue_range
Documentation

The rational cyclotomic class value has full value group.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · statement
theorem rationalCyclotomicZHatIdeleClassValue_range :
    rationalCyclotomicZHatIdeleClassValueContinuous.toAddMonoidHom.range =
      (⊤ : AddSubgroup ZHat)
theorem

cyclotomicZHatIntersectionDegree_nsmul_normalizedIdeleClassValue

L714 ↗
GlobalClassFieldTheory.Reciprocity.cyclotomicZHatIntersectionDegree_nsmul_normalizedIdeleClassValue
Documentation

The defining normalized-value identity after descent to idele classes:

f_K v_K(c) = v_ℚ(N_{K/ℚ} c).

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · statement
theorem
    cyclotomicZHatIntersectionDegree_nsmul_normalizedIdeleClassValue
    (c : Additive (IdeleClassGroup K)) :
    cyclotomicZHatIntersectionDegree K •
        normalizedCyclotomicZHatIdeleClassValueContinuous K c =
      rationalCyclotomicZHatIdeleClassValueContinuous
        (Additive.ofMul
          (_root_.ideleClassNorm ℚ K
            (Additive.toMul c)))
def

rationalCyclotomicZHatIdeleClassNormComposite

L743 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatIdeleClassNormComposite
Documentation

The rational cyclotomic value after the actual class norm N_{K/ℚ} : C_K → C_ℚ.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · statement
def rationalCyclotomicZHatIdeleClassNormComposite :
    Additive (IdeleClassGroup K) →+ ZHat
theorem

rationalCyclotomicZHatIdeleClassNormComposite_apply

L750 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatIdeleClassNormComposite_apply
Documentation

Evaluation of the rational class-norm composite.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · statement
theorem rationalCyclotomicZHatIdeleClassNormComposite_apply
    (c : Additive (IdeleClassGroup K)) :
    rationalCyclotomicZHatIdeleClassNormComposite K c =
      rationalCyclotomicZHatIdeleClassValueContinuous
        (Additive.ofMul
          (_root_.ideleClassNorm ℚ K
            (Additive.toMul c)))
theorem

rationalCyclotomicZHatIdeleClassNormComposite_range

L761 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatIdeleClassNormComposite_range
Documentation

Exact image of the actual idele-class norm under the rational cyclotomic value.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · statement
theorem rationalCyclotomicZHatIdeleClassNormComposite_range :
    (rationalCyclotomicZHatIdeleClassNormComposite K).range =
      nsmulImage (⊤ : AddSubgroup ZHat)
        (cyclotomicZHatIntersectionDegree K)
def

normalizedCyclotomicZHatNormOneIdeleClassValue

L796 ↗
GlobalClassFieldTheory.Reciprocity.normalizedCyclotomicZHatNormOneIdeleClassValue
Documentation

Restriction of the normalized class value to the compact norm-one idele class group.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · statement
def normalizedCyclotomicZHatNormOneIdeleClassValue :
    Additive (IdeleClassGroup.normOneSubgroup (K := K)) →+ ZHat
theorem

normalizedCyclotomicZHatNormOneIdeleClassValue_surjective

L803 ↗
GlobalClassFieldTheory.Reciprocity.normalizedCyclotomicZHatNormOneIdeleClassValue_surjective
Documentation

The normalized norm-one class value remains surjective.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · statement
theorem normalizedCyclotomicZHatNormOneIdeleClassValue_surjective :
    Function.Surjective
      (normalizedCyclotomicZHatNormOneIdeleClassValue K)
def

rationalCyclotomicZHatNormOneIdeleClassNormComposite

L819 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatNormOneIdeleClassNormComposite
Documentation

The rational class value composed with the actual class norm, restricted to norm-one idele classes. The codomain restriction in normOneNorm is supplied by preservation of the absolute idele norm.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · statement
def rationalCyclotomicZHatNormOneIdeleClassNormComposite :
    Additive (IdeleClassGroup.normOneSubgroup (K := K)) →+ ZHat
theorem

cyclotomicZHatIntersectionDegree_nsmul_normalizedNormOneIdeleClassValue

L828 ↗
GlobalClassFieldTheory.Reciprocity.cyclotomicZHatIntersectionDegree_nsmul_normalizedNormOneIdeleClassValue
Documentation

The normalized identity restricted to the actual norm-one class norm.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · statement
theorem
    cyclotomicZHatIntersectionDegree_nsmul_normalizedNormOneIdeleClassValue
    (c : Additive
      (IdeleClassGroup.normOneSubgroup (K := K))) :
    cyclotomicZHatIntersectionDegree K •
        normalizedCyclotomicZHatNormOneIdeleClassValue K c =
      rationalCyclotomicZHatNormOneIdeleClassNormComposite K c
theorem

rationalCyclotomicZHatNormOneIdeleClassNormComposite_range

L859 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatNormOneIdeleClassNormComposite_range
Documentation

The exact cyclotomic image of the actual class norm is already attained on norm-one idele classes.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · statement
theorem
    rationalCyclotomicZHatNormOneIdeleClassNormComposite_range :
    (rationalCyclotomicZHatNormOneIdeleClassNormComposite K).range =
      nsmulImage (⊤ : AddSubgroup ZHat)
        (cyclotomicZHatIntersectionDegree K)
def

rationalCyclotomicZHatValuation

L893 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatValuation
Documentation

The rational cyclotomic class valuation transported to the distinguished base fixed part of the absolute idele-class representation.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · statement
def rationalCyclotomicZHatValuation :
    KummerTheory.ambientFixedAddSubgroup
        rationalIdeleClassRepresentation
        (ClassFormation.baseField
          (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) →+
      ZHat
theorem

rationalCyclotomicZHatValuation_surjective

L903 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatValuation_surjective
Documentation

The transported rational cyclotomic valuation is surjective.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · statement
theorem rationalCyclotomicZHatValuation_surjective :
    Function.Surjective rationalCyclotomicZHatValuation
theorem

rationalCyclotomicZHatValuation_range

L920 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatValuation_range
Documentation

The value group of the transported rational valuation is all of ZHat.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · statement
theorem rationalCyclotomicZHatValuation_range :
    rationalCyclotomicZHatValuation.range =
      (⊤ : AddSubgroup ZHat)
theorem

rationalCyclotomicZHatValuation_integer_mem_range

L929 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatValuation_integer_mem_range
Documentation

Every integral profinite value belongs to the transported rational cyclotomic valuation range.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · statement
theorem rationalCyclotomicZHatValuation_integer_mem_range
    (m : ℤ) :
    (Int.castRingHom ZHat) m ∈
      rationalCyclotomicZHatValuation.range
theorem

rationalCyclotomicZHatValuation_canonicalValueQuotientMap_bijective

L938 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatValuation_canonicalValueQuotientMap_bijective
Documentation

The canonical quotient map for the transported rational cyclotomic valuation is bijective at every positive level.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · statement
theorem
    rationalCyclotomicZHatValuation_canonicalValueQuotientMap_bijective
    (n : ℕ) (hn : 0 < n) :
    Function.Bijective
      (canonicalValueQuotientMap
        rationalCyclotomicZHatValuation.range n hn)
instance

rationalCyclotomicFiniteAbstractFieldQuotientFinite

L953 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicFiniteAbstractFieldQuotientFinite
Source context 12 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
section AbstractFixedFieldNormRange
variable
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
Lean source · statement
instance rationalCyclotomicFiniteAbstractFieldQuotientFinite :
    Finite
      ((ClassFormation.baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (ClassFormation.baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          H.field (ClassFormation.le_baseField H.field))
theorem

rationalAbstractFixedFieldFiniteDimensional

L963 ↗
GlobalClassFieldTheory.Reciprocity.rationalAbstractFixedFieldFiniteDimensional
Source context 13 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
section AbstractFixedFieldNormRange
variable
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
local instance rationalCyclotomicFiniteAbstractFieldQuotientFinite :
    Finite
      ((ClassFormation.baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (ClassFormation.baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          H.field (ClassFormation.le_baseField H.field)) :=
  H.finite
Lean source · statement
theorem rationalAbstractFixedFieldFiniteDimensional :
    FiniteDimensional ℚ
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field)
theorem

rationalAbstractFixedFieldNumberField

L970 ↗
GlobalClassFieldTheory.Reciprocity.rationalAbstractFixedFieldNumberField
Source context 13 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
section AbstractFixedFieldNormRange
variable
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
local instance rationalCyclotomicFiniteAbstractFieldQuotientFinite :
    Finite
      ((ClassFormation.baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (ClassFormation.baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          H.field (ClassFormation.le_baseField H.field)) :=
  H.finite
Lean source · statement
theorem rationalAbstractFixedFieldNumberField :
    NumberField
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field)
theorem

rationalCyclotomicZHatIdeleClassNormComposite_abstractFixedField_range

L985 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatIdeleClassNormComposite_abstractFixedField_range
Documentation

For the actual number field fixed by a finite abstract field, the actual idele-class norm has cyclotomic image equal to the residue-degree multiples of ZHat.

Source context 13 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
section AbstractFixedFieldNormRange
variable
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
local instance rationalCyclotomicFiniteAbstractFieldQuotientFinite :
    Finite
      ((ClassFormation.baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (ClassFormation.baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          H.field (ClassFormation.le_baseField H.field)) :=
  H.finite
Lean source · full declaration
theorem
    rationalCyclotomicZHatIdeleClassNormComposite_abstractFixedField_range :
    let F :=
      LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field
    let : FiniteDimensional ℚ F :=
      rationalAbstractFixedFieldFiniteDimensional H
    let : NumberField F :=
      rationalAbstractFixedFieldNumberField H
    (rationalCyclotomicZHatIdeleClassNormComposite F).range =
      nsmulImage (⊤ : AddSubgroup ZHat)
        (H.residueDegree rationalCyclotomicDegreeData : ℕ) := by
  intro F hfinite hnumberField
  clear hfinite
  have hdegree :=
    cyclotomicZHatIntersectionDegree_abstractFixedField_eq_residueDegree H
  rw [rationalCyclotomicZHatIdeleClassNormComposite_range]
  exact
    congrArg
      (fun n : ℕ => nsmulImage (⊤ : AddSubgroup ZHat) n)
      hdegree
theorem

rationalCyclotomicZHatValuation_normToBase_range

L1009 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatValuation_normToBase_range
Documentation

Exact norm-range identity after transport from the actual fixed-field idele class group to the abstract fixed part.

Source context 13 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
section AbstractFixedFieldNormRange
variable
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
local instance rationalCyclotomicFiniteAbstractFieldQuotientFinite :
    Finite
      ((ClassFormation.baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (ClassFormation.baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          H.field (ClassFormation.le_baseField H.field)) :=
  H.finite
Lean source · statement
theorem rationalCyclotomicZHatValuation_normToBase_range :
    (rationalCyclotomicZHatValuation.comp
      (normToBase rationalIdeleClassRepresentation H.field)).range =
      nsmulImage rationalCyclotomicZHatValuation.range
        (H.residueDegree rationalCyclotomicDegreeData : ℕ)
def

rationalCyclotomicIdeleClassValuationData

L1071 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicIdeleClassValuationData
Documentation

The concrete henselian valuation data on the absolute rational idele-class representation, with cyclotomic degree data.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · full declaration
def rationalCyclotomicIdeleClassValuationData :
    ValuationData
      rationalCyclotomicDegreeData
      rationalIdeleClassRepresentation where
  toAddMonoidHom :=
    rationalCyclotomicZHatValuation
  integers_mem :=
    rationalCyclotomicZHatValuation_integer_mem_range
  canonical_value_quotient_bijective :=
    rationalCyclotomicZHatValuation_canonicalValueQuotientMap_bijective
  norm_range := by
    intro H
    exact rationalCyclotomicZHatValuation_normToBase_range H
theorem

rationalCyclotomicZHatValuation_normToBase_fixed_apply

L1088 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatValuation_normToBase_fixed_apply
Documentation

Transporting an actual fixed-field idele class into the rational absolute representation and then taking the base norm gives its ordinary idele-class norm cyclotomic value.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · statement
theorem rationalCyclotomicZHatValuation_normToBase_fixed_apply
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (c : Additive
      (IdeleClassGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field))) :
    rationalCyclotomicZHatValuation
        (normToBase rationalIdeleClassRepresentation H.field
          (rationalAbstractFixedFieldIdeleClassEquivFixed H.field c)) =
      rationalCyclotomicZHatIdeleClassNormComposite
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field) c
theorem

rationalCyclotomicIdeleClassValuationData_valuationAt_fixed_apply

L1124 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicIdeleClassValuationData_valuationAt_fixed_apply
Documentation

Under the genuine fixed-field idele-class comparison, the valuation used by abstract reciprocity is exactly the normalized cyclotomic idele-class value of that fixed field.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
attribute [local instance] cyclotomicValuationIdeleClassCommGroup
variable (K : Type) [Field K] [NumberField K]
/-- Use the rational algebra structure expected by the imported finite-layer
API throughout this block.  Fixing it before the first finite-layer binder
keeps the parameter and every restriction target definitionally aligned. -/
noncomputable local instance
    cyclotomicIdeleClassValuation_rationalCyclotomicZHatFieldAlgebra :
    Algebra ℚ rationalCyclotomicZHatField :=
  DivisionRing.toRatAlgebra
attribute [local instance]
  numberFieldCyclotomicZHatFiniteLayerNumberField
Lean source · statement
theorem
    rationalCyclotomicIdeleClassValuationData_valuationAt_fixed_apply
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (c : Additive
      (IdeleClassGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field))) :
    ((rationalCyclotomicIdeleClassValuationData.valuationAt H
        (rationalAbstractFixedFieldIdeleClassEquivFixed H.field c) :
          rationalCyclotomicIdeleClassValuationData.valueGroup) :
        ZHat) =
      normalizedCyclotomicZHatIdeleClassValueContinuous
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field) c

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