Module

CyclicRayClassMaximality.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.CyclicRayClassMaximality

4 declarations indexed from sourceView source ↗

Module documentation

Maximal cyclic quotients at the narrow finite conductor

For a finite cyclic extension, the actual idèle-class norm quotient has order equal to the extension degree. The ray class group at the exact narrow finite conductor surjects onto this norm quotient. This file identifies the case in which that surjection is an isomorphism: precisely when the ray class number already equals the extension degree.

Equivalently, the actual norm subgroup is then exactly the ray congruence subgroup at its narrow finite conductor.

Imports2

Imported by3

theorem

cyclicRayClassMaximalityClassGroupIsMulCommutative

L35 ↗

GlobalClassFieldTheory.GlobalClassFields.cyclicRayClassMaximalityClassGroupIsMulCommutative

Documentation

The canonical idèle-class multiplication makes every subgroup normal.

Source context 5 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField

Lean source · statement

theorem cyclicRayClassMaximalityClassGroupIsMulCommutative
    (F : Type) [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)

theorem

ideleClassNorm_range_eq_narrowConductorSubgroup_iff_rayClass_card_eq_degree

L52 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNorm_range_eq_narrowConductorSubgroup_iff_rayClass_card_eq_degree

Documentation

The actual idèle-class norm subgroup of a finite cyclic extension is the congruence subgroup at its exact narrow finite conductor precisely when the corresponding ray class number equals the extension degree.

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
attribute [local instance] cyclicRayClassMaximalityClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]

Lean source · statement

theorem
    ideleClassNorm_range_eq_narrowConductorSubgroup_iff_rayClass_card_eq_degree :
    (_root_.ideleClassNorm K L).range =
        RayClass.Modulus.congruenceSubgroup
          (RayClass.Modulus.narrowOfFinite
            (ideleClassNormNarrowFiniteConductor (K := K) (L := L))) ↔
      Nat.card
          (RayClass.RayClassGroup
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))) =
        Module.finrank K L

theorem

narrowFiniteConductorRayClassGroupToIdeleClassNormQuotient_injective_iff_card_eq_extensionDegree

L72 ↗

GlobalClassFieldTheory.GlobalClassFields.narrowFiniteConductorRayClassGroupToIdeleClassNormQuotient_injective_iff_card_eq_extensionDegree

Documentation

The canonical map from the ray class group at the exact narrow finite norm conductor to the actual norm quotient is injective precisely when the ray class number equals the extension degree.

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
attribute [local instance] cyclicRayClassMaximalityClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]

Lean source · statement

theorem
  narrowFiniteConductorRayClassGroupToIdeleClassNormQuotient_injective_iff_card_eq_extensionDegree :
    Function.Injective
        (narrowFiniteConductorRayClassGroupToIdeleClassNormQuotient
          (K := K) (L := L)) ↔
      Nat.card
          (RayClass.RayClassGroup
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))) =
        Module.finrank K L

def

cyclicNormQuotientEquivNarrowFiniteConductorRayClassGroup

L92 ↗

GlobalClassFieldTheory.GlobalClassFields.cyclicNormQuotientEquivNarrowFiniteConductorRayClassGroup

Documentation

When the ray class number at the exact narrow finite norm conductor equals the degree of a finite cyclic extension, its actual norm quotient is canonically the full ray class group at that conductor.

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
attribute [local instance] cyclicRayClassMaximalityClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]

Lean source · statement

def cyclicNormQuotientEquivNarrowFiniteConductorRayClassGroup
    (hcard :
      Nat.card
          (RayClass.RayClassGroup
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))) =
        Module.finrank K L) :
    (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) ≃*
      RayClass.RayClassGroup
        (RayClass.Modulus.narrowOfFinite
          (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))

Module documentation

Maximal cyclic quotients at the narrow finite conductor

Declarations

cyclicRayClassMaximalityClassGroupIsMulCommutative

ideleClassNorm_range_eq_narrowConductorSubgroup_iff_rayClass_card_eq_degree

narrowFiniteConductorRayClassGroupToIdeleClassNormQuotient_injective_iff_card_eq_extensionDegree

cyclicNormQuotientEquivNarrowFiniteConductorRayClassGroup