NYLL
Module

CyclotomicNormOneCorrection.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.CyclotomicNormOneCorrection
1 declaration indexed from sourceView source ↗

Module documentation

Norm-one correction for the normalized cyclotomic idele value

The positive archimedean section over ℚ gives the source term in the cyclotomic norm-one reduction. After taking a positive [K : ℚ]-th root of the absolute norm of an idele, scalar extension of that section cancels the absolute norm. Its rational cyclotomic Artin value is trivial, so the normalized value is unchanged.

Imports3
Imported by2

Declarations

theorem

exists_normOneIdele_same_normalizedCyclotomicZHatIdeleValue

L35 ↗
GlobalClassFieldTheory.Reciprocity.exists_normOneIdele_same_normalizedCyclotomicZHatIdeleValue
Documentation

Every idele has the same normalized cyclotomic value as an actual norm-one idele.

Source context 6 commands

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

open scoped NNReal NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem
    exists_normOneIdele_same_normalizedCyclotomicZHatIdeleValue
    (a : IdeleGroup K) :
    ∃ b : IdeleGroup.normOneSubgroup (K := K),
      normalizedCyclotomicZHatIdeleValue K
          (Additive.ofMul (b : IdeleGroup K)) =
        normalizedCyclotomicZHatIdeleValue K
          (Additive.ofMul a)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.