Module

NormLimitation.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.NormLimitation

5 declarations indexed from sourceView source ↗

Module documentation

Ideal and ray consequences of norm limitation

For a finite extension L / K, norm limitation identifies its idèle-class norm range with that of the maximal abelian subfield in the chosen finite normal closure. This leaf transports that equality to the corresponding ideal norm group for every defining modulus and to the image of the norm range in every ray class group.

Imports1

Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.NormLimitationCore

Imported by1

Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.All

theorem

normLimitationIdeleClassIsMulCommutative

L26 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.normLimitationIdeleClassIsMulCommutative

Source context 4 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory

Lean source · statement

theorem normLimitationIdeleClassIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)

def

rayNormSubgroup

L41 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.rayNormSubgroup

Documentation

The norm subgroup in the ray class group is the image of the actual idèle-class norm range modulo the ray congruence subgroup.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
attribute [local instance] normLimitationIdeleClassIsMulCommutative
variable
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]

Lean source · statement

def rayNormSubgroup (m : RayClass.Modulus K) :
    Subgroup (RayClass.RayClassGroup m)

theorem

rayNormSubgroup_eq_rayClassToNormQuotient_ker

L52 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.rayNormSubgroup_eq_rayClassToNormQuotient_ker

Documentation

For a defining modulus, the ray norm subgroup is exactly the kernel of the canonical map from the ray class group to the idèle-class norm quotient.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
attribute [local instance] normLimitationIdeleClassIsMulCommutative
variable
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [FiniteDimensional K L] in

Lean source · statement

theorem rayNormSubgroup_eq_rayClassToNormQuotient_ker
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range) :
    rayNormSubgroup K L m =
      (rayClassToNormQuotient m
        ((_root_.ideleClassNorm K L).range) hm).ker

theorem

idealNormSubgroup_eq_maximalAbelianSubfield

L76 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.idealNormSubgroup_eq_maximalAbelianSubfield

Documentation

Ideal norm limitation: for every defining modulus, the genuine ideal norm group of a finite extension equals that of its maximal abelian subfield in the chosen finite normal closure.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
attribute [local instance] normLimitationIdeleClassIsMulCommutative
variable
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]

Lean source · statement

theorem idealNormSubgroup_eq_maximalAbelianSubfield
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range) :
    idealNormSubgroupMaximalAbelianStatement K L m hm

theorem

rayNormSubgroup_eq_maximalAbelianSubfield

L87 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.rayNormSubgroup_eq_maximalAbelianSubfield

Documentation

Ray norm limitation: the image of a finite extension's idèle-class norm range in every ray class group is already the image of the norm range from its maximal abelian subfield.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
attribute [local instance] normLimitationIdeleClassIsMulCommutative
variable
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]

Lean source · statement

theorem rayNormSubgroup_eq_maximalAbelianSubfield
    (m : RayClass.Modulus K) :
    rayNormSubgroup K L m =
      rayNormSubgroup K
        (finiteNormalClosureMaximalAbelianSubfield K L) m

Module documentation

Ideal and ray consequences of norm limitation

Declarations

normLimitationIdeleClassIsMulCommutative

rayNormSubgroup

rayNormSubgroup_eq_rayClassToNormQuotient_ker

idealNormSubgroup_eq_maximalAbelianSubfield

rayNormSubgroup_eq_maximalAbelianSubfield