Module

PrincipalIdealTheorem.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.PrincipalIdealTheorem

4 declarations indexed from sourceView source ↗

Module documentation

The principal ideal theorem

This file descends genuine idele extension to the reciprocity quotients defining the two small Hilbert class fields and proves that the resulting map forms the naturality square with the existing ideal-class extension ClassGroup.extendedHom.

Imports3

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.IdealClass
Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.HilbertClassFieldComparison
Mathlib.RingTheory.ClassGroup.ExtendedHom

Imported by2

theorem

principalIdealTheoremClassGroupIsMulCommutative

L32 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.principalIdealTheoremClassGroupIsMulCommutative

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 IdealClassFieldTheory
open NumberField

Lean source · statement

theorem principalIdealTheoremClassGroupIsMulCommutative
    (F : Type*) [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)

def

smallHilbertClassFieldIdeleExtensionMap

L49 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertClassFieldIdeleExtensionMap

Documentation

The map on small-Hilbert reciprocity quotients induced by the concrete extension map on ideles.

Source context 9 commands

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

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

Lean source · statement

def smallHilbertClassFieldIdeleExtensionMap :
    (IdeleClassGroup K ⧸
        GlobalClassFields.smallHilbertClassFieldNormSubgroup) →*
      (IdeleClassGroup L ⧸
        GlobalClassFields.smallHilbertClassFieldNormSubgroup)

theorem

smallHilbertClassFieldIdeleExtensionMap_mk'

L76 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertClassFieldIdeleExtensionMap_mk'

Documentation

Evaluation of the small-Hilbert idele-extension map on a quotient representative.

Source context 9 commands

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

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

Lean source · statement

theorem smallHilbertClassFieldIdeleExtensionMap_mk'
    (c : IdeleClassGroup K) :
    smallHilbertClassFieldIdeleExtensionMap K L
        (QuotientGroup.mk'
          (GlobalClassFields.smallHilbertClassFieldNormSubgroup (K := K)) c) =
      QuotientGroup.mk'
        (GlobalClassFields.smallHilbertClassFieldNormSubgroup (K := L))
        (ideleClassExtension K L c)

theorem

smallHilbertClassFieldIdeleExtensionMap_naturality

L89 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertClassFieldIdeleExtensionMap_naturality

Documentation

The concrete idele extension and extension of ideal classes form the naturality square on the small-Hilbert quotients.

Source context 9 commands

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

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

Lean source · statement

theorem smallHilbertClassFieldIdeleExtensionMap_naturality
    (q : IdeleClassGroup K ⧸
      GlobalClassFields.smallHilbertClassFieldNormSubgroup) :
    GlobalClassFields.smallHilbertClassFieldQuotientEquivClassGroup
        (K := L)
        (smallHilbertClassFieldIdeleExtensionMap K L q) =
      ClassGroup.extendedHom (𝓞 K) (𝓞 L)
        (GlobalClassFields.smallHilbertClassFieldQuotientEquivClassGroup
          (K := K) q)

Module documentation

The principal ideal theorem

Declarations

principalIdealTheoremClassGroupIsMulCommutative

smallHilbertClassFieldIdeleExtensionMap

smallHilbertClassFieldIdeleExtensionMap_mk'

smallHilbertClassFieldIdeleExtensionMap_naturality