Module

UnramifiedInfinitePlaceAllNorm.lean

Nyll.ClassFieldTheory.Theorems.NormTheorems.UnramifiedInfinitePlaceAllNorm

1 declaration indexed from sourceView source ↗

Module documentation

Norms at an unramified infinite place

For a finite abelian extension, the determinant norm from the whole archimedean tensor algebra is surjective when the base place is unramified in the extension.

Imports2

Imported by1

Nyll.ClassFieldTheory.Theorems.NormTheorems.All

theorem

isNormAtInfinitePlace_of_unramified

L27 ↗

ClassFieldTheory.isNormAtInfinitePlace_of_unramified

Documentation

Every nonzero base-field element is an archimedean tensor norm at an unramified infinite place of a finite abelian extension.

Source context 4 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace ClassFieldTheory

Lean source · statement

theorem isNormAtInfinitePlace_of_unramified
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    (v : InfinitePlace K) (hv : v.IsUnramifiedIn L) (x : Kˣ) :
    IsNormAtInfinitePlace K L v x

Module documentation

Norms at an unramified infinite place

Declarations

isNormAtInfinitePlace_of_unramified