Module

LocalNorm.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.LocalNorm

2 declarations indexed from sourceView source ↗

Module documentation

Local components of the idele norm

The local algebra at a place of the base field is a finite product of the completions above it. This file proves that the determinant norm on a finite product is the product of the norms of its factors. The last theorem applies this calculation to the canonical completion decomposition.

Imports3

Imported by5

theorem

localNorm_eq_prod

L41 ↗

RelativeIdeleGroup.localNorm_eq_prod

Documentation

At one place of the base field, under the canonical isomorphism

K_v ⊗[K] L ≃ ∏_{w ∣ v} L_w,

the determinant norm of an arbitrary local component is the product of the field norms of its components above v.

Source context 6 commands

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

open scoped BigOperators TensorProduct
noncomputable section
namespace RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open ValuationTheory.Completion
universe u v

Lean source · full declaration

theorem localNorm_eq_prod
    {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (z : vK.Completion ⊗[K] L) :
    letI :=
      completionTensorDecomposition_extensionFintype
        (K := K) (L := L) vK hvK
    letI : ∀ w : AbsoluteValueExtension vK L,
        Algebra vK.Completion w.1.Completion :=
      fun w ↦ AbsoluteValue.completionAlgebra vK w.1 w.2
    letI : ∀ w : AbsoluteValueExtension vK L,
        Module.Finite vK.Completion w.1.Completion :=
      fun w ↦ completionModuleFinite vK hvK w
    _root_.Algebra.norm vK.Completion z =
      ∏ w : AbsoluteValueExtension vK L,
        _root_.Algebra.norm vK.Completion
          (completionTensorDecomposition_left
            (K := K) (L := L) vK hvK z w) := by
  classical
  let :=
    completionTensorDecomposition_extensionFintype
      (K := K) (L := L) vK hvK
  let : ∀ w : AbsoluteValueExtension vK L,
      Algebra vK.Completion w.1.Completion :=
    fun w ↦ AbsoluteValue.completionAlgebra vK w.1 w.2
  let : ∀ w : AbsoluteValueExtension vK L,
      Module.Free vK.Completion w.1.Completion :=
    fun w ↦ Module.Free.of_divisionRing
      vK.Completion w.1.Completion
  let : ∀ w : AbsoluteValueExtension vK L,
      Module.Finite vK.Completion w.1.Completion :=
    fun w ↦ completionModuleFinite vK hvK w
  let e :=
    completionTensorDecomposition_left
      (K := K) (L := L) vK hvK
  calc
    _root_.Algebra.norm vK.Completion z =
        _root_.Algebra.norm vK.Completion (e z) :=
      (_root_.Algebra.norm_eq_of_algEquiv e z).symm
    _ = ∏ w : AbsoluteValueExtension vK L,
        _root_.Algebra.norm vK.Completion (e z w) :=
      algebra_norm_pi_apply
        (R := vK.Completion)
        (fun w : AbsoluteValueExtension vK L ↦
          w.1.Completion) (e z)

theorem

localNorm_units_eq_prod

L91 ↗

RelativeIdeleGroup.localNorm_units_eq_prod