Module

IdeleClassBaseChange.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.IdeleClassBaseChange

5 declarations indexed from sourceView source ↗

Module documentation

Relative and ordinary idele classes

The tensor-product presentation of the ideles of a finite Galois extension is canonically equivalent to the ordinary restricted-product presentation. This file descends that equivalence through principal ideles and identifies relative class inclusion with the concrete extension map on ordinary idele classes.

Imports3

Imported by3

theorem

relativeIdelePrincipalSubgroup_map_baseChange

L37 ↗

Documentation

Scalar extension identifies the relative and ordinary principal idele subgroups.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]

Lean source · statement

theorem relativeIdelePrincipalSubgroup_map_baseChange :
    (RelativeIdeleGroup.principalSubgroup K L).map
        (relativeIdeleBaseChangeMulEquiv
          (K := K) (L := L)).toMonoidHom =
      IdeleGroup.principalSubgroup L

def

relativeIdeleClassBaseChangeMulEquiv

L60 ↗

Documentation

Scalar extension identifies the relative presentation of the idele class group with the ordinary idele class group of the extension field.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]

Lean source · statement

def relativeIdeleClassBaseChangeMulEquiv :
    RelativeIdeleGroup.ClassGroup K L ≃*
      IdeleClassGroup L

theorem

relativeIdeleClassBaseChangeMulEquiv_mk

L72 ↗

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]

Lean source · statement

theorem relativeIdeleClassBaseChangeMulEquiv_mk
    (z : RelativeIdeleGroup K L) :
    relativeIdeleClassBaseChangeMulEquiv
        (K := K) (L := L)
        (QuotientGroup.mk'
          (RelativeIdeleGroup.principalSubgroup K L) z) =
      QuotientGroup.mk'
        (IdeleGroup.principalSubgroup L)
        (relativeIdeleBaseChangeMulEquiv
          (K := K) (L := L) z)

theorem

relativeIdeleClassBaseChangeMulEquiv_classInclusion

L87 ↗

Documentation

Under the relative-to-ordinary comparison, relative class inclusion is the concrete extension map on ordinary idele classes.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]

Lean source · statement

theorem relativeIdeleClassBaseChangeMulEquiv_classInclusion
    (c : IdeleClassGroup K) :
    relativeIdeleClassBaseChangeMulEquiv
        (K := K) (L := L)
        (RelativeIdeleGroup.classInclusion K L c) =
      ideleClassExtension K L c

theorem

relativeIdeleClassBaseChange_comp_classInclusion

L99 ↗

Documentation

Homomorphism form of the compatibility between relative class inclusion and ordinary idele-class extension.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]

Lean source · statement

theorem relativeIdeleClassBaseChange_comp_classInclusion :
    (relativeIdeleClassBaseChangeMulEquiv
        (K := K) (L := L)).toMonoidHom.comp
      (RelativeIdeleGroup.classInclusion K L) =
        ideleClassExtension K L

Module documentation

Relative and ordinary idele classes

Declarations

relativeIdelePrincipalSubgroup_map_baseChange

relativeIdeleClassBaseChangeMulEquiv

relativeIdeleClassBaseChangeMulEquiv_mk

relativeIdeleClassBaseChangeMulEquiv_classInclusion

relativeIdeleClassBaseChange_comp_classInclusion