NYLL
Module

NormRayClassMaximality.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.NormRayClassMaximality
7 declarations indexed from sourceView source ↗

Module documentation

Exact narrow finite ray-class presentations of norm quotients

For every finite Galois extension, the ray class group at the exact narrow finite conductor surjects onto the actual idèle-class norm quotient. This file characterizes when that presentation has no residual kernel: the norm subgroup is then exactly the congruence subgroup at its narrow finite conductor, equivalently the two finite quotient groups have the same order.

Imports1
Imported by2

Declarations

theorem

normRayClassMaximalityClassGroupIsMulCommutative

L31 ↗
GlobalClassFieldTheory.GlobalClassFields.normRayClassMaximalityClassGroupIsMulCommutative
Documentation

Canonical class-group commutativity supplies normality for the quotient.

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 normRayClassMaximalityClassGroupIsMulCommutative
    (F : Type*) [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)
theorem

ideleClassNorm_range_eq_narrowConductorSubgroup_iff_rayClass_card_eq_normQuotient_card

L47 ↗
GlobalClassFieldTheory.GlobalClassFields.ideleClassNorm_range_eq_narrowConductorSubgroup_iff_rayClass_card_eq_normQuotient_card
Documentation

The actual idèle-class norm subgroup is exactly the ray congruence subgroup at its narrow finite conductor if and only if the conductor ray class group and the actual norm quotient have the same order.

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] normRayClassMaximalityClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem
    ideleClassNorm_range_eq_narrowConductorSubgroup_iff_rayClass_card_eq_normQuotient_card :
    (_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)))) =
        Nat.card
          (IdeleClassGroup K ⧸
            (_root_.ideleClassNorm K L).range)
theorem

narrowFiniteConductorRayClassGroupToIdeleClassNormQuotient_injective_iff_card_eq_normQuotient_card

L105 ↗
GlobalClassFieldTheory.GlobalClassFields.narrowFiniteConductorRayClassGroupToIdeleClassNormQuotient_injective_iff_card_eq_normQuotient_card
Documentation

The canonical narrow finite conductor ray-class map to the actual idèle-class norm quotient is injective if and only if its finite source and target have the same order.

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] normRayClassMaximalityClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem
  narrowFiniteConductorRayClassGroupToIdeleClassNormQuotient_injective_iff_card_eq_normQuotient_card
    :
    Function.Injective
        (narrowFiniteConductorRayClassGroupToIdeleClassNormQuotient
          (K := K) (L := L)) ↔
      Nat.card
          (RayClass.RayClassGroup
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor
                (K := K) (L := L)))) =
        Nat.card
          (IdeleClassGroup K ⧸
            (_root_.ideleClassNorm K L).range)
def

normQuotientEquivNarrowFiniteConductorRayClassGroup

L139 ↗
GlobalClassFieldTheory.GlobalClassFields.normQuotientEquivNarrowFiniteConductorRayClassGroup
Documentation

If the narrow finite conductor ray class group and the actual idèle-class norm quotient have the same order, the latter is canonically the full ray class group at its narrow finite 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] normRayClassMaximalityClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def normQuotientEquivNarrowFiniteConductorRayClassGroup
    (hcard :
      Nat.card
          (RayClass.RayClassGroup
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor
                (K := K) (L := L)))) =
        Nat.card
          (IdeleClassGroup K ⧸
            (_root_.ideleClassNorm K L).range)) :
    (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) ≃*
      RayClass.RayClassGroup
        (RayClass.Modulus.narrowOfFinite
          (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))
theorem

ideleClassNorm_ranges_eq_of_narrowFiniteConductors_eq_of_rayClassGroup_cards_eq_normQuotient_cards

L161 ↗
GlobalClassFieldTheory.GlobalClassFields.ideleClassNorm_ranges_eq_of_narrowFiniteConductors_eq_of_rayClassGroup_cards_eq_normQuotient_cards
Documentation

Two finite Galois extensions with the same exact narrow finite conductor and maximal ray-class presentations have the same actual idèle-class norm subgroup.

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] normRayClassMaximalityClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem
  ideleClassNorm_ranges_eq_of_narrowFiniteConductors_eq_of_rayClassGroup_cards_eq_normQuotient_cards
    {M : Type}
    [Field M] [NumberField M] [Algebra K M]
    [FiniteDimensional K M] [IsGalois K M]
    (hconductor :
      ideleClassNormNarrowFiniteConductor (K := K) (L := L) =
        ideleClassNormNarrowFiniteConductor (K := K) (L := M))
    (hLcard :
      Nat.card
          (RayClass.RayClassGroup
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor
                (K := K) (L := L)))) =
        Nat.card
          (IdeleClassGroup K ⧸
            (_root_.ideleClassNorm K L).range))
    (hMcard :
      Nat.card
          (RayClass.RayClassGroup
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor
                (K := K) (L := M)))) =
        Nat.card
          (IdeleClassGroup K ⧸
            (_root_.ideleClassNorm K M).range)) :
    (_root_.ideleClassNorm K L).range =
      (_root_.ideleClassNorm K M).range
def

normQuotientEquivOfNarrowFiniteConductorsEqOfRayClassGroupCardsEqNormQuotientCards

L211 ↗
GlobalClassFieldTheory.GlobalClassFields.normQuotientEquivOfNarrowFiniteConductorsEqOfRayClassGroupCardsEqNormQuotientCards
Documentation

The actual norm quotients of two maximal narrow finite conductor ray-class presentations with the same conductor are canonically equivalent.

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] normRayClassMaximalityClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def normQuotientEquivOfNarrowFiniteConductorsEqOfRayClassGroupCardsEqNormQuotientCards
    {M : Type}
    [Field M] [NumberField M] [Algebra K M]
    [FiniteDimensional K M] [IsGalois K M]
    (hconductor :
      ideleClassNormNarrowFiniteConductor (K := K) (L := L) =
        ideleClassNormNarrowFiniteConductor (K := K) (L := M))
    (hLcard :
      Nat.card
          (RayClass.RayClassGroup
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor
                (K := K) (L := L)))) =
        Nat.card
          (IdeleClassGroup K ⧸
            (_root_.ideleClassNorm K L).range))
    (hMcard :
      Nat.card
          (RayClass.RayClassGroup
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor
                (K := K) (L := M)))) =
        Nat.card
          (IdeleClassGroup K ⧸
            (_root_.ideleClassNorm K M).range)) :
    (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) ≃*
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K M).range)
theorem

normQuotientEquivOfNarrowFiniteConductorsEqOfRayClassGroupCardsEqNormQuotientCards_mk

L249 ↗
GlobalClassFieldTheory.GlobalClassFields.normQuotientEquivOfNarrowFiniteConductorsEqOfRayClassGroupCardsEqNormQuotientCards_mk
Documentation

The canonical equivalence between maximal narrow finite conductor ray-class norm quotients preserves every idèle-class representative.

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] normRayClassMaximalityClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem
    normQuotientEquivOfNarrowFiniteConductorsEqOfRayClassGroupCardsEqNormQuotientCards_mk
    {M : Type}
    [Field M] [NumberField M] [Algebra K M]
    [FiniteDimensional K M] [IsGalois K M]
    (hconductor :
      ideleClassNormNarrowFiniteConductor (K := K) (L := L) =
        ideleClassNormNarrowFiniteConductor (K := K) (L := M))
    (hLcard :
      Nat.card
          (RayClass.RayClassGroup
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor
                (K := K) (L := L)))) =
        Nat.card
          (IdeleClassGroup K ⧸
            (_root_.ideleClassNorm K L).range))
    (hMcard :
      Nat.card
          (RayClass.RayClassGroup
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor
                (K := K) (L := M)))) =
        Nat.card
          (IdeleClassGroup K ⧸
            (_root_.ideleClassNorm K M).range))
    (c : IdeleClassGroup K) :
    normQuotientEquivOfNarrowFiniteConductorsEqOfRayClassGroupCardsEqNormQuotientCards
        (K := K) (L := L) (M := M)
        hconductor hLcard hMcard
        (QuotientGroup.mk'
          ((_root_.ideleClassNorm K L).range) c) =
      QuotientGroup.mk'
        ((_root_.ideleClassNorm K M).range) c

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