NYLL
Module

MathlibGlobalReciprocity.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.MathlibGlobalReciprocity
14 declarations indexed from sourceView source ↗

Module documentation

Global class field theory implementation

This is the implementation layer for the reader-facing global CFT module. It collects the existing finite reciprocity, maximal abelian reciprocity, class-field existence, and infinite correspondence modules without adding parallel names or existence wrappers.

Imports15
Imported by2

Declarations

theorem

ideleClassGroupIsMulCommutative

L43 ↗
ClassFieldTheory.GlobalClassFieldComparison.ideleClassGroupIsMulCommutative
Documentation

The idèle class group is commutative. Keeping this witness public stabilizes normal-subgroup arguments in exported quotient statements.

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
Lean source · statement
theorem ideleClassGroupIsMulCommutative
    (K : Type) [Field K] [NumberField K] :
    IsMulCommutative (IdeleClassGroup K)
theorem

exists_unramifiedOutsideModulus

L53 ↗
ClassFieldTheory.GlobalClassFieldComparison.exists_unramifiedOutsideModulus
Documentation

The ramified finite primes form a finite set. Adding every real place produces a public modulus outside which a number-field extension is unramified, independently of any Artin-map construction.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
attribute [local instance 2000] ideleClassGroupIsMulCommutative
Lean source · statement
theorem exists_unramifiedOutsideModulus
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L] :
    ∃ m : RayClassModulus K, IsUnramifiedOutsideModulus K L m
def

normConductorRayClassModulus

L98 ↗
ClassFieldTheory.GlobalClassFieldComparison.normConductorRayClassModulus
Documentation

The public narrow modulus whose finite part is the actual norm conductor.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
attribute [local instance 2000] ideleClassGroupIsMulCommutative
Lean source · statement
def normConductorRayClassModulus
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L] : RayClassModulus K
theorem

normConductorRayClassModulus_original

L111 ↗
ClassFieldTheory.GlobalClassFieldComparison.normConductorRayClassModulus_original
Documentation

The public norm-conductor modulus is the original narrow modulus.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
attribute [local instance 2000] ideleClassGroupIsMulCommutative
Lean source · statement
theorem normConductorRayClassModulus_original
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L] :
    rayClassModulusToOriginal K (normConductorRayClassModulus K L) =
      RayClass.Modulus.narrowOfFinite
        (GlobalClassFieldTheory.GlobalClassFields.ideleClassNormNarrowFiniteConductor
          (K := K) (L := L))
theorem

normConductorRayClassModulus_unramifiedOutside

L130 ↗
ClassFieldTheory.GlobalClassFieldComparison.normConductorRayClassModulus_unramifiedOutside
Documentation

The actual narrow finite norm conductor, together with every real place, is a public modulus outside which a finite abelian extension is unramified.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
attribute [local instance 2000] ideleClassGroupIsMulCommutative
open _root_.GlobalClassFieldTheory.GlobalClassFields (
  ideleClassNorm_narrowFiniteConductor_support_eq_ramifiedBaseFinitePlaces
) in
Lean source · statement
theorem normConductorRayClassModulus_unramifiedOutside
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L] :
    IsUnramifiedOutsideModulus K L (normConductorRayClassModulus K L)
theorem

unramifiedOutside_normConductorModulus

L165 ↗
ClassFieldTheory.GlobalClassFieldComparison.unramifiedOutside_normConductorModulus
Documentation

The norm conductor yields a public modulus outside which the extension is unramified.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
attribute [local instance 2000] ideleClassGroupIsMulCommutative
Lean source · statement
theorem unramifiedOutside_normConductorModulus
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L] :
    ∃ m : RayClassModulus K,
      m.finitePart =
        GlobalClassFieldTheory.GlobalClassFields.ideleClassNormNarrowFiniteConductor
          (K := K) (L := L) ∧
        IsUnramifiedOutsideModulus K L m
theorem

normConductorRayClassModulus_isDefining

L184 ↗
ClassFieldTheory.GlobalClassFieldComparison.normConductorRayClassModulus_isDefining
Documentation

The public norm-conductor modulus is a defining modulus for the actual idèle-class norm subgroup.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
attribute [local instance 2000] ideleClassGroupIsMulCommutative
open _root_.GlobalClassFieldTheory.GlobalClassFields (
  ideleClassNorm_narrowFiniteConductor_isDefiningModulus
) in
Lean source · statement
theorem normConductorRayClassModulus_isDefining
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L] :
    RayClass.Modulus.congruenceSubgroup
        (rayClassModulusToOriginal K (normConductorRayClassModulus K L)) ≤
      (_root_.ideleClassNorm K L).range
def

normConductorArtin

L198 ↗
ClassFieldTheory.GlobalClassFieldComparison.normConductorArtin
Documentation

Arithmetic global reciprocity, descended to the public ray class group at the actual narrow norm conductor.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
attribute [local instance 2000] ideleClassGroupIsMulCommutative
Lean source · statement
def normConductorArtin
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L] :
    RayClassGroup (normConductorRayClassModulus K L) →* (L ≃ₐ[K] L)
theorem

normConductorArtin_surjective

L216 ↗
ClassFieldTheory.GlobalClassFieldComparison.normConductorArtin_surjective
Documentation

The conductor ray-class Artin map is onto the finite abelian Galois group.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
attribute [local instance 2000] ideleClassGroupIsMulCommutative
Lean source · statement
theorem normConductorArtin_surjective
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L] :
    Function.Surjective (normConductorArtin K L)
theorem

normConductorArtin_prime

L236 ↗
ClassFieldTheory.GlobalClassFieldComparison.normConductorArtin_prime
Documentation

At a prime away from the norm conductor, the public Artin map agrees with the arithmetic prime Artin element of the original idèle theory.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
attribute [local instance 2000] ideleClassGroupIsMulCommutative
open _root_.GlobalClassFieldTheory.IdealClassFieldTheory (
  arithmeticIdealArtinGaloisMap_primeIdeal_eq_arithmeticFinitePlacePrimeArtin
) in
Lean source · statement
theorem normConductorArtin_prime
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ (normConductorRayClassModulus K L).finitePart.support) :
    normConductorArtin K L
        (rayClassOfFinitePrime (normConductorRayClassModulus K L) v hv) =
      GlobalClassFieldTheory.GlobalClassFields.arithmeticFinitePlacePrimeArtin
        (K := K) (L := L) v
theorem

classFieldExistence_normSubgroup

L267 ↗
ClassFieldTheory.GlobalClassFieldComparison.classFieldExistence_normSubgroup
Documentation

The class field selected from a closed finite-index idèle-class subgroup has exactly that subgroup as its norm group.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
attribute [local instance 2000] ideleClassGroupIsMulCommutative
Lean source · statement
theorem classFieldExistence_normSubgroup
    (K : Type) [Field K] [NumberField K]
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    (_root_.ideleClassNorm K
        (GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassField
          (K := K) H hclosed)).range = H
theorem

classFieldExistence_degree

L280 ↗
ClassFieldTheory.GlobalClassFieldComparison.classFieldExistence_degree
Documentation

The degree of the selected class field is the index of its defining idèle-class subgroup.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
attribute [local instance 2000] ideleClassGroupIsMulCommutative
Lean source · statement
theorem classFieldExistence_degree
    (K : Type) [Field K] [NumberField K]
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    Module.finrank K
        (GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassField
          (K := K) H hclosed) = H.index
theorem

finiteAbelianGlobalReciprocity

L293 ↗
ClassFieldTheory.GlobalClassFieldComparison.finiteAbelianGlobalReciprocity
Documentation

The implemented arithmetic norm-residue isomorphism proves finite abelian global reciprocity in quotient form.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
attribute [local instance 2000] ideleClassGroupIsMulCommutative
Lean source · statement
theorem finiteAbelianGlobalReciprocity
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L] :
    Nonempty
      ((IdeleClassGroup K ⧸ (_root_.ideleClassNorm K L).range) ≃ₜ*
        (L ≃ₐ[K] L))
theorem

maximalAbelianGlobalReciprocity

L306 ↗
ClassFieldTheory.GlobalClassFieldComparison.maximalAbelianGlobalReciprocity
Documentation

Maximal abelian reciprocity after quotienting by the identity component.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
attribute [local instance 2000] ideleClassGroupIsMulCommutative
Lean source · statement
theorem maximalAbelianGlobalReciprocity
    (K : Type) [Field K] [NumberField K] :
    Nonempty
      (ideleClassComponentQuotient K ≃ₜ*
        (maximalAbelianExtension K ≃ₐ[K] maximalAbelianExtension K))

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