NYLL
Module

ConductorRayClassMaximality.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ConductorRayClassMaximality
15 declarations indexed from sourceView source ↗

Module documentation

Exact narrow finite conductor ray-class presentations

For a conductorial subgroup H of the idèle class group, the ray class group at its exact narrow finite conductor maps canonically onto C_K / H. This file characterizes injectivity of that map by equality of the two finite orders and proves uniqueness of subgroups whose exact narrow finite conductor ray-class presentations are maximal.

Imports1
Imported by3

Declarations

instance

conductorRayClassMaximality_ideleClassGroupIsMulCommutative

L34 ↗
GlobalClassFieldTheory.GlobalClassFields.conductorRayClassMaximality_ideleClassGroupIsMulCommutative
Documentation

Fix the canonical commutative structure used to infer normality of subgroups of the idèle class group in this module.

Source context 6 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
instance
    conductorRayClassMaximality_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K)
def

narrowFiniteConductorRayClassGroupToQuotient

L43 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductorRayClassGroupToQuotient
Documentation

The canonical quotient map from the ray class group at the exact narrow finite conductor of H onto C_K / H.

Source context 8 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type} [Field K] [NumberField K]
/-- Fix the canonical commutative structure used to infer normality of
subgroups of the idèle class group in this module. -/
local instance
    conductorRayClassMaximality_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
namespace ConductorialSubgroup
Lean source · statement
def narrowFiniteConductorRayClassGroupToQuotient
    (H : ConductorialSubgroup K) :
    RayClass.RayClassGroup
        (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor) →*
      IdeleClassGroup K ⧸ H.1
theorem

narrowFiniteConductorRayClassGroupToQuotient_mk

L64 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductorRayClassGroupToQuotient_mk
Documentation

The exact narrow finite conductor quotient map preserves every idèle-class representative.

Source context 8 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type} [Field K] [NumberField K]
/-- Fix the canonical commutative structure used to infer normality of
subgroups of the idèle class group in this module. -/
local instance
    conductorRayClassMaximality_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
namespace ConductorialSubgroup
Lean source · statement
theorem narrowFiniteConductorRayClassGroupToQuotient_mk
    (H : ConductorialSubgroup K)
    (c : IdeleClassGroup K) :
    H.narrowFiniteConductorRayClassGroupToQuotient
      (QuotientGroup.mk'
          (RayClass.Modulus.congruenceSubgroup
            (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor)) c) =
      QuotientGroup.mk' H.1 c
theorem

narrowFiniteConductorRayClassGroupToQuotient_surjective

L76 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductorRayClassGroupToQuotient_surjective
Documentation

The exact narrow finite conductor ray-class map onto C_K / H is surjective.

Source context 8 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type} [Field K] [NumberField K]
/-- Fix the canonical commutative structure used to infer normality of
subgroups of the idèle class group in this module. -/
local instance
    conductorRayClassMaximality_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
namespace ConductorialSubgroup
Lean source · statement
theorem narrowFiniteConductorRayClassGroupToQuotient_surjective
    (H : ConductorialSubgroup K) :
    Function.Surjective H.narrowFiniteConductorRayClassGroupToQuotient
theorem

narrowFiniteConductorRayClassGroupToQuotient_ker

L90 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductorRayClassGroupToQuotient_ker
Documentation

The kernel of the exact narrow finite conductor ray-class map is the image of H modulo the conductor congruence subgroup.

Source context 8 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type} [Field K] [NumberField K]
/-- Fix the canonical commutative structure used to infer normality of
subgroups of the idèle class group in this module. -/
local instance
    conductorRayClassMaximality_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
namespace ConductorialSubgroup
Lean source · statement
theorem narrowFiniteConductorRayClassGroupToQuotient_ker
    (H : ConductorialSubgroup K) :
    MonoidHom.ker H.narrowFiniteConductorRayClassGroupToQuotient =
      Subgroup.map
        (QuotientGroup.mk'
          (RayClass.Modulus.congruenceSubgroup
            (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor)))
        H.1
def

narrowFiniteConductorRayClassSubgroupQuotientEquivIdeleClassQuotient

L114 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductorRayClassSubgroupQuotientEquivIdeleClassQuotient
Documentation

Quotienting the exact narrow finite conductor ray class group by the image of H recovers C_K / H.

Source context 8 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type} [Field K] [NumberField K]
/-- Fix the canonical commutative structure used to infer normality of
subgroups of the idèle class group in this module. -/
local instance
    conductorRayClassMaximality_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
namespace ConductorialSubgroup
Lean source · statement
def
    narrowFiniteConductorRayClassSubgroupQuotientEquivIdeleClassQuotient
    (H : ConductorialSubgroup K) :
    (RayClass.RayClassGroup
        (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor) ⧸
        Subgroup.map
          (QuotientGroup.mk'
            (RayClass.Modulus.congruenceSubgroup
              (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor)))
          H.1) ≃*
      IdeleClassGroup K ⧸ H.1
theorem

narrowFiniteConductorRayClassGroup_card_eq_subgroupImage_card_mul_quotient_card

L134 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductorRayClassGroup_card_eq_subgroupImage_card_mul_quotient_card
Documentation

The exact narrow finite conductor ray class number factors as the order of the image of H modulo conductor congruence times the order of C_K / H.

Source context 8 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type} [Field K] [NumberField K]
/-- Fix the canonical commutative structure used to infer normality of
subgroups of the idèle class group in this module. -/
local instance
    conductorRayClassMaximality_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
namespace ConductorialSubgroup
Lean source · statement
theorem
    narrowFiniteConductorRayClassGroup_card_eq_subgroupImage_card_mul_quotient_card
    (H : ConductorialSubgroup K) :
    Nat.card (RayClass.RayClassGroup
      (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor)) =
      Nat.card
          (Subgroup.map
            (QuotientGroup.mk'
              (RayClass.Modulus.congruenceSubgroup
                (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor)))
            H.1) *
        Nat.card (IdeleClassGroup K ⧸ H.1)
theorem

ideleClassQuotient_card_dvd_narrowFiniteConductorRayClassGroup_card

L172 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.ideleClassQuotient_card_dvd_narrowFiniteConductorRayClassGroup_card
Documentation

The order of C_K / H divides the ray class number at the exact narrow finite conductor of H.

Source context 8 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type} [Field K] [NumberField K]
/-- Fix the canonical commutative structure used to infer normality of
subgroups of the idèle class group in this module. -/
local instance
    conductorRayClassMaximality_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
namespace ConductorialSubgroup
Lean source · statement
theorem ideleClassQuotient_card_dvd_narrowFiniteConductorRayClassGroup_card
    (H : ConductorialSubgroup K) :
      Nat.card (IdeleClassGroup K ⧸ H.1) ∣
      Nat.card (RayClass.RayClassGroup
        (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor))
theorem

narrowFiniteConductorRayClassGroupToQuotient_injective_iff_card_eq

L182 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductorRayClassGroupToQuotient_injective_iff_card_eq
Documentation

The exact narrow finite conductor ray-class map is injective exactly when its finite source and target have the same order.

Source context 8 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type} [Field K] [NumberField K]
/-- Fix the canonical commutative structure used to infer normality of
subgroups of the idèle class group in this module. -/
local instance
    conductorRayClassMaximality_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
namespace ConductorialSubgroup
Lean source · statement
theorem narrowFiniteConductorRayClassGroupToQuotient_injective_iff_card_eq
    (H : ConductorialSubgroup K) :
    Function.Injective H.narrowFiniteConductorRayClassGroupToQuotient ↔
      Nat.card (RayClass.RayClassGroup
        (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor)) =
        Nat.card (IdeleClassGroup K ⧸ H.1)
def

narrowFiniteConductorRayClassGroupEquivQuotientOfCardEq

L204 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductorRayClassGroupEquivQuotientOfCardEq
Documentation

When the exact narrow finite conductor ray class group and C_K / H have the same order, the canonical quotient map is a multiplicative equivalence.

Source context 8 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type} [Field K] [NumberField K]
/-- Fix the canonical commutative structure used to infer normality of
subgroups of the idèle class group in this module. -/
local instance
    conductorRayClassMaximality_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
namespace ConductorialSubgroup
Lean source · statement
def narrowFiniteConductorRayClassGroupEquivQuotientOfCardEq
    (H : ConductorialSubgroup K)
    (hcard :
      Nat.card (RayClass.RayClassGroup
        (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor)) =
        Nat.card (IdeleClassGroup K ⧸ H.1)) :
    RayClass.RayClassGroup
        (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor) ≃*
      IdeleClassGroup K ⧸ H.1
theorem

narrowFiniteConductorRayClassGroupEquivQuotientOfCardEq_mk

L222 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductorRayClassGroupEquivQuotientOfCardEq_mk
Documentation

The maximal exact narrow finite conductor equivalence preserves every idèle-class representative.

Source context 8 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type} [Field K] [NumberField K]
/-- Fix the canonical commutative structure used to infer normality of
subgroups of the idèle class group in this module. -/
local instance
    conductorRayClassMaximality_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
namespace ConductorialSubgroup
Lean source · statement
theorem narrowFiniteConductorRayClassGroupEquivQuotientOfCardEq_mk
    (H : ConductorialSubgroup K)
    (hcard :
      Nat.card (RayClass.RayClassGroup
        (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor)) =
        Nat.card (IdeleClassGroup K ⧸ H.1))
    (c : IdeleClassGroup K) :
    H.narrowFiniteConductorRayClassGroupEquivQuotientOfCardEq
        hcard
      (QuotientGroup.mk'
          (RayClass.Modulus.congruenceSubgroup
            (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor)) c) =
      QuotientGroup.mk' H.1 c
theorem

subgroup_eq_narrowFiniteConductorCongruenceSubgroup_iff_rayClassGroup_card_eq_quotient_card

L240 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.subgroup_eq_narrowFiniteConductorCongruenceSubgroup_iff_rayClassGroup_card_eq_quotient_card
Documentation

A conductorial subgroup is exactly the congruence subgroup at its narrow finite conductor precisely when its quotient has the full exact narrow finite conductor ray class number.

Source context 8 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type} [Field K] [NumberField K]
/-- Fix the canonical commutative structure used to infer normality of
subgroups of the idèle class group in this module. -/
local instance
    conductorRayClassMaximality_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
namespace ConductorialSubgroup
Lean source · statement
theorem
    subgroup_eq_narrowFiniteConductorCongruenceSubgroup_iff_rayClassGroup_card_eq_quotient_card
    (H : ConductorialSubgroup K) :
    H.1 = RayClass.Modulus.congruenceSubgroup
      (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor) ↔
      Nat.card (RayClass.RayClassGroup
        (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor)) =
        Nat.card (IdeleClassGroup K ⧸ H.1)
theorem

subgroups_eq_of_narrowFiniteConductors_eq_of_rayClassGroup_cards_eq_quotient_cards

L287 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.subgroups_eq_of_narrowFiniteConductors_eq_of_rayClassGroup_cards_eq_quotient_cards
Documentation

Conductorial subgroups with the same exact narrow finite conductor and maximal exact-conductor ray-class presentations have equal underlying subgroups.

Source context 8 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type} [Field K] [NumberField K]
/-- Fix the canonical commutative structure used to infer normality of
subgroups of the idèle class group in this module. -/
local instance
    conductorRayClassMaximality_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
namespace ConductorialSubgroup
Lean source · statement
theorem
    subgroups_eq_of_narrowFiniteConductors_eq_of_rayClassGroup_cards_eq_quotient_cards
    (H J : ConductorialSubgroup K)
    (hconductor : H.narrowFiniteConductor = J.narrowFiniteConductor)
    (hHcard :
      Nat.card (RayClass.RayClassGroup
        (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor)) =
        Nat.card (IdeleClassGroup K ⧸ H.1))
    (hJcard :
      Nat.card (RayClass.RayClassGroup
        (RayClass.Modulus.narrowOfFinite J.narrowFiniteConductor)) =
        Nat.card (IdeleClassGroup K ⧸ J.1)) :
    H.1 = J.1
def

ideleClassQuotientEquivOfNarrowFiniteConductorsEqOfRayClassGroupCardsEqQuotientCards

L318 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.ideleClassQuotientEquivOfNarrowFiniteConductorsEqOfRayClassGroupCardsEqQuotientCards
Documentation

The quotients by two maximal exact narrow finite conductor subgroups with the same conductor are canonically equivalent.

Source context 8 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type} [Field K] [NumberField K]
/-- Fix the canonical commutative structure used to infer normality of
subgroups of the idèle class group in this module. -/
local instance
    conductorRayClassMaximality_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
namespace ConductorialSubgroup
Lean source · statement
def ideleClassQuotientEquivOfNarrowFiniteConductorsEqOfRayClassGroupCardsEqQuotientCards
    (H J : ConductorialSubgroup K)
    (hconductor : H.narrowFiniteConductor = J.narrowFiniteConductor)
    (hHcard :
      Nat.card (RayClass.RayClassGroup
        (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor)) =
        Nat.card (IdeleClassGroup K ⧸ H.1))
    (hJcard :
      Nat.card (RayClass.RayClassGroup
        (RayClass.Modulus.narrowOfFinite J.narrowFiniteConductor)) =
        Nat.card (IdeleClassGroup K ⧸ J.1)) :
    (IdeleClassGroup K ⧸ H.1) ≃*
      (IdeleClassGroup K ⧸ J.1)
theorem

ideleClassQuotientEquivOfNarrowFiniteConductorsEqOfRayClassGroupCardsEqQuotientCards_mk

L338 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.ideleClassQuotientEquivOfNarrowFiniteConductorsEqOfRayClassGroupCardsEqQuotientCards_mk
Documentation

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

Source context 8 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type} [Field K] [NumberField K]
/-- Fix the canonical commutative structure used to infer normality of
subgroups of the idèle class group in this module. -/
local instance
    conductorRayClassMaximality_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
namespace ConductorialSubgroup
Lean source · statement
theorem
    ideleClassQuotientEquivOfNarrowFiniteConductorsEqOfRayClassGroupCardsEqQuotientCards_mk
    (H J : ConductorialSubgroup K)
    (hconductor : H.narrowFiniteConductor = J.narrowFiniteConductor)
    (hHcard :
      Nat.card (RayClass.RayClassGroup
        (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor)) =
        Nat.card (IdeleClassGroup K ⧸ H.1))
    (hJcard :
      Nat.card (RayClass.RayClassGroup
        (RayClass.Modulus.narrowOfFinite J.narrowFiniteConductor)) =
        Nat.card (IdeleClassGroup K ⧸ J.1))
    (c : IdeleClassGroup K) :
    H.ideleClassQuotientEquivOfNarrowFiniteConductorsEqOfRayClassGroupCardsEqQuotientCards
        J hconductor hHcard hJcard
        (QuotientGroup.mk' H.1 c) =
      QuotientGroup.mk' J.1 c

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