NYLL
Module

FinitePlaceTensorBlock.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Adele.FinitePlaceTensorBlock
12 declarations indexed from sourceView source ↗

Module documentation

Finite-place tensor factors as induced local blocks

This file is the finite-place counterpart of InfinitePlaceTensorBlock. It compares the concrete completion K_v used by the idele restricted product with the absolute-value completion used by the canonical local tensor decomposition, and records equivariance for conjugation on the second tensor factor.

Imports3
Imported by5

Declarations

theorem

finitePlaceLocalTensorAlgEquiv_conjugation

L42 ↗
Documentation

Base change from the absolute-value completion to the concrete adic completion commutes with conjugation on 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 HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem finitePlaceLocalTensorAlgEquiv_conjugation
    (v : HeightOneSpectrum (𝓞 K))
    (σ : L ≃ₐ[K] L)
    (z :
      LocalTensorAlgebra (L := L)
        (HeightOneSpectrum.adicAbv K v)) :
    finitePlaceLocalTensorAlgEquiv
        (K := K) (L := L) v
        (localTensorConjugation
          (K := K) (L := L)
          (HeightOneSpectrum.adicAbv K v) σ z) =
      scalarTensorConjugation
        (K := K) (L := L)
        (A := v.adicCompletion K) σ
        (finitePlaceLocalTensorAlgEquiv
          (K := K) (L := L) v z)
theorem

finitePlaceLocalTensorUnitsEquiv_smul

L64 ↗
Documentation

The finite-completion comparison on tensor units is equivariant.

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 HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] [FiniteDimensional K L] [IsGalois K L] in
Lean source · full declaration
theorem finitePlaceLocalTensorUnitsEquiv_smul
    (v : HeightOneSpectrum (𝓞 K))
    (σ : L ≃ₐ[K] L)
    (z :
      (LocalTensorAlgebra (L := L)
        (HeightOneSpectrum.adicAbv K v))ˣ) :
    letI :=
      localTensorUnitsAction
        (K := K) (L := L)
        (HeightOneSpectrum.adicAbv K v)
    letI :=
      scalarTensorUnitsAction
        (K := K) (L := L)
        (A := v.adicCompletion K)
    finitePlaceLocalTensorUnitsEquiv
        (K := K) (L := L) v (σ • z) =
      σ • finitePlaceLocalTensorUnitsEquiv
        (K := K) (L := L) v z := by
  let :=
    localTensorUnitsAction
      (K := K) (L := L)
      (HeightOneSpectrum.adicAbv K v)
  let :=
    scalarTensorUnitsAction
      (K := K) (L := L)
      (A := v.adicCompletion K)
  apply Units.ext
  exact finitePlaceLocalTensorAlgEquiv_conjugation
    (K := K) (L := L) v σ
      (z :
        LocalTensorAlgebra (L := L)
          (HeightOneSpectrum.adicAbv K v))
theorem

finitePlaceLocalTensorUnitsEquiv_symm_smul

L99 ↗
Documentation

Equivariance of the inverse finite-completion comparison.

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 HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] [FiniteDimensional K L] [IsGalois K L] in
Lean source · full declaration
theorem finitePlaceLocalTensorUnitsEquiv_symm_smul
    (v : HeightOneSpectrum (𝓞 K))
    (σ : L ≃ₐ[K] L)
    (z : (v.adicCompletion K ⊗[K] L)ˣ) :
    letI :=
      localTensorUnitsAction
        (K := K) (L := L)
        (HeightOneSpectrum.adicAbv K v)
    letI :=
      scalarTensorUnitsAction
        (K := K) (L := L)
        (A := v.adicCompletion K)
    (finitePlaceLocalTensorUnitsEquiv
        (K := K) (L := L) v).symm (σ • z) =
      σ •
        (finitePlaceLocalTensorUnitsEquiv
          (K := K) (L := L) v).symm z := by
  let :=
    localTensorUnitsAction
      (K := K) (L := L)
      (HeightOneSpectrum.adicAbv K v)
  let :=
    scalarTensorUnitsAction
      (K := K) (L := L)
      (A := v.adicCompletion K)
  apply
    (finitePlaceLocalTensorUnitsEquiv
      (K := K) (L := L) v).injective
  rw [MulEquiv.apply_symm_apply,
    finitePlaceLocalTensorUnitsEquiv_smul,
    MulEquiv.apply_symm_apply]
def

finitePlaceTensorUnitsEquivLocalPlaceBlock

L133 ↗
Documentation

The local tensor decomposition for the concrete finite component type used by relative ideles.

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 HilbertRamification
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 finitePlaceTensorUnitsEquivLocalPlaceBlock
    (v : HeightOneSpectrum (𝓞 K))
    (w : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K v) L) :
    letI :=
      decompositionGroupLocalUnitsAction
        (HeightOneSpectrum.adicAbv K v)
        (RayClass.adicAbv_isNontrivial v) w
    letI hK :=
      AbsoluteValue.extensionCompletionAlgebra
        (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI :=
      AbsoluteValue.completionAlgebra
        (HeightOneSpectrum.adicAbv K v) w.1 w.2
    letI : ∀ w' : AbsoluteValueExtension
        (HeightOneSpectrum.adicAbv K v) L,
      Algebra
        (HeightOneSpectrum.adicAbv K v).Completion
        w'.1.Completion :=
      fun w' =>
        AbsoluteValue.completionAlgebra
          (HeightOneSpectrum.adicAbv K v)
          w'.1 w'.2
    (v.adicCompletion K ⊗[K] L)ˣ ≃*
      LocalPlaceBlock
        (HeightOneSpectrum.adicAbv K v)
        (RayClass.adicAbv_isNontrivial v) w :=
  (finitePlaceLocalTensorUnitsEquiv
      (K := K) (L := L) v).symm.trans
    (localTensorUnitsEquivLocalPlaceBlock
      (HeightOneSpectrum.adicAbv K v)
      (RayClass.adicAbv_isNontrivial v) w)
instance

finitePlaceDecompositionGroupAction

L174 ↗
Source context 9 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 HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Equivariance
variable
    (v : HeightOneSpectrum (𝓞 K))
    (w : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K v) L)
Lean source · statement
instance finitePlaceDecompositionGroupAction :
    MulDistribMulAction
      (absoluteValueDecompositionGroup K w.1)
      (AlgebraicNumberTheory.Valuations.LocalizedCompletion
        (HeightOneSpectrum.adicAbv K v) w)ˣ
instance

finitePlaceExtensionCompletionAlgebra

L183 ↗
Source context 10 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 HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Equivariance
variable
    (v : HeightOneSpectrum (𝓞 K))
    (w : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K v) L)
local instance finitePlaceDecompositionGroupAction :
    MulDistribMulAction
      (absoluteValueDecompositionGroup K w.1)
      (AlgebraicNumberTheory.Valuations.LocalizedCompletion
        (HeightOneSpectrum.adicAbv K v) w)ˣ :=
  decompositionGroupLocalUnitsAction
    (HeightOneSpectrum.adicAbv K v)
    (RayClass.adicAbv_isNontrivial v) w
Lean source · statement
instance finitePlaceExtensionCompletionAlgebra :
    Algebra K w.1.Completion
instance

finitePlaceExtensionCompletionSMul

L187 ↗
Source context 11 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 HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Equivariance
variable
    (v : HeightOneSpectrum (𝓞 K))
    (w : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K v) L)
local instance finitePlaceDecompositionGroupAction :
    MulDistribMulAction
      (absoluteValueDecompositionGroup K w.1)
      (AlgebraicNumberTheory.Valuations.LocalizedCompletion
        (HeightOneSpectrum.adicAbv K v) w)ˣ :=
  decompositionGroupLocalUnitsAction
    (HeightOneSpectrum.adicAbv K v)
    (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceExtensionCompletionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
Lean source · statement
instance finitePlaceExtensionCompletionSMul :
    SMul K w.1.Completion
instance

finitePlaceLocalizedCompletionAlgebra

L191 ↗
Source context 12 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 HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Equivariance
variable
    (v : HeightOneSpectrum (𝓞 K))
    (w : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K v) L)
local instance finitePlaceDecompositionGroupAction :
    MulDistribMulAction
      (absoluteValueDecompositionGroup K w.1)
      (AlgebraicNumberTheory.Valuations.LocalizedCompletion
        (HeightOneSpectrum.adicAbv K v) w)ˣ :=
  decompositionGroupLocalUnitsAction
    (HeightOneSpectrum.adicAbv K v)
    (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceExtensionCompletionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance finitePlaceExtensionCompletionSMul :
    SMul K w.1.Completion :=
  (finitePlaceExtensionCompletionAlgebra v w).toSMul
Lean source · statement
instance finitePlaceLocalizedCompletionAlgebra :
    Algebra
      (HeightOneSpectrum.adicAbv K v).Completion
      w.1.Completion
instance

finitePlaceAllCompletionAlgebra

L198 ↗
Source context 13 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 HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Equivariance
variable
    (v : HeightOneSpectrum (𝓞 K))
    (w : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K v) L)
local instance finitePlaceDecompositionGroupAction :
    MulDistribMulAction
      (absoluteValueDecompositionGroup K w.1)
      (AlgebraicNumberTheory.Valuations.LocalizedCompletion
        (HeightOneSpectrum.adicAbv K v) w)ˣ :=
  decompositionGroupLocalUnitsAction
    (HeightOneSpectrum.adicAbv K v)
    (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceExtensionCompletionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance finitePlaceExtensionCompletionSMul :
    SMul K w.1.Completion :=
  (finitePlaceExtensionCompletionAlgebra v w).toSMul
local instance finitePlaceLocalizedCompletionAlgebra :
    Algebra
      (HeightOneSpectrum.adicAbv K v).Completion
      w.1.Completion :=
  AbsoluteValue.completionAlgebra
    (HeightOneSpectrum.adicAbv K v) w.1 w.2
Lean source · statement
instance finitePlaceAllCompletionAlgebra
    (w' : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K v) L) :
    Algebra
      (HeightOneSpectrum.adicAbv K v).Completion
      w'.1.Completion
instance

finitePlaceScalarTensorUnitsAction

L207 ↗
Source context 14 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 HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Equivariance
variable
    (v : HeightOneSpectrum (𝓞 K))
    (w : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K v) L)
local instance finitePlaceDecompositionGroupAction :
    MulDistribMulAction
      (absoluteValueDecompositionGroup K w.1)
      (AlgebraicNumberTheory.Valuations.LocalizedCompletion
        (HeightOneSpectrum.adicAbv K v) w)ˣ :=
  decompositionGroupLocalUnitsAction
    (HeightOneSpectrum.adicAbv K v)
    (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceExtensionCompletionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance finitePlaceExtensionCompletionSMul :
    SMul K w.1.Completion :=
  (finitePlaceExtensionCompletionAlgebra v w).toSMul
local instance finitePlaceLocalizedCompletionAlgebra :
    Algebra
      (HeightOneSpectrum.adicAbv K v).Completion
      w.1.Completion :=
  AbsoluteValue.completionAlgebra
    (HeightOneSpectrum.adicAbv K v) w.1 w.2
local instance finitePlaceAllCompletionAlgebra
    (w' : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K v) L) :
    Algebra
      (HeightOneSpectrum.adicAbv K v).Completion
      w'.1.Completion :=
  AbsoluteValue.completionAlgebra
    (HeightOneSpectrum.adicAbv K v) w'.1 w'.2
Lean source · statement
instance finitePlaceScalarTensorUnitsAction :
    MulDistribMulAction
      (L ≃ₐ[K] L)
      (v.adicCompletion K ⊗[K] L)ˣ
instance

finitePlaceLocalTensorUnitsAction

L214 ↗
Source context 15 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 HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Equivariance
variable
    (v : HeightOneSpectrum (𝓞 K))
    (w : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K v) L)
local instance finitePlaceDecompositionGroupAction :
    MulDistribMulAction
      (absoluteValueDecompositionGroup K w.1)
      (AlgebraicNumberTheory.Valuations.LocalizedCompletion
        (HeightOneSpectrum.adicAbv K v) w)ˣ :=
  decompositionGroupLocalUnitsAction
    (HeightOneSpectrum.adicAbv K v)
    (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceExtensionCompletionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance finitePlaceExtensionCompletionSMul :
    SMul K w.1.Completion :=
  (finitePlaceExtensionCompletionAlgebra v w).toSMul
local instance finitePlaceLocalizedCompletionAlgebra :
    Algebra
      (HeightOneSpectrum.adicAbv K v).Completion
      w.1.Completion :=
  AbsoluteValue.completionAlgebra
    (HeightOneSpectrum.adicAbv K v) w.1 w.2
local instance finitePlaceAllCompletionAlgebra
    (w' : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K v) L) :
    Algebra
      (HeightOneSpectrum.adicAbv K v).Completion
      w'.1.Completion :=
  AbsoluteValue.completionAlgebra
    (HeightOneSpectrum.adicAbv K v) w'.1 w'.2
local instance finitePlaceScalarTensorUnitsAction :
    MulDistribMulAction
      (L ≃ₐ[K] L)
      (v.adicCompletion K ⊗[K] L)ˣ :=
  scalarTensorUnitsAction
    (K := K) (L := L) (A := v.adicCompletion K)
Lean source · statement
instance finitePlaceLocalTensorUnitsAction :
    MulDistribMulAction
      (L ≃ₐ[K] L)
      (LocalTensorAlgebra (L := L)
        (HeightOneSpectrum.adicAbv K v))ˣ
theorem

finitePlaceTensorUnitsEquivLocalPlaceBlock_smul

L226 ↗
Documentation

The concrete finite-place local tensor decomposition is equivariant for the full global Galois action.

Source context 17 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 HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Equivariance
variable
    (v : HeightOneSpectrum (𝓞 K))
    (w : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K v) L)
local instance finitePlaceDecompositionGroupAction :
    MulDistribMulAction
      (absoluteValueDecompositionGroup K w.1)
      (AlgebraicNumberTheory.Valuations.LocalizedCompletion
        (HeightOneSpectrum.adicAbv K v) w)ˣ :=
  decompositionGroupLocalUnitsAction
    (HeightOneSpectrum.adicAbv K v)
    (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceExtensionCompletionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance finitePlaceExtensionCompletionSMul :
    SMul K w.1.Completion :=
  (finitePlaceExtensionCompletionAlgebra v w).toSMul
local instance finitePlaceLocalizedCompletionAlgebra :
    Algebra
      (HeightOneSpectrum.adicAbv K v).Completion
      w.1.Completion :=
  AbsoluteValue.completionAlgebra
    (HeightOneSpectrum.adicAbv K v) w.1 w.2
local instance finitePlaceAllCompletionAlgebra
    (w' : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K v) L) :
    Algebra
      (HeightOneSpectrum.adicAbv K v).Completion
      w'.1.Completion :=
  AbsoluteValue.completionAlgebra
    (HeightOneSpectrum.adicAbv K v) w'.1 w'.2
local instance finitePlaceScalarTensorUnitsAction :
    MulDistribMulAction
      (L ≃ₐ[K] L)
      (v.adicCompletion K ⊗[K] L)ˣ :=
  scalarTensorUnitsAction
    (K := K) (L := L) (A := v.adicCompletion K)
local instance finitePlaceLocalTensorUnitsAction :
    MulDistribMulAction
      (L ≃ₐ[K] L)
      (LocalTensorAlgebra (L := L)
        (HeightOneSpectrum.adicAbv K v))ˣ :=
  localTensorUnitsAction
    (K := K) (L := L)
    (HeightOneSpectrum.adicAbv K v)
omit [NumberField L] in
Lean source · statement
theorem finitePlaceTensorUnitsEquivLocalPlaceBlock_smul
    (σ : L ≃ₐ[K] L)
    (z : (v.adicCompletion K ⊗[K] L)ˣ) :
    finitePlaceTensorUnitsEquivLocalPlaceBlock
        (K := K) (L := L) v w (σ • z) =
      σ •
        finitePlaceTensorUnitsEquivLocalPlaceBlock
          (K := K) (L := L) v w z

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