NYLL
Module

ArithmeticClassFieldCorrespondence.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ArithmeticClassFieldCorrespondence
5 declarations indexed from sourceView source ↗

Module documentation

Arithmetic topological class-field correspondence

For a closed finite-index subgroup H ≤ C_K, the selected actual class field has norm range exactly H. This module records the canonical arithmetic reciprocity homeomorphism Gal(L/K) ≃ₜ* C_K/H, so both the field and the topological group map are fixed rather than merely asserted to exist.

Imports10
Imported by2

Declarations

instance

arithmeticClassFieldCorrespondenceIdeleClassGroupIsMulCommutative

L45 ↗
GlobalClassFieldTheory.GlobalClassFields.arithmeticClassFieldCorrespondenceIdeleClassGroupIsMulCommutative
Documentation

Fix the commutative idèle-class instance path used by every quotient in this module, so the norm quotient and the literal quotient share one normality construction during elaboration.

Source context 7 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
open Reciprocity
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
instance
    arithmeticClassFieldCorrespondenceIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)
def

arithmeticClosedFiniteIndexClassFieldReciprocityData

L51 ↗
GlobalClassFieldTheory.GlobalClassFields.arithmeticClosedFiniteIndexClassFieldReciprocityData
Source context 8 commands

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

open scoped IsMulCommutative 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 used by every quotient in
this module, so the norm quotient and the literal quotient share one normality
construction during elaboration. -/
local instance
    arithmeticClassFieldCorrespondenceIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def
    arithmeticClosedFiniteIndexClassFieldReciprocityData
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    {e : Gal((closedFiniteIndexClassField
            (K := K) H hclosed) / K) ≃ₜ*
          IdeleClassGroup K ⧸ H //
      ∀ c : IdeleClassGroup K,
        e (arithmeticGlobalNormResidueMonoidHom K
            (closedFiniteIndexClassField
              (K := K) H hclosed) c) =
          QuotientGroup.mk' H c}
def

arithmeticClosedFiniteIndexClassFieldGaloisContinuousMulEquivNormQuotient

L122 ↗
GlobalClassFieldTheory.GlobalClassFields.arithmeticClosedFiniteIndexClassFieldGaloisContinuousMulEquivNormQuotient
Documentation

Arithmetic global reciprocity for the actual class field selected by a closed finite-index idèle-class subgroup.

Source context 8 commands

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

open scoped IsMulCommutative 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 used by every quotient in
this module, so the norm quotient and the literal quotient share one normality
construction during elaboration. -/
local instance
    arithmeticClassFieldCorrespondenceIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def
    arithmeticClosedFiniteIndexClassFieldGaloisContinuousMulEquivNormQuotient
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    Gal((closedFiniteIndexClassField
          (K := K) H hclosed) / K) ≃ₜ*
      IdeleClassGroup K ⧸ H
theorem

arithmeticClosedFiniteIndexClassFieldGaloisContinuousMulEquivNormQuotient_globalNormResidue

L136 ↗
GlobalClassFieldTheory.GlobalClassFields.arithmeticClosedFiniteIndexClassFieldGaloisContinuousMulEquivNormQuotient_globalNormResidue
Documentation

The arithmetic norm-residue symbol of an idèle class maps to its literal class modulo the defining subgroup.

Source context 8 commands

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

open scoped IsMulCommutative 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 used by every quotient in
this module, so the norm quotient and the literal quotient share one normality
construction during elaboration. -/
local instance
    arithmeticClassFieldCorrespondenceIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem
    arithmeticClosedFiniteIndexClassFieldGaloisContinuousMulEquivNormQuotient_globalNormResidue
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex]
    (c : IdeleClassGroup K) :
    arithmeticClosedFiniteIndexClassFieldGaloisContinuousMulEquivNormQuotient
        (K := K) H hclosed
        (arithmeticGlobalNormResidueMonoidHom K
          (closedFiniteIndexClassField
            (K := K) H hclosed) c) =
      QuotientGroup.mk' H c
theorem

arithmeticClosedFiniteIndexClassFieldGaloisContinuousMulEquivNormQuotient_symm_mk

L155 ↗
GlobalClassFieldTheory.GlobalClassFields.arithmeticClosedFiniteIndexClassFieldGaloisContinuousMulEquivNormQuotient_symm_mk
Documentation

The inverse correspondence sends a represented class modulo H to its actual arithmetic global norm-residue automorphism.

Source context 8 commands

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

open scoped IsMulCommutative 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 used by every quotient in
this module, so the norm quotient and the literal quotient share one normality
construction during elaboration. -/
local instance
    arithmeticClassFieldCorrespondenceIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem
    arithmeticClosedFiniteIndexClassFieldGaloisContinuousMulEquivNormQuotient_symm_mk
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex]
    (c : IdeleClassGroup K) :
    (arithmeticClosedFiniteIndexClassFieldGaloisContinuousMulEquivNormQuotient
      (K := K) H hclosed).symm
        (QuotientGroup.mk' H c) =
      arithmeticGlobalNormResidueMonoidHom K
        (closedFiniteIndexClassField
          (K := K) H hclosed) c

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