Module

NormProperties.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.NormProperties

2 declarations indexed from sourceView source ↗

Module documentation

Functorial properties of the idele norm

In the tensor-product presentation 𝔸_L = 𝔸_K ⊗_K L, the idele norm is the determinant norm of a finite free algebra. Thus transitivity is the general transitivity theorem for determinant norms. The remaining statements record the base-field power formula and compatibility with principal ideles and Galois conjugation.

Imports2

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.BaseChange
Mathlib.RingTheory.Norm.Transitivity

Imported by4

theorem

fieldNormUnits_eq_prod_conjugates

L37 ↗

RelativeIdeleGroup.fieldNormUnits_eq_prod_conjugates

Documentation

The field norm, regarded in L, is the product of all Galois conjugates. This is the unit-valued form used for principal ideles in the Galois product norm formula.

Source context 6 commands

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

open scoped BigOperators
open NumberField
noncomputable section
namespace RelativeIdeleGroup
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField K] [NumberField L] in

Lean source · statement

theorem fieldNormUnits_eq_prod_conjugates
    [IsGalois K L] (x : Lˣ) :
    Units.map (algebraMap K L)
        (Units.map (_root_.Algebra.norm K) x) =
      ∏ σ : L ≃ₐ[K] L,
        Units.map σ.toRingEquiv.toMonoidHom x

theorem

inclusion_norm_principalIdele_eq_prod_conjugates

L53 ↗

RelativeIdeleGroup.inclusion_norm_principalIdele_eq_prod_conjugates