Module

RayClassComparison.lean

Nyll.ClassFieldTheory.KroneckerWeber.RayClassComparison

4 declarations indexed from sourceView source ↗

Module documentation

The rational ray-class/cyclotomic comparison

For K = ℚ, both the ray class quotient modulo (m) and the Galois group of the m-th cyclotomic field are canonically (ℤ/mℤ)ˣ. This file composes the two independently constructed equivalences and verifies the degree/index equality showing that the ray class field is ℚ(μ_m).

Imports3

Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.Topology
Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.Rational
Mathlib.NumberTheory.Cyclotomic.Gal

Imported by3

def

rationalRayClassGroupEquivCyclotomicAut

L31 ↗

KroneckerWeber.rationalRayClassGroupEquivCyclotomicAut

Documentation

The rational ray class group modulo (m) is canonically the automorphism group of the m-th cyclotomic field.

Source context 4 commands

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

open scoped NumberField Cyclotomic
noncomputable section
namespace KroneckerWeber
open Polynomial

Lean source · statement

def rationalRayClassGroupEquivCyclotomicAut
    (m : ℕ) (hm : m ≠ 0) :
    RayClass.RayClassGroup (RayClass.rationalModulus m) ≃*
      (CyclotomicField m ℚ ≃ₐ[ℚ] CyclotomicField m ℚ)

def

rationalRayClassFieldQuotientEquivCyclotomicAut

L49 ↗

KroneckerWeber.rationalRayClassFieldQuotientEquivCyclotomicAut

Documentation

The quotient by the rational ray-class norm subgroup is the Galois group of the corresponding cyclotomic field.

Source context 4 commands

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

open scoped NumberField Cyclotomic
noncomputable section
namespace KroneckerWeber
open Polynomial

Lean source · statement

def rationalRayClassFieldQuotientEquivCyclotomicAut
    (m : ℕ) (hm : m ≠ 0) :
    IdeleClassGroup ℚ ⧸
        RayClass.Modulus.congruenceSubgroup
          (RayClass.rationalModulus m) ≃*
      (CyclotomicField m ℚ ≃ₐ[ℚ] CyclotomicField m ℚ)

theorem

rationalRayClassFieldQuotient_card_eq_cyclotomicDegree

L59 ↗

KroneckerWeber.rationalRayClassFieldQuotient_card_eq_cyclotomicDegree

Documentation

The index of the rational ray congruence subgroup equals the degree of the m-th cyclotomic field.

Source context 4 commands

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

open scoped NumberField Cyclotomic
noncomputable section
namespace KroneckerWeber
open Polynomial

Lean source · statement

theorem rationalRayClassFieldQuotient_card_eq_cyclotomicDegree
    (m : ℕ) (hm : m ≠ 0) :
    Nat.card
        (IdeleClassGroup ℚ ⧸
          RayClass.Modulus.congruenceSubgroup
            (RayClass.rationalModulus m)) =
      Module.finrank ℚ (CyclotomicField m ℚ)

theorem

rationalRayClassFieldQuotient_card_eq_totient

L90 ↗

KroneckerWeber.rationalRayClassFieldQuotient_card_eq_totient

Documentation

Both sides of the rational ray-class/cyclotomic comparison have Euler-totient order.

Source context 4 commands

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

open scoped NumberField Cyclotomic
noncomputable section
namespace KroneckerWeber
open Polynomial

Lean source · statement

theorem rationalRayClassFieldQuotient_card_eq_totient
    (m : ℕ) (hm : m ≠ 0) :
    Nat.card
        (IdeleClassGroup ℚ ⧸
          RayClass.Modulus.congruenceSubgroup
            (RayClass.rationalModulus m)) =
      m.totient

Module documentation

The rational ray-class/cyclotomic comparison

Declarations

rationalRayClassGroupEquivCyclotomicAut

rationalRayClassFieldQuotientEquivCyclotomicAut

rationalRayClassFieldQuotient_card_eq_cyclotomicDegree

rationalRayClassFieldQuotient_card_eq_totient