NYLL
Module

CyclicConductorUniqueness.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.CyclicConductorUniqueness
6 declarations indexed from sourceView source ↗

Module documentation

Uniqueness of maximal cyclic norm subgroups at a narrow finite conductor

Two finite cyclic extensions whose exact narrow finite conductors agree and whose degrees exhaust the corresponding ray class number determine the same actual idèle-class norm subgroup. Thus their concrete norm quotients are canonically equivalent. This is the norm-subgroup uniqueness part of the cyclic class-field correspondence at a fixed narrow finite conductor.

Imports1
Imported by1

Declarations

theorem

cyclicConductorUniquenessIdeleClassIsMulCommutative

L28 ↗
GlobalClassFieldTheory.GlobalClassFields.cyclicConductorUniquenessIdeleClassIsMulCommutative
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 cyclicConductorUniquenessIdeleClassIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)
theorem

cyclicIdeleClassNorm_ranges_eq_of_narrowFiniteConductors_eq_of_rayClassCards_eq_degrees

L47 ↗
GlobalClassFieldTheory.GlobalClassFields.cyclicIdeleClassNorm_ranges_eq_of_narrowFiniteConductors_eq_of_rayClassCards_eq_degrees
Documentation

Maximal cyclic extensions with the same exact narrow finite conductor 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] cyclicConductorUniquenessIdeleClassIsMulCommutative
variable
    {K L M : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [Field M] [NumberField M] [Algebra K M]
    [FiniteDimensional K L] [IsGalois K L]
    [FiniteDimensional K M] [IsGalois K M]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsCyclic (M ≃ₐ[K] M)]
Lean source · statement
theorem
    cyclicIdeleClassNorm_ranges_eq_of_narrowFiniteConductors_eq_of_rayClassCards_eq_degrees
    (hconductor :
      ideleClassNormNarrowFiniteConductor (K := K) (L := L) =
        ideleClassNormNarrowFiniteConductor (K := K) (L := M))
    (hLcard :
      Nat.card
          (RayClass.RayClassGroup
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))) =
        Module.finrank K L)
    (hMcard :
      Nat.card
          (RayClass.RayClassGroup
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor (K := K) (L := M)))) =
        Module.finrank K M) :
    (_root_.ideleClassNorm K L).range =
      (_root_.ideleClassNorm K M).range
def

cyclicNormQuotientEquivOfNarrowFiniteConductorsEqOfRayClassGroupCardsEqExtensionDegrees

L87 ↗
GlobalClassFieldTheory.GlobalClassFields.cyclicNormQuotientEquivOfNarrowFiniteConductorsEqOfRayClassGroupCardsEqExtensionDegrees
Documentation

The actual norm quotients of two maximal cyclic extensions with the same exact narrow finite 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] cyclicConductorUniquenessIdeleClassIsMulCommutative
variable
    {K L M : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [Field M] [NumberField M] [Algebra K M]
    [FiniteDimensional K L] [IsGalois K L]
    [FiniteDimensional K M] [IsGalois K M]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsCyclic (M ≃ₐ[K] M)]
Lean source · statement
def cyclicNormQuotientEquivOfNarrowFiniteConductorsEqOfRayClassGroupCardsEqExtensionDegrees
    (hconductor :
      ideleClassNormNarrowFiniteConductor (K := K) (L := L) =
        ideleClassNormNarrowFiniteConductor (K := K) (L := M))
    (hLcard :
      Nat.card
          (RayClass.RayClassGroup
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))) =
        Module.finrank K L)
    (hMcard :
      Nat.card
          (RayClass.RayClassGroup
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor (K := K) (L := M)))) =
        Module.finrank K M) :
    (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) ≃*
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K M).range)
theorem

cyclicNormQuotientEquivOfNarrowFiniteConductorsEqOfRayClassGroupCardsEqExtensionDegrees_mk

L115 ↗
GlobalClassFieldTheory.GlobalClassFields.cyclicNormQuotientEquivOfNarrowFiniteConductorsEqOfRayClassGroupCardsEqExtensionDegrees_mk
Documentation

The canonical equivalence between the two maximal cyclic 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] cyclicConductorUniquenessIdeleClassIsMulCommutative
variable
    {K L M : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [Field M] [NumberField M] [Algebra K M]
    [FiniteDimensional K L] [IsGalois K L]
    [FiniteDimensional K M] [IsGalois K M]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsCyclic (M ≃ₐ[K] M)]
Lean source · statement
theorem
    cyclicNormQuotientEquivOfNarrowFiniteConductorsEqOfRayClassGroupCardsEqExtensionDegrees_mk
    (hconductor :
      ideleClassNormNarrowFiniteConductor (K := K) (L := L) =
        ideleClassNormNarrowFiniteConductor (K := K) (L := M))
    (hLcard :
      Nat.card
          (RayClass.RayClassGroup
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))) =
        Module.finrank K L)
    (hMcard :
      Nat.card
          (RayClass.RayClassGroup
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor (K := K) (L := M)))) =
        Module.finrank K M)
    (c : IdeleClassGroup K) :
    cyclicNormQuotientEquivOfNarrowFiniteConductorsEqOfRayClassGroupCardsEqExtensionDegrees
        (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
theorem

nestedMaximalCyclicExtensions_sameNarrowFiniteConductor_relativeDegree_eq_one

L147 ↗
GlobalClassFieldTheory.GlobalClassFields.nestedMaximalCyclicExtensions_sameNarrowFiniteConductor_relativeDegree_eq_one
Documentation

If two nested cyclic extensions have the same exact narrow finite conductor and both exhaust its ray class group, then the upper extension has relative degree one. Thus a maximal cyclic class field at a fixed narrow finite conductor has no proper nested cyclic overextension with the same 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] cyclicConductorUniquenessIdeleClassIsMulCommutative
variable
    {K L M : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [Field M] [NumberField M] [Algebra K M]
    [FiniteDimensional K L] [IsGalois K L]
    [FiniteDimensional K M] [IsGalois K M]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsCyclic (M ≃ₐ[K] M)]
Lean source · statement
theorem
    nestedMaximalCyclicExtensions_sameNarrowFiniteConductor_relativeDegree_eq_one
    [Algebra M L] [IsScalarTower K M L]
    [FiniteDimensional M L]
    (hconductor :
      ideleClassNormNarrowFiniteConductor (K := K) (L := L) =
        ideleClassNormNarrowFiniteConductor (K := K) (L := M))
    (hLcard :
      Nat.card
          (RayClass.RayClassGroup
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))) =
        Module.finrank K L)
    (hMcard :
      Nat.card
          (RayClass.RayClassGroup
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor (K := K) (L := M)))) =
        Module.finrank K M) :
    Module.finrank M L = 1
theorem

nestedMaximalCyclicExtensions_narrowFiniteConductors_ne_of_relativeDegree_ne_one

L202 ↗
GlobalClassFieldTheory.GlobalClassFields.nestedMaximalCyclicExtensions_narrowFiniteConductors_ne_of_relativeDegree_ne_one
Documentation

A proper nested cyclic overextension cannot remain maximal at the same exact narrow finite conductor. Hence maximal cyclic class fields in a proper tower have distinct narrow finite conductors.

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] cyclicConductorUniquenessIdeleClassIsMulCommutative
variable
    {K L M : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [Field M] [NumberField M] [Algebra K M]
    [FiniteDimensional K L] [IsGalois K L]
    [FiniteDimensional K M] [IsGalois K M]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsCyclic (M ≃ₐ[K] M)]
Lean source · statement
theorem
    nestedMaximalCyclicExtensions_narrowFiniteConductors_ne_of_relativeDegree_ne_one
    [Algebra M L] [IsScalarTower K M L]
    [FiniteDimensional M L]
    (hLcard :
      Nat.card
          (RayClass.RayClassGroup
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))) =
        Module.finrank K L)
    (hMcard :
      Nat.card
          (RayClass.RayClassGroup
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor (K := K) (L := M)))) =
        Module.finrank K M)
    (hrelativeDegree :
      Module.finrank M L ≠ 1) :
    ideleClassNormNarrowFiniteConductor (K := K) (L := L) ≠
      ideleClassNormNarrowFiniteConductor (K := K) (L := M)

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