Module

CyclicNormConductor.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.CyclicNormConductor

2 declarations indexed from sourceView source ↗

Module documentation

Narrow finite conductors of cyclic class-norm subgroups

For a finite cyclic extension, the actual idele-class norm quotient has order equal to the extension degree. Substituting this norm-index theorem into the narrow finite conductor ray-class factorization identifies the ray class number at the exact narrow finite conductor as the product of the residual norm-subgroup image order and the extension degree.

Imports2

Imported by2

theorem

narrowFiniteConductorRayClassGroup_card_eq_normSubgroupImage_card_mul_extensionDegree

L41 ↗

GlobalClassFieldTheory.GlobalClassFields.narrowFiniteConductorRayClassGroup_card_eq_normSubgroupImage_card_mul_extensionDegree

Documentation

For a finite cyclic extension, the ray class number at the exact narrow finite norm conductor is the order of the norm-subgroup image modulo the conductor congruence subgroup times the extension degree.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
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
    narrowFiniteConductorRayClassGroup_card_eq_normSubgroupImage_card_mul_extensionDegree :
    Nat.card
        (RayClass.RayClassGroup
          (RayClass.Modulus.narrowOfFinite
            (ideleClassNormNarrowFiniteConductor
              (K := K) (L := L)))) =
      Nat.card
          (Subgroup.map
            (QuotientGroup.mk'
              (RayClass.Modulus.congruenceSubgroup
                (RayClass.Modulus.narrowOfFinite
                  (ideleClassNormNarrowFiniteConductor
                    (K := K) (L := L)))))
            ((_root_.ideleClassNorm K L).range)) *
        Module.finrank K L

theorem

cyclicExtensionDegree_dvd_narrowFiniteConductorRayClassGroup_card

L66 ↗

GlobalClassFieldTheory.GlobalClassFields.cyclicExtensionDegree_dvd_narrowFiniteConductorRayClassGroup_card