Module

ArithmeticHilbertClassFieldReciprocity.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ArithmeticHilbertClassFieldReciprocity

11 declarations indexed from sourceView source ↗

Module documentation

Arithmetic reciprocity for the actual Hilbert class fields

The canonical ideal-theoretic Artin map uses arithmetic Frobenius. Accordingly, these equivalences use arithmetic global reciprocity before identifying the intrinsic Hilbert norm quotient with the narrow or ordinary ideal class group. The class groups in the current API carry no native topological structure, so the mathematically correct public bundle here is MulEquiv; the preceding Galois/norm-quotient factor remains a ContinuousMulEquiv.

Imports6

Imported by2

instance

arithmeticHilbertClassFieldIdeleClassGroupIsMulCommutative

L42 ↗

GlobalClassFieldTheory.GlobalClassFields.arithmeticHilbertClassFieldIdeleClassGroupIsMulCommutative

Documentation

Fix the commutative idèle-class instance path shared by the norm quotient and its transported literal quotient throughout this module.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

instance
    arithmeticHilbertClassFieldIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)

theorem

arithmeticReciprocity_quotientTransport_globalNormResidue

L50 ↗

GlobalClassFieldTheory.GlobalClassFields.arithmeticReciprocity_quotientTransport_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
variable {K : Type} [Field K] [NumberField K]
/-- Fix the commutative idèle-class instance path shared by the norm quotient
and its transported literal quotient throughout this module. -/
local instance
    arithmeticHilbertClassFieldIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem
    arithmeticReciprocity_quotientTransport_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

theorem

arithmeticReciprocity_quotientTransport_trans_globalNormResidue

L88 ↗

GlobalClassFieldTheory.GlobalClassFields.arithmeticReciprocity_quotientTransport_trans_globalNormResidue

Documentation

Postcomposing transported arithmetic reciprocity with any quotient equivalence preserves the represented quotient class formula.

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
variable {K : Type} [Field K] [NumberField K]
/-- Fix the commutative idèle-class instance path shared by the norm quotient
and its transported literal quotient throughout this module. -/
local instance
    arithmeticHilbertClassFieldIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem
    arithmeticReciprocity_quotientTransport_trans_globalNormResidue
    {F E A : Type} [Field F] [NumberField F]
    [Field E] [NumberField E] [Algebra F E]
    [FiniteDimensional F E] [IsAbelianGalois F E]
    [Group A]
    (H : Subgroup (IdeleClassGroup F))
    (h : (_root_.ideleClassNorm F E).range = H)
    (f : (IdeleClassGroup F ⧸ H) ≃* A)
    (c : IdeleClassGroup F) :
    ((arithmeticGlobalReciprocityContinuousMulEquiv F E).toMulEquiv.trans
        ((QuotientGroup.quotientMulEquivOfEq h).trans f))
        (arithmeticGlobalNormResidueMonoidHom F E c) =
      f (QuotientGroup.mk' H c)

def

arithmeticBigHilbertClassFieldReciprocityData

L115 ↗

GlobalClassFieldTheory.GlobalClassFields.arithmeticBigHilbertClassFieldReciprocityData

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
variable {K : Type} [Field K] [NumberField K]
/-- Fix the commutative idèle-class instance path shared by the norm quotient
and its transported literal quotient throughout this module. -/
local instance
    arithmeticHilbertClassFieldIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

def arithmeticBigHilbertClassFieldReciprocityData
    (K : Type) [Field K] [NumberField K] :
    { e : Gal((bigHilbertClassField K) / K) ≃*
        RayClass.NarrowClassGroup K //
      ∀ c : IdeleClassGroup K,
        e (arithmeticGlobalNormResidueMonoidHom
            K (bigHilbertClassField K) c) =
          bigHilbertClassFieldQuotientEquivNarrowClassGroup
            (K := K)
            (QuotientGroup.mk'
              (bigHilbertClassFieldNormSubgroup (K := K)) c) }

def

arithmeticSmallHilbertClassFieldReciprocityData

L140 ↗

GlobalClassFieldTheory.GlobalClassFields.arithmeticSmallHilbertClassFieldReciprocityData

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
variable {K : Type} [Field K] [NumberField K]
/-- Fix the commutative idèle-class instance path shared by the norm quotient
and its transported literal quotient throughout this module. -/
local instance
    arithmeticHilbertClassFieldIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

def arithmeticSmallHilbertClassFieldReciprocityData
    (K : Type) [Field K] [NumberField K] :
    { e : Gal((smallHilbertClassField K) / K) ≃*
        ClassGroup (𝓞 K) //
      ∀ c : IdeleClassGroup K,
        e (arithmeticGlobalNormResidueMonoidHom
            K (smallHilbertClassField K) c) =
          smallHilbertClassFieldQuotientEquivClassGroup
            (K := K)
            (QuotientGroup.mk'
              (smallHilbertClassFieldNormSubgroup (K := K)) c) }

def

arithmeticBigHilbertClassFieldGaloisEquivNarrowClassGroupOverOriginal

L167 ↗

GlobalClassFieldTheory.GlobalClassFields.arithmeticBigHilbertClassFieldGaloisEquivNarrowClassGroupOverOriginal

Documentation

Arithmetic global reciprocity for the selected big Hilbert class field over the original number field.

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
variable {K : Type} [Field K] [NumberField K]
/-- Fix the commutative idèle-class instance path shared by the norm quotient
and its transported literal quotient throughout this module. -/
local instance
    arithmeticHilbertClassFieldIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

def
    arithmeticBigHilbertClassFieldGaloisEquivNarrowClassGroupOverOriginal :
    Gal((bigHilbertClassField K) / K) ≃*
      RayClass.NarrowClassGroup K

theorem

arithmeticBigHilbertClassFieldGaloisEquivNarrowClassGroupOverOriginal_globalNormResidue

L176 ↗

GlobalClassFieldTheory.GlobalClassFields.arithmeticBigHilbertClassFieldGaloisEquivNarrowClassGroupOverOriginal_globalNormResidue

Documentation

The arithmetic global norm-residue symbol maps to its genuine narrow ideal 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
variable {K : Type} [Field K] [NumberField K]
/-- Fix the commutative idèle-class instance path shared by the norm quotient
and its transported literal quotient throughout this module. -/
local instance
    arithmeticHilbertClassFieldIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem
    arithmeticBigHilbertClassFieldGaloisEquivNarrowClassGroupOverOriginal_globalNormResidue
    (c : IdeleClassGroup K) :
    arithmeticBigHilbertClassFieldGaloisEquivNarrowClassGroupOverOriginal
        (K := K)
        (arithmeticGlobalNormResidueMonoidHom
          K (bigHilbertClassField K) c) =
      bigHilbertClassFieldQuotientEquivNarrowClassGroup
        (K := K)
        (QuotientGroup.mk'
          (bigHilbertClassFieldNormSubgroup (K := K)) c)

theorem

arithmeticBigHilbertClassFieldGaloisEquivNarrowClassGroupOverOriginal_idele

L192 ↗

GlobalClassFieldTheory.GlobalClassFields.arithmeticBigHilbertClassFieldGaloisEquivNarrowClassGroupOverOriginal_idele

Documentation

On an actual idèle, arithmetic big-Hilbert reciprocity is its narrow ideal 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
variable {K : Type} [Field K] [NumberField K]
/-- Fix the commutative idèle-class instance path shared by the norm quotient
and its transported literal quotient throughout this module. -/
local instance
    arithmeticHilbertClassFieldIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem
    arithmeticBigHilbertClassFieldGaloisEquivNarrowClassGroupOverOriginal_idele
    (a : IdeleGroup K) :
    arithmeticBigHilbertClassFieldGaloisEquivNarrowClassGroupOverOriginal
        (K := K)
        (arithmeticGlobalNormResidueMonoidHom
          K (bigHilbertClassField K)
          (QuotientGroup.mk'
            (IdeleGroup.principalSubgroup K) a)) =
      QuotientGroup.mk'
        (RayClass.narrowDenominator (K := K)) a

def

arithmeticSmallHilbertClassFieldGaloisEquivClassGroupOverOriginal

L209 ↗

GlobalClassFieldTheory.GlobalClassFields.arithmeticSmallHilbertClassFieldGaloisEquivClassGroupOverOriginal

Documentation

Arithmetic global reciprocity for the selected small Hilbert class field over the original number field.

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
variable {K : Type} [Field K] [NumberField K]
/-- Fix the commutative idèle-class instance path shared by the norm quotient
and its transported literal quotient throughout this module. -/
local instance
    arithmeticHilbertClassFieldIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

def
    arithmeticSmallHilbertClassFieldGaloisEquivClassGroupOverOriginal :
    Gal((smallHilbertClassField K) / K) ≃*
      ClassGroup (𝓞 K)

theorem

arithmeticSmallHilbertClassFieldGaloisEquivClassGroupOverOriginal_globalNormResidue

L218 ↗

GlobalClassFieldTheory.GlobalClassFields.arithmeticSmallHilbertClassFieldGaloisEquivClassGroupOverOriginal_globalNormResidue

Documentation

The arithmetic global norm-residue symbol maps to its genuine ordinary ideal 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
variable {K : Type} [Field K] [NumberField K]
/-- Fix the commutative idèle-class instance path shared by the norm quotient
and its transported literal quotient throughout this module. -/
local instance
    arithmeticHilbertClassFieldIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem
    arithmeticSmallHilbertClassFieldGaloisEquivClassGroupOverOriginal_globalNormResidue
    (c : IdeleClassGroup K) :
    arithmeticSmallHilbertClassFieldGaloisEquivClassGroupOverOriginal
        (K := K)
        (arithmeticGlobalNormResidueMonoidHom
          K (smallHilbertClassField K) c) =
      smallHilbertClassFieldQuotientEquivClassGroup
        (K := K)
        (QuotientGroup.mk'
          (smallHilbertClassFieldNormSubgroup (K := K)) c)

theorem

arithmeticSmallHilbertClassFieldGaloisEquivClassGroupOverOriginal_idele

L234 ↗

GlobalClassFieldTheory.GlobalClassFields.arithmeticSmallHilbertClassFieldGaloisEquivClassGroupOverOriginal_idele

Documentation

On an actual idèle, arithmetic small-Hilbert reciprocity is its ordinary ideal 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
variable {K : Type} [Field K] [NumberField K]
/-- Fix the commutative idèle-class instance path shared by the norm quotient
and its transported literal quotient throughout this module. -/
local instance
    arithmeticHilbertClassFieldIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem
    arithmeticSmallHilbertClassFieldGaloisEquivClassGroupOverOriginal_idele
    (a : IdeleGroup K) :
    arithmeticSmallHilbertClassFieldGaloisEquivClassGroupOverOriginal
        (K := K)
        (arithmeticGlobalNormResidueMonoidHom
          K (smallHilbertClassField K)
          (QuotientGroup.mk'
            (IdeleGroup.principalSubgroup K) a)) =
      IdeleGroup.idealClass a

Module documentation

Arithmetic reciprocity for the actual Hilbert class fields

Declarations