NYLL
Module

ArithmeticRayClassFieldReciprocity.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ArithmeticRayClassFieldReciprocity
6 declarations indexed from sourceView source ↗

Module documentation

Arithmetic reciprocity for actual ray class fields

This is the canonical topological isomorphism Gal(Kᵐ/K) ≃ₜ* C_K/C_Kᵐ with arithmetic Frobenius normalization. It uses the actual selected ray class field, its exact idèle norm range, the finite Krull topology, and the native ray-class quotient topology.

Imports2
Imported by2

Declarations

theorem

arithmeticRayClassIdeleClassGroupIsMulCommutative

L32 ↗
GlobalClassFieldTheory.GlobalClassFields.arithmeticRayClassIdeleClassGroupIsMulCommutative
Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
open Reciprocity
Lean source · statement
theorem arithmeticRayClassIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)
theorem

arithmeticReciprocity_quotientMulEquivOfEq_globalNormResidue

L43 ↗
GlobalClassFieldTheory.GlobalClassFields.arithmeticReciprocity_quotientMulEquivOfEq_globalNormResidue
Documentation

Arithmetic reciprocity followed by transport between equal norm quotients sends a norm-residue symbol to its represented quotient class.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
open Reciprocity
attribute [local instance] arithmeticRayClassIdeleClassGroupIsMulCommutative
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
theorem
    arithmeticReciprocity_quotientMulEquivOfEq_globalNormResidue
    {F E : Type} [Field F] [NumberField F]
    [Field E] [NumberField E] [Algebra F E]
    [FiniteDimensional F E] [IsAbelianGalois F E]
    (H : Subgroup (IdeleClassGroup F))
    (h : (_root_.ideleClassNorm F E).range = H)
    (c : IdeleClassGroup F) :
    QuotientGroup.quotientMulEquivOfEq h
        (arithmeticGlobalReciprocityContinuousMulEquiv F E
          (arithmeticGlobalNormResidueMonoidHom F E c)) =
      QuotientGroup.mk' H c
def

arithmeticRayClassFieldGaloisContinuousMulEquivRayClassGroup

L80 ↗
GlobalClassFieldTheory.GlobalClassFields.arithmeticRayClassFieldGaloisContinuousMulEquivRayClassGroup
Documentation

Arithmetic global reciprocity for the actual selected ray class field, bundled with both native topologies.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
open Reciprocity
attribute [local instance] arithmeticRayClassIdeleClassGroupIsMulCommutative
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
def
    arithmeticRayClassFieldGaloisContinuousMulEquivRayClassGroup
    (m : RayClass.Modulus K) :
    Gal((rayClassField K m) / K) ≃ₜ*
      RayClass.RayClassGroup m
theorem

arithmeticRayClassFieldGaloisContinuousMulEquivRayClassGroup_apply

L112 ↗
GlobalClassFieldTheory.GlobalClassFields.arithmeticRayClassFieldGaloisContinuousMulEquivRayClassGroup_apply
Documentation

Pointwise evaluation of arithmetic ray-class reciprocity separates global reciprocity from the transport between the equal norm quotients.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
open Reciprocity
attribute [local instance] arithmeticRayClassIdeleClassGroupIsMulCommutative
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
theorem
    arithmeticRayClassFieldGaloisContinuousMulEquivRayClassGroup_apply
    (m : RayClass.Modulus K)
    (σ : Gal((rayClassField K m)/K)) :
    arithmeticRayClassFieldGaloisContinuousMulEquivRayClassGroup
        (K := K) m σ =
      QuotientGroup.quotientMulEquivOfEq
        (rayClassField_ideleClassNorm_range_over_original
          (K := K) m)
        (arithmeticGlobalReciprocityContinuousMulEquiv
          K (rayClassField K m) σ)
theorem

arithmeticRayClassFieldGaloisContinuousMulEquivRayClassGroup_globalNormResidue

L128 ↗
GlobalClassFieldTheory.GlobalClassFields.arithmeticRayClassFieldGaloisContinuousMulEquivRayClassGroup_globalNormResidue
Documentation

Arithmetic ray-class reciprocity sends the arithmetic global norm-residue symbol of an idèle class to its literal ray class.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
open Reciprocity
attribute [local instance] arithmeticRayClassIdeleClassGroupIsMulCommutative
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
theorem
    arithmeticRayClassFieldGaloisContinuousMulEquivRayClassGroup_globalNormResidue
    (m : RayClass.Modulus K)
    (c : IdeleClassGroup K) :
    arithmeticRayClassFieldGaloisContinuousMulEquivRayClassGroup
        (K := K) m
        (arithmeticGlobalNormResidueMonoidHom
          K (rayClassField K m) c) =
      QuotientGroup.mk'
        (RayClass.Modulus.congruenceSubgroup m) c
theorem

arithmeticRayClassFieldGaloisContinuousMulEquivRayClassGroup_symm_mk

L162 ↗
GlobalClassFieldTheory.GlobalClassFields.arithmeticRayClassFieldGaloisContinuousMulEquivRayClassGroup_symm_mk
Documentation

Inverse arithmetic ray reciprocity sends a represented ray class back to the arithmetic global norm-residue symbol.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
open Reciprocity
attribute [local instance] arithmeticRayClassIdeleClassGroupIsMulCommutative
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
theorem
    arithmeticRayClassFieldGaloisContinuousMulEquivRayClassGroup_symm_mk
    (m : RayClass.Modulus K)
    (c : IdeleClassGroup K) :
    (arithmeticRayClassFieldGaloisContinuousMulEquivRayClassGroup
      (K := K) m).symm
        (QuotientGroup.mk'
          (RayClass.Modulus.congruenceSubgroup m) c) =
      arithmeticGlobalNormResidueMonoidHom
        K (rayClassField K m) c

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