Module

IdeleClassNorm.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.NormTopology.IdeleClassNorm

4 declarations indexed from sourceView source ↗

Module documentation

The ordinary norm on idele classes

The ordinary idele-class norm preserves the absolute norm and restricts to the norm-one idele-class subgroups.

Imports3

Imported by2

theorem

absoluteNorm_ideleClassNorm

L36 ↗

IdeleClassGroup.absoluteNorm_ideleClassNorm

Documentation

The ordinary idèle-class norm preserves the absolute idèle norm.

Source context 6 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace IdeleClassGroup
universe u v
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [FiniteDimensional K L]

Lean source · statement

theorem absoluteNorm_ideleClassNorm
    (c : IdeleClassGroup L) :
    absoluteNorm (_root_.ideleClassNorm K L c) =
      absoluteNorm c

theorem

ideleClassNorm_mem_normOneSubgroup

L56 ↗

IdeleClassGroup.ideleClassNorm_mem_normOneSubgroup

Documentation

The ordinary idele-class norm carries norm-one idele classes to norm-one idele classes.

Source context 6 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace IdeleClassGroup
universe u v
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [FiniteDimensional K L]

Lean source · statement

theorem ideleClassNorm_mem_normOneSubgroup
    (c : IdeleClassGroup L)
    (hc : c ∈ normOneSubgroup (K := L)) :
    _root_.ideleClassNorm K L c ∈
      normOneSubgroup (K := K)

def

normOneNorm

L69 ↗

IdeleClassGroup.normOneNorm

Documentation

The ordinary idele-class norm restricted to the norm-one idele-class groups.

Source context 6 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace IdeleClassGroup
universe u v
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [FiniteDimensional K L]

Lean source · statement

def normOneNorm :
    normOneSubgroup (K := L) →*
      normOneSubgroup (K := K)

theorem

normOneNorm_apply

L81 ↗

IdeleClassGroup.normOneNorm_apply

Documentation

Coercing the restricted norm-one map recovers the ordinary idèle-class norm.

Source context 6 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace IdeleClassGroup
universe u v
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [FiniteDimensional K L]

Lean source · statement

theorem normOneNorm_apply
    (c : normOneSubgroup (K := L)) :
    (normOneNorm K L c : IdeleClassGroup K) =
      _root_.ideleClassNorm K L c.1

Module documentation

The ordinary norm on idele classes

Declarations

absoluteNorm_ideleClassNorm

ideleClassNorm_mem_normOneSubgroup

normOneNorm

normOneNorm_apply