Module

ClassGroup.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.ClassGroup

10 declarations indexed from sourceView source ↗

Module documentation

Idele classes in finite extensions

The tensor-product model makes the key intersection calculation

I_K ∩ Lˣ = Kˣ

an elementary linear-algebra statement. A linear retraction of K → 𝔸_K shows that an equality a ⊗ 1 = 1 ⊗ x forces both factors to come from the same scalar in K. We then descend the idele inclusion to quotients and prove it injective.

Imports2

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.NormProperties
Mathlib.LinearAlgebra.Basis.VectorSpace

Imported by5

theorem

exists_scalar_of_adeleInclusion_eq_fieldInclusion

L41 ↗

RelativeIdeleGroup.exists_scalar_of_adeleInclusion_eq_fieldInclusion

Documentation

If a base adele and an extension-field element define the same element of 𝔸_K ⊗_K L, then they arise from one scalar of K.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
omit [NumberField L] [FiniteDimensional K L] in

Lean source · statement

theorem exists_scalar_of_adeleInclusion_eq_fieldInclusion
    (a : NumberField.AdeleRing (𝓞 K) K) (x : L)
    (h : adeleInclusion K L a = fieldInclusion K L x) :
    ∃ k : K,
      a = algebraMap K (NumberField.AdeleRing (𝓞 K) K) k ∧
      x = algebraMap K L k

def

principalSubgroup

L86 ↗

RelativeIdeleGroup.principalSubgroup

Documentation

The subgroup of principal relative ideles.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup

Lean source · statement

def principalSubgroup :
    Subgroup (RelativeIdeleGroup K L)

abbrev

ClassGroup

L92 ↗

RelativeIdeleGroup.ClassGroup

Documentation

The relative idele class group in the canonical presentation 𝔸_L = 𝔸_K ⊗_K L.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup

Lean source · statement

abbrev ClassGroup

theorem

comap_principalSubgroup

L98 ↗

RelativeIdeleGroup.comap_principalSubgroup

Documentation

The preimage of the principal relative ideles under I_K → I_L is exactly the subgroup of principal ideles of K.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
omit [NumberField L] [FiniteDimensional K L] in

Lean source · statement

theorem comap_principalSubgroup :
    Subgroup.comap (inclusion K L)
        (principalSubgroup K L) =
      IdeleGroup.principalSubgroup K

def

classInclusion

L136 ↗

RelativeIdeleGroup.classInclusion

Documentation

Inclusion of ideles descends to inclusion of idele classes.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup

Lean source · statement

def classInclusion :
    IdeleClassGroup K →* ClassGroup K L

theorem

classInclusion_mk

L147 ↗

RelativeIdeleGroup.classInclusion_mk

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
omit [NumberField L] [FiniteDimensional K L] in

Lean source · statement

theorem classInclusion_mk (a : IdeleGroup K) :
    classInclusion K L
        (QuotientGroup.mk' (IdeleGroup.principalSubgroup K) a) =
      QuotientGroup.mk' (principalSubgroup K L)
        (inclusion K L a)

def

classNorm

L156 ↗

RelativeIdeleGroup.classNorm

Documentation

The determinant norm on relative ideles, descended to their relative idele-class presentation.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup

Lean source · statement

def classNorm :
    ClassGroup K L →* IdeleClassGroup K

theorem

classNorm_mk

L172 ↗

RelativeIdeleGroup.classNorm_mk

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
omit [NumberField L] in

Lean source · statement

theorem classNorm_mk
    (a : RelativeIdeleGroup K L) :
    classNorm K L
        (QuotientGroup.mk' (principalSubgroup K L) a) =
      QuotientGroup.mk'
        (IdeleGroup.principalSubgroup K)
        (RelativeIdeleGroup.norm K L a)

abbrev

ClassNormQuotient

L182 ↗

RelativeIdeleGroup.ClassNormQuotient

Documentation

The norm quotient in the relative idele-class presentation.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup

Lean source · statement

abbrev ClassNormQuotient

theorem

classInclusion_injective

L187 ↗

RelativeIdeleGroup.classInclusion_injective

Documentation

The scalar-extension map C_K → C_L is injective.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
omit [NumberField L] [FiniteDimensional K L] in

Lean source · statement

theorem classInclusion_injective :
    Function.Injective (classInclusion K L)

Module documentation

Idele classes in finite extensions

Declarations