Nyll.ClassFieldTheory.Theorems.NormTheorems.InfiniteNormIffPositive

Module documentation

The norm criterion at a real place that becomes complex

At such a place the determinant norms from the full archimedean tensor algebra are exactly the positive real elements. In particular this does not incorrectly replace the tensor norm by a separate condition at every factor of the tensor product.

theorem

isNormAtInfinitePlace_iff_positive_of_real_complex

L29 ↗

ClassFieldTheory.isNormAtInfinitePlace_iff_positive_of_real_complex

Documentation

At a real place that becomes complex in a finite Galois extension, being a norm from the archimedean tensor algebra is equivalent to positivity.

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_iff_positive_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)
    (x : Kˣ) :
    IsNormAtInfinitePlace K L v x ↔
      0 < InfinitePlace.Completion.extensionEmbeddingOfIsReal hv
        (algebraMap K v.Completion (x : K))

Module documentation

The norm criterion at a real place that becomes complex

Declarations

isNormAtInfinitePlace_iff_positive_of_real_complex