NYLL
Module

FinitePlaceTensorNorm.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Relative.FinitePlaceTensorNorm
11 declarations indexed from sourceView source ↗

Module documentation

Tensor norm images at actual finite places

This file specializes the local tensor norm calculation to a height-one prime of a number field. The canonical comparison

(K, |·|_v)^∧ ≃ K_v

identifies the determinant norm on (K, |·|_v)^∧ ⊗[K] L with the determinant norm on the concrete tensor factor K_v ⊗[K] L used by relative ideles. Consequently its image is the chosen open local norm subgroup from LocalNormApproximation.

The finite component of every global relative-idele norm therefore lies in that subgroup, and its corresponding local quotient class is one.

Imports3
Imported by13

Declarations

def

finitePlaceCompletionAlgEquiv

L48 ↗
Documentation

The canonical completion comparison as a K-algebra equivalence.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · full declaration
def finitePlaceCompletionAlgEquiv
    (v : HeightOneSpectrum (𝓞 K)) :
    (NumberField.HeightOneSpectrum.adicAbv K v).Completion ≃ₐ[K]
      v.adicCompletion K where
  __ := finitePlaceCompletionRingEquiv v
  commutes' x := by
    change
      finitePlaceCompletionRingHom v
          (((WithAbs.equiv
            (NumberField.HeightOneSpectrum.adicAbv K v)).symm x :
              WithAbs
                (NumberField.HeightOneSpectrum.adicAbv K v)) :
            (NumberField.HeightOneSpectrum.adicAbv K v).Completion) =
        algebraMap K (v.adicCompletion K) x
    rw [finitePlaceCompletionRingHom_coe]
    rfl
def

finitePlaceLocalTensorAlgEquiv

L67 ↗
Documentation

Base change of the first tensor factor gives the concrete tensor algebra at v.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def finitePlaceLocalTensorAlgEquiv
    (v : HeightOneSpectrum (𝓞 K)) :
    LocalTensorAlgebra (L := L)
        (NumberField.HeightOneSpectrum.adicAbv K v) ≃ₐ[K]
      v.adicCompletion K ⊗[K] L
def

finitePlaceLocalTensorUnitsEquiv

L77 ↗
Documentation

The induced equivalence on tensor-algebra unit groups.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def finitePlaceLocalTensorUnitsEquiv
    (v : HeightOneSpectrum (𝓞 K)) :
    (LocalTensorAlgebra (L := L)
      (NumberField.HeightOneSpectrum.adicAbv K v))ˣ ≃*
      (v.adicCompletion K ⊗[K] L)ˣ
theorem

finitePlaceLocalTensorNorm_commutes

L89 ↗
Documentation

The completed-base comparison intertwines the two determinant norm maps.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] [IsGalois K L] in
Lean source · statement
theorem finitePlaceLocalTensorNorm_commutes
    (v : HeightOneSpectrum (𝓞 K))
    (z :
      (LocalTensorAlgebra (L := L)
        (NumberField.HeightOneSpectrum.adicAbv K v))ˣ) :
    finitePlaceCompletionUnitsContinuousMulEquiv v
        (localTensorDetNorm
          (K := K) (L := L)
          (NumberField.HeightOneSpectrum.adicAbv K v) z) =
      _root_.localTensorNorm
        (K := K) (L := L) v
        (finitePlaceLocalTensorUnitsEquiv
          (K := K) (L := L) v z)
theorem

finitePlaceLocalTensorNorm_range_eq_transport

L113 ↗
Documentation

Before choosing a localization, the concrete determinant-norm image is the transport of the absolute-value tensor norm image.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] [IsGalois K L] in
Lean source · statement
theorem finitePlaceLocalTensorNorm_range_eq_transport
    (v : HeightOneSpectrum (𝓞 K)) :
    (_root_.localTensorNorm
        (K := K) (L := L) v).range =
      (localTensorNormSubgroup
        (K := K) (L := L)
        (NumberField.HeightOneSpectrum.adicAbv K v)).map
          (finitePlaceCompletionUnitsContinuousMulEquiv
            v).toMonoidHom
theorem

finitePlaceLocalTensorNorm_range_eq_chosenLocalNormSubgroup

L170 ↗
Documentation

Actual finite-place tensor norm image. The image of the determinant norm on K_v ⊗[K] L is exactly the chosen local field-norm subgroup in the concrete finite idele coordinate.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] in
Lean source · statement
theorem finitePlaceLocalTensorNorm_range_eq_chosenLocalNormSubgroup
    (v : HeightOneSpectrum (𝓞 K)) :
    (_root_.localTensorNorm
        (K := K) (L := L) v).range =
      chosenFinitePlaceLocalNormSubgroup
        (K := K) (L := L) v
def

finitePlaceTensorNormClass

L206 ↗
Documentation

The quotient projection whose kernel is the finite-place tensor norm image.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] in
Lean source · statement
def finitePlaceTensorNormClass
    (v : HeightOneSpectrum (𝓞 K)) :
    (v.adicCompletion K)ˣ →*
      ChosenFinitePlaceNormQuotient
        (K := K) (L := L) v
theorem

finitePlaceTensorNormClass_eq_one_iff

L218 ↗
Documentation

A concrete local class is trivial exactly when its representative is a determinant norm from K_v ⊗[K] L.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] in
Lean source · statement
theorem finitePlaceTensorNormClass_eq_one_iff
    (v : HeightOneSpectrum (𝓞 K))
    (x : (v.adicCompletion K)ˣ) :
    finitePlaceTensorNormClass
        (K := K) (L := L) v x = 1 ↔
      ∃ z : (v.adicCompletion K ⊗[K] L)ˣ,
        _root_.localTensorNorm
          (K := K) (L := L) v z = x
theorem

finitePlaceTensorNormClass_ker

L255 ↗
Documentation

The kernel of the concrete quotient projection is precisely the finite-place determinant norm image.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] in
Lean source · statement
theorem finitePlaceTensorNormClass_ker
    (v : HeightOneSpectrum (𝓞 K)) :
    (finitePlaceTensorNormClass
      (K := K) (L := L) v).ker =
      (_root_.localTensorNorm
        (K := K) (L := L) v).range
theorem

relativeIdeleNorm_finiteComponent_mem_chosenLocalNormSubgroup

L270 ↗
Documentation

Every finite component of a global relative-idele norm lies in the chosen local norm subgroup.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] in
Lean source · statement
theorem relativeIdeleNorm_finiteComponent_mem_chosenLocalNormSubgroup
    (v : HeightOneSpectrum (𝓞 K))
    (a : RelativeIdeleGroup K L) :
    IdeleGroup.finiteComponent v
        (RelativeIdeleGroup.norm K L a) ∈
      chosenFinitePlaceLocalNormSubgroup
        (K := K) (L := L) v
theorem

finitePlaceTensorNormClass_relativeIdeleNorm

L289 ↗
Documentation

Hence the local tensor-norm class of every finite component of a global relative-idele norm is trivial.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] in
Lean source · statement
theorem finitePlaceTensorNormClass_relativeIdeleNorm
    (v : HeightOneSpectrum (𝓞 K))
    (a : RelativeIdeleGroup K L) :
    finitePlaceTensorNormClass
        (K := K) (L := L) v
        (IdeleGroup.finiteComponent v
          (RelativeIdeleGroup.norm K L a)) = 1

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