Module

NormOne.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.NormTopology.NormOne

3 declarations indexed from sourceView source ↗

Module documentation

Norms on norm-one idele groups

The ordinary idele norm restricts to a homomorphism between the actual norm-one idele subgroups.

Imports2

Imported by1

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.NormTopology.All

theorem

norm_mem_normOneSubgroup

L33 ↗

IdeleGroup.norm_mem_normOneSubgroup

Documentation

The ordinary idèle norm carries norm-one idèles to norm-one idèles.

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] [FiniteDimensional K L]

Lean source · statement

theorem norm_mem_normOneSubgroup
    (a : IdeleGroup L)
    (ha : a ∈ normOneSubgroup (K := L)) :
    norm K L a ∈ normOneSubgroup (K := K)

def

normOneNorm

L43 ↗

IdeleGroup.normOneNorm

Documentation

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

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] [FiniteDimensional K L]

Lean source · statement

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

theorem

normOneNorm_apply

L54 ↗

IdeleGroup.normOneNorm_apply

Documentation

Coercing the restricted norm-one map recovers the ordinary 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 IdeleGroup
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
    (a : normOneSubgroup (K := L)) :
    (normOneNorm K L a : IdeleGroup K) =
      norm K L a.1

Module documentation

Norms on norm-one idele groups

Declarations

norm_mem_normOneSubgroup

normOneNorm

normOneNorm_apply