Module

NegativeOneNotInfiniteNorm.lean

Nyll.ClassFieldTheory.Theorems.NormTheorems.NegativeOneNotInfiniteNorm

1 declaration indexed from sourceView source ↗

Module documentation

The real-to-complex norm obstruction

At a real place which becomes complex, the determinant norm from the whole archimedean tensor algebra cannot be negative. The tensor algebra, rather than a single chosen completion, is the object in the public statement.

Imports3

Imported by1

Nyll.ClassFieldTheory.Theorems.NormTheorems.All

theorem

not_isNormAtInfinitePlace_neg_one_of_real_complex

L28 ↗

ClassFieldTheory.not_isNormAtInfinitePlace_neg_one_of_real_complex

Documentation

Negative one is not a norm from the complete archimedean tensor algebra if a real place becomes complex in a finite Galois 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 not_isNormAtInfinitePlace_neg_one_of_real_complex
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (v : InfinitePlace K) (w : InfinitePlace L)
    (hw : w.comap (algebraMap K L) = v)
    (hv : v.IsReal) (hc : w.IsComplex) :
    ¬ IsNormAtInfinitePlace K L v (-1 : Kˣ)

Module documentation

The real-to-complex norm obstruction

Declarations

not_isNormAtInfinitePlace_neg_one_of_real_complex