Module

IdeleNorm.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.IdeleNorm

5 declarations indexed from sourceView source ↗

Module documentation

The norm on ordinary ideles

The relative idele group carries the determinant norm. The scalar-extension equivalence with the ordinary ideles of the extension field transports that existing norm to the usual map N_{L/K} : I_L → I_K.

Imports2

Imported by6

def

norm

L37 ↗

IdeleGroup.norm

Documentation

The ordinary idele norm N_{L/K} : I_L → I_K, transported from the determinant norm on the relative idele group.

Source context 6 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace IdeleGroup
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 norm :
    IdeleGroup L →* IdeleGroup K

theorem

norm_relativeIdeleBaseChangeMulEquiv

L44 ↗

IdeleGroup.norm_relativeIdeleBaseChangeMulEquiv

Source context 6 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace IdeleGroup
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 norm_relativeIdeleBaseChangeMulEquiv
    (z : RelativeIdeleGroup K L) :
    norm K L
        (relativeIdeleBaseChangeMulEquiv
          (K := K) (L := L) z) =
      RelativeIdeleGroup.norm K L z

theorem

norm_principalIdele

L55 ↗

IdeleGroup.norm_principalIdele

Documentation

On principal ideles, the ordinary idele norm is induced by the field norm.

Source context 6 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace IdeleGroup
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 norm_principalIdele
    (x : Lˣ) :
    norm K L (principalIdele L x) =
      principalIdele K (Units.map (Algebra.norm K) x)

def

ideleClassNorm

L74 ↗

Documentation

The ordinary idele-class norm N_{L/K} : C_L → C_K.

Source context 5 commands

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

open scoped NumberField
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 ideleClassNorm :
    IdeleClassGroup L →* IdeleClassGroup K

theorem

ideleClassNorm_mk

L87 ↗

Source context 5 commands

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

open scoped NumberField
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 ideleClassNorm_mk
    (a : IdeleGroup L) :
    ideleClassNorm K L
        (QuotientGroup.mk'
          (IdeleGroup.principalSubgroup L) a) =
      QuotientGroup.mk'
        (IdeleGroup.principalSubgroup K)
        (IdeleGroup.norm K L a)

Module documentation

The norm on ordinary ideles

Declarations

norm

norm_relativeIdeleBaseChangeMulEquiv

norm_principalIdele

ideleClassNorm

ideleClassNorm_mk