NYLL
Module

InfinitePlaceTensorBlock.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Adele.InfinitePlaceTensorBlock
15 declarations indexed from sourceView source ↗

Module documentation

Archimedean relative-idele factors as induced local blocks

The concrete archimedean completion w.Completion used by the adele library is canonically the completion of the underlying absolute value w.1. Base change along this equivalence connects the actual archimedean component of a relative idele to the local tensor block of the local tensor decomposition, equivariantly for the full Galois action.

Imports3
Imported by4

Declarations

def

infinitePlaceCompletionAlgEquiv

L44 ↗
Documentation

The wrapper completion at an infinite place as a K-algebra equivalence with the underlying absolute-value completion.

Source context 8 commands

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

open scoped NumberField TensorProduct NumberField.LiesOver
open NumberField
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source · full declaration
def infinitePlaceCompletionAlgEquiv
    (w : InfinitePlace K) :
    w.Completion ≃ₐ[K] w.1.Completion where
  __ := InfinitePlace.Completion.equiv w
  commutes' _ := rfl
theorem

infinitePlaceCompletionAlgEquiv_algebraMap

L54 ↗
Documentation

The canonical comparisons from concrete infinite-place completions to absolute-value completions commute with the completion maps in a tower of number fields.

Source context 9 commands

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

open scoped NumberField TensorProduct NumberField.LiesOver
open NumberField
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source · full declaration
theorem infinitePlaceCompletionAlgEquiv_algebraMap
    (v : InfinitePlace K) (w : InfinitePlace L)
    (hw : w.comap (algebraMap K L) = v) :
    letI : w.1.LiesOver v.1 :=
      ⟨congrArg (fun q : InfinitePlace K => q.1) hw⟩
    let u : AbsoluteValueExtension v.1 L :=
      ⟨w.1, fun x =>
        congrArg (fun q : InfinitePlace K => q.1 x) hw⟩
    letI : Algebra v.1.Completion u.1.Completion :=
      AbsoluteValue.completionAlgebra v.1 u.1 u.2
    RingHom.comp
        (algebraMap v.1.Completion u.1.Completion)
        (infinitePlaceCompletionAlgEquiv v).toRingEquiv =
      RingHom.comp
        (infinitePlaceCompletionAlgEquiv w).toRingEquiv
        (algebraMap v.Completion w.Completion) := by
  let : w.1.LiesOver v.1 :=
    ⟨congrArg (fun q : InfinitePlace K => q.1) hw⟩
  let u : AbsoluteValueExtension v.1 L :=
    ⟨w.1, fun x =>
      congrArg (fun q : InfinitePlace K => q.1 x) hw⟩
  let : Algebra v.1.Completion u.1.Completion :=
    AbsoluteValue.completionAlgebra v.1 u.1 u.2
  ext x
  refine InfinitePlace.Completion.induction_on v x ?_ ?_
  · exact
      isClosed_eq
        ((AbsoluteValue.completionMap_isometry
            v.1 w.1 u.2).continuous.comp
          (InfinitePlace.Completion.continuous_toCompletion v))
        ((InfinitePlace.Completion.continuous_toCompletion w).comp
          NumberField.LiesOver.continuous_completionMap)
  · intro y
    have hy :
        (y : v.1.Completion) =
          algebraMap K v.1.Completion
            (WithAbs.equiv v.1 y) := by
      rw [← AbsoluteValue.toCompletion_eq_algebraMap]
      simp
    change
      AbsoluteValue.completionMap v.1 u.1 u.2
          (y : v.1.Completion) =
        (NumberField.LiesOver.completionMap
          (v := v) (w := w)
          (y : v.Completion)).toCompletion
    rw [NumberField.LiesOver.completionMap_coe]
    rw [hy, AbsoluteValue.completionMap_coe]
    rfl
def

infinitePlaceLocalTensorAlgEquiv

L105 ↗
Documentation

Base change of the first tensor factor from the concrete archimedean completion to the absolute-value completion.

Source context 8 commands

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

open scoped NumberField TensorProduct NumberField.LiesOver
open NumberField
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source · statement
def infinitePlaceLocalTensorAlgEquiv
    (w : InfinitePlace K) :
    w.Completion ⊗[K] L ≃ₐ[K]
      LocalTensorAlgebra (L := L) w.1
theorem

infinitePlaceLocalTensorAlgEquiv_tmul

L117 ↗
Documentation

The concrete-to-absolute completion comparison acts componentwise on a pure tensor.

Source context 9 commands

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

open scoped NumberField TensorProduct NumberField.LiesOver
open NumberField
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField K] [NumberField L] [FiniteDimensional K L] in
Lean source · statement
theorem infinitePlaceLocalTensorAlgEquiv_tmul
    (w : InfinitePlace K) (a : w.Completion) (x : L) :
    infinitePlaceLocalTensorAlgEquiv
        (K := K) (L := L) w (a ⊗ₜ[K] x) =
      infinitePlaceCompletionAlgEquiv w a ⊗ₜ[K] x
def

infinitePlaceLocalTensorUnitsEquiv

L125 ↗
Documentation

The induced multiplicative equivalence on local tensor units.

Source context 8 commands

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

open scoped NumberField TensorProduct NumberField.LiesOver
open NumberField
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source · statement
def infinitePlaceLocalTensorUnitsEquiv
    (w : InfinitePlace K) :
    (w.Completion ⊗[K] L)ˣ ≃*
      (LocalTensorAlgebra (L := L) w.1)ˣ
theorem

infinitePlaceLocalTensorAlgEquiv_conjugation

L136 ↗
Documentation

Completion comparison commutes with conjugation on the second tensor factor.

Source context 9 commands

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

open scoped NumberField TensorProduct NumberField.LiesOver
open NumberField
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField K] [NumberField L] [FiniteDimensional K L] in
Lean source · statement
theorem infinitePlaceLocalTensorAlgEquiv_conjugation
    (w : InfinitePlace K)
    (σ : L ≃ₐ[K] L)
    (z : w.Completion ⊗[K] L) :
    infinitePlaceLocalTensorAlgEquiv
        (K := K) (L := L) w
        (scalarTensorConjugation
          (K := K) (L := L)
          (A := w.Completion) σ z) =
      localTensorConjugation
        (K := K) (L := L) w.1 σ
        (infinitePlaceLocalTensorAlgEquiv
          (K := K) (L := L) w z)
theorem

infinitePlaceLocalTensorUnitsEquiv_smul

L155 ↗
Documentation

The completion comparison on units is equivariant.

Source context 9 commands

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

open scoped NumberField TensorProduct NumberField.LiesOver
open NumberField
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField K] [NumberField L] [FiniteDimensional K L] in
Lean source · full declaration
theorem infinitePlaceLocalTensorUnitsEquiv_smul
    (w : InfinitePlace K)
    (σ : L ≃ₐ[K] L)
    (z : (w.Completion ⊗[K] L)ˣ) :
    letI := scalarTensorUnitsAction
      (K := K) (L := L) (A := w.Completion)
    letI := localTensorUnitsAction
      (K := K) (L := L) w.1
    infinitePlaceLocalTensorUnitsEquiv
        (K := K) (L := L) w (σ • z) =
      σ • infinitePlaceLocalTensorUnitsEquiv
        (K := K) (L := L) w z := by
  let := scalarTensorUnitsAction
    (K := K) (L := L) (A := w.Completion)
  let := localTensorUnitsAction
    (K := K) (L := L) w.1
  apply Units.ext
  exact infinitePlaceLocalTensorAlgEquiv_conjugation
    (K := K) (L := L) w σ
      (z : w.Completion ⊗[K] L)
def

infinitePlaceTensorUnitsEquivLocalPlaceBlock

L182 ↗
Documentation

The local tensor decomposition for the actual archimedean component type used by the relative idele restricted product.

Source context 10 commands

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

open scoped NumberField TensorProduct NumberField.LiesOver
open NumberField
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
section Galois
variable [IsGalois K L]
Lean source · full declaration
def
    infinitePlaceTensorUnitsEquivLocalPlaceBlock
    (w : InfinitePlace K)
    (hw : w.1.IsNontrivial)
    (u : AbsoluteValueExtension w.1 L) :
    letI :=
      decompositionGroupLocalUnitsAction w.1 hw u
    letI hK :=
      AbsoluteValue.extensionCompletionAlgebra
        (K := K) u.1
    letI : SMul K u.1.Completion := hK.toSMul
    letI :=
      AbsoluteValue.completionAlgebra
        w.1 u.1 u.2
    letI : ∀ u' : AbsoluteValueExtension w.1 L,
        Algebra w.1.Completion u'.1.Completion :=
      fun u' =>
        AbsoluteValue.completionAlgebra
          w.1 u'.1 u'.2
    (w.Completion ⊗[K] L)ˣ ≃*
      LocalPlaceBlock w.1 hw u := by
  letI :=
    decompositionGroupLocalUnitsAction w.1 hw u
  letI hK :=
    AbsoluteValue.extensionCompletionAlgebra
      (K := K) u.1
  letI : SMul K u.1.Completion := hK.toSMul
  letI :=
    AbsoluteValue.completionAlgebra
      w.1 u.1 u.2
  letI : ∀ u' : AbsoluteValueExtension w.1 L,
      Algebra w.1.Completion u'.1.Completion :=
    fun u' =>
      AbsoluteValue.completionAlgebra
        w.1 u'.1 u'.2
  exact
    (infinitePlaceLocalTensorUnitsEquiv
      (K := K) (L := L) w).trans
      (localTensorUnitsEquivLocalPlaceBlock
        w.1 hw u)
instance

infinitePlaceExtensionCompletionAlgebra

L230 ↗
Source context 12 commands

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

open scoped NumberField TensorProduct NumberField.LiesOver
open NumberField
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
section Galois
variable [IsGalois K L]
section Equivariance
variable
    (w : InfinitePlace K)
    (hw : w.1.IsNontrivial)
    (u : AbsoluteValueExtension w.1 L)
Lean source · statement
instance infinitePlaceExtensionCompletionAlgebra :
    Algebra K u.1.Completion
instance

infinitePlaceExtensionCompletionSMul

L234 ↗
Source context 13 commands

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

open scoped NumberField TensorProduct NumberField.LiesOver
open NumberField
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
section Galois
variable [IsGalois K L]
section Equivariance
variable
    (w : InfinitePlace K)
    (hw : w.1.IsNontrivial)
    (u : AbsoluteValueExtension w.1 L)
local instance infinitePlaceExtensionCompletionAlgebra :
    Algebra K u.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) u.1
Lean source · statement
instance infinitePlaceExtensionCompletionSMul :
    SMul K u.1.Completion
instance

infinitePlaceLocalizedCompletionAlgebra

L238 ↗
Source context 14 commands

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

open scoped NumberField TensorProduct NumberField.LiesOver
open NumberField
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
section Galois
variable [IsGalois K L]
section Equivariance
variable
    (w : InfinitePlace K)
    (hw : w.1.IsNontrivial)
    (u : AbsoluteValueExtension w.1 L)
local instance infinitePlaceExtensionCompletionAlgebra :
    Algebra K u.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) u.1
local instance infinitePlaceExtensionCompletionSMul :
    SMul K u.1.Completion :=
  infinitePlaceExtensionCompletionAlgebra w u |>.toSMul
Lean source · statement
instance infinitePlaceLocalizedCompletionAlgebra :
    Algebra w.1.Completion u.1.Completion
instance

infinitePlaceAllCompletionAlgebra

L242 ↗
Source context 15 commands

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

open scoped NumberField TensorProduct NumberField.LiesOver
open NumberField
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
section Galois
variable [IsGalois K L]
section Equivariance
variable
    (w : InfinitePlace K)
    (hw : w.1.IsNontrivial)
    (u : AbsoluteValueExtension w.1 L)
local instance infinitePlaceExtensionCompletionAlgebra :
    Algebra K u.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) u.1
local instance infinitePlaceExtensionCompletionSMul :
    SMul K u.1.Completion :=
  infinitePlaceExtensionCompletionAlgebra w u |>.toSMul
local instance infinitePlaceLocalizedCompletionAlgebra :
    Algebra w.1.Completion u.1.Completion :=
  AbsoluteValue.completionAlgebra w.1 u.1 u.2
Lean source · statement
instance infinitePlaceAllCompletionAlgebra
    (u' : AbsoluteValueExtension w.1 L) :
    Algebra w.1.Completion u'.1.Completion
instance

infinitePlaceScalarTensorUnitsAction

L247 ↗
Source context 16 commands

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

open scoped NumberField TensorProduct NumberField.LiesOver
open NumberField
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
section Galois
variable [IsGalois K L]
section Equivariance
variable
    (w : InfinitePlace K)
    (hw : w.1.IsNontrivial)
    (u : AbsoluteValueExtension w.1 L)
local instance infinitePlaceExtensionCompletionAlgebra :
    Algebra K u.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) u.1
local instance infinitePlaceExtensionCompletionSMul :
    SMul K u.1.Completion :=
  infinitePlaceExtensionCompletionAlgebra w u |>.toSMul
local instance infinitePlaceLocalizedCompletionAlgebra :
    Algebra w.1.Completion u.1.Completion :=
  AbsoluteValue.completionAlgebra w.1 u.1 u.2
local instance infinitePlaceAllCompletionAlgebra
    (u' : AbsoluteValueExtension w.1 L) :
    Algebra w.1.Completion u'.1.Completion :=
  AbsoluteValue.completionAlgebra w.1 u'.1 u'.2
Lean source · statement
instance infinitePlaceScalarTensorUnitsAction :
    MulDistribMulAction (L ≃ₐ[K] L) (w.Completion ⊗[K] L)ˣ
instance

infinitePlaceLocalTensorUnitsAction

L251 ↗
Source context 17 commands

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

open scoped NumberField TensorProduct NumberField.LiesOver
open NumberField
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
section Galois
variable [IsGalois K L]
section Equivariance
variable
    (w : InfinitePlace K)
    (hw : w.1.IsNontrivial)
    (u : AbsoluteValueExtension w.1 L)
local instance infinitePlaceExtensionCompletionAlgebra :
    Algebra K u.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) u.1
local instance infinitePlaceExtensionCompletionSMul :
    SMul K u.1.Completion :=
  infinitePlaceExtensionCompletionAlgebra w u |>.toSMul
local instance infinitePlaceLocalizedCompletionAlgebra :
    Algebra w.1.Completion u.1.Completion :=
  AbsoluteValue.completionAlgebra w.1 u.1 u.2
local instance infinitePlaceAllCompletionAlgebra
    (u' : AbsoluteValueExtension w.1 L) :
    Algebra w.1.Completion u'.1.Completion :=
  AbsoluteValue.completionAlgebra w.1 u'.1 u'.2
local instance infinitePlaceScalarTensorUnitsAction :
    MulDistribMulAction (L ≃ₐ[K] L) (w.Completion ⊗[K] L)ˣ :=
  scalarTensorUnitsAction (K := K) (L := L) (A := w.Completion)
Lean source · statement
instance infinitePlaceLocalTensorUnitsAction :
    MulDistribMulAction
      (L ≃ₐ[K] L)
      (LocalTensorAlgebra (L := L) w.1)ˣ
theorem

infinitePlaceTensorUnitsEquivLocalPlaceBlock_smul

L260 ↗
Documentation

The actual archimedean local tensor equivalence is equivariant for the full Galois action.

Source context 19 commands

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

open scoped NumberField TensorProduct NumberField.LiesOver
open NumberField
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
section Galois
variable [IsGalois K L]
section Equivariance
variable
    (w : InfinitePlace K)
    (hw : w.1.IsNontrivial)
    (u : AbsoluteValueExtension w.1 L)
local instance infinitePlaceExtensionCompletionAlgebra :
    Algebra K u.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) u.1
local instance infinitePlaceExtensionCompletionSMul :
    SMul K u.1.Completion :=
  infinitePlaceExtensionCompletionAlgebra w u |>.toSMul
local instance infinitePlaceLocalizedCompletionAlgebra :
    Algebra w.1.Completion u.1.Completion :=
  AbsoluteValue.completionAlgebra w.1 u.1 u.2
local instance infinitePlaceAllCompletionAlgebra
    (u' : AbsoluteValueExtension w.1 L) :
    Algebra w.1.Completion u'.1.Completion :=
  AbsoluteValue.completionAlgebra w.1 u'.1 u'.2
local instance infinitePlaceScalarTensorUnitsAction :
    MulDistribMulAction (L ≃ₐ[K] L) (w.Completion ⊗[K] L)ˣ :=
  scalarTensorUnitsAction (K := K) (L := L) (A := w.Completion)
local instance infinitePlaceLocalTensorUnitsAction :
    MulDistribMulAction
      (L ≃ₐ[K] L)
      (LocalTensorAlgebra (L := L) w.1)ˣ :=
  localTensorUnitsAction (K := K) (L := L) w.1
omit [NumberField K] [NumberField L] in
Lean source · full declaration
theorem
    infinitePlaceTensorUnitsEquivLocalPlaceBlock_smul
    (σ : L ≃ₐ[K] L)
    (z : (w.Completion ⊗[K] L)ˣ) :
    letI :=
      decompositionGroupLocalUnitsAction w.1 hw u
    infinitePlaceTensorUnitsEquivLocalPlaceBlock
        (K := K) (L := L) w hw u (σ • z) =
      σ •
        infinitePlaceTensorUnitsEquivLocalPlaceBlock
          (K := K) (L := L) w hw u z := by
  let :=
    decompositionGroupLocalUnitsAction w.1 hw u
  have hsource :
      infinitePlaceLocalTensorUnitsEquiv
          (K := K) (L := L) w (σ • z) =
        σ • infinitePlaceLocalTensorUnitsEquiv
          (K := K) (L := L) w z :=
    infinitePlaceLocalTensorUnitsEquiv_smul
      (K := K) (L := L) w σ z
  calc
    infinitePlaceTensorUnitsEquivLocalPlaceBlock
        (K := K) (L := L) w hw u (σ • z) =
      localTensorUnitsEquivLocalPlaceBlock w.1 hw u
        (σ • infinitePlaceLocalTensorUnitsEquiv
          (K := K) (L := L) w z) :=
      congrArg
        (localTensorUnitsEquivLocalPlaceBlock w.1 hw u)
        hsource
    _ =
      σ • infinitePlaceTensorUnitsEquivLocalPlaceBlock
        (K := K) (L := L) w hw u z :=
      localTensorUnitsEquivLocalPlaceBlock_smul
        w.1 hw u σ
        (infinitePlaceLocalTensorUnitsEquiv
          (K := K) (L := L) w z)

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