Module

GlobalNormIsEverywhereLocalNorm.lean

Nyll.ClassFieldTheory.Theorems.NormTheorems.GlobalNormIsEverywhereLocalNorm

1 declaration indexed from sourceView source ↗

Module documentation

Global norms are local norms everywhere

This module states the elementary local consequence of being a global field norm. The assumptions give a finite extension L / K of number fields and a unit x of K. The conclusion says that if x lies in the global norm subgroup, then after scalar extension it is a determinant norm at every finite and every infinite completion of K.

Imports3

Imported by1

Nyll.ClassFieldTheory.Theorems.NormTheorems.All

theorem

globalNorm_isEverywhereLocalNorm

L28 ↗

ClassFieldTheory.globalNorm_isEverywhereLocalNorm

Documentation

Every global field norm is a norm over every completion.

Source context 3 commands

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

open scoped NumberField
namespace ClassFieldTheory
universe u v

Lean source · statement

theorem globalNorm_isEverywhereLocalNorm
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
    (x : Kˣ) :
    IsFieldNorm K L x → IsEverywhereLocalNorm K L x

Module documentation

Global norms are local norms everywhere

Declarations

globalNorm_isEverywhereLocalNorm