NYLL
Module

LocalComponent.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.LocalComponent
26 declarations indexed from sourceView source β†—

Module documentation

Local components of relative adeles and ideles

For a finite place v of K, evaluation on the finite-adele coordinate is a K-algebra homomorphism 𝔸_K β†’ K_v. Scalar extension along L/K therefore gives the actual local component map

𝔸_K βŠ—[K] L β†’ K_v βŠ—[K] L.

This is the map needed to apply the local tensor decomposition and the local norm calculation to a genuine relative idele.

Imports1
Imported by6

Declarations

def

infiniteAdeleComponentAlgHom

L38 β†—
Documentation

Evaluation of an adele at an infinite place, as a K-algebra homomorphism.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
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 infiniteAdeleComponentAlgHom
    (v : InfinitePlace K) :
    NumberField.AdeleRing (π“ž K) K →ₐ[K]
      v.Completion
theorem

infiniteAdeleComponentAlgHom_apply

L49 β†—
Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
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
theorem infiniteAdeleComponentAlgHom_apply
    (v : InfinitePlace K)
    (a : NumberField.AdeleRing (π“ž K) K) :
    infiniteAdeleComponentAlgHom v a = a.1 v
theorem

infiniteAdeleComponentAlgHom_algebraMap

L56 β†—
Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
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
theorem infiniteAdeleComponentAlgHom_algebraMap
    (v : InfinitePlace K) (x : K) :
    infiniteAdeleComponentAlgHom v
        (algebraMap K
          (NumberField.AdeleRing (π“ž K) K) x) =
      algebraMap K v.Completion x
def

relativeAdeleInfiniteComponent

L66 β†—
Documentation

The relative-adele component at an infinite place: 𝔸_K βŠ—[K] L β†’ K_v βŠ—[K] L.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
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 relativeAdeleInfiniteComponent
    (v : InfinitePlace K) :
    RelativeAdeleRing K L →ₐ[K]
      v.Completion βŠ—[K] L
theorem

relativeAdeleInfiniteComponent_tmul

L76 β†—
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
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] [FiniteDimensional K L] in
Lean source Β· statement
theorem relativeAdeleInfiniteComponent_tmul
    (v : InfinitePlace K)
    (a : NumberField.AdeleRing (π“ž K) K) (x : L) :
    relativeAdeleInfiniteComponent
        (K := K) (L := L) v (a βŠ—β‚œ[K] x) =
      a.1 v βŠ—β‚œ[K] x
def

finiteAdeleComponentAlgHom

L86 β†—
Documentation

Evaluation of an adele at a finite place, as a K-algebra homomorphism.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
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 finiteAdeleComponentAlgHom
    (v : HeightOneSpectrum (π“ž K)) :
    NumberField.AdeleRing (π“ž K) K →ₐ[K]
      v.adicCompletion K
theorem

finiteAdeleComponentAlgHom_apply

L102 β†—
Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
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
theorem finiteAdeleComponentAlgHom_apply
    (v : HeightOneSpectrum (π“ž K))
    (a : NumberField.AdeleRing (π“ž K) K) :
    finiteAdeleComponentAlgHom v a = a.2 v
theorem

finiteAdeleComponentAlgHom_algebraMap

L109 β†—
Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
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
theorem finiteAdeleComponentAlgHom_algebraMap
    (v : HeightOneSpectrum (π“ž K)) (x : K) :
    finiteAdeleComponentAlgHom v
        (algebraMap K
          (NumberField.AdeleRing (π“ž K) K) x) =
      algebraMap K (v.adicCompletion K) x
def

relativeAdeleFiniteComponent

L120 β†—
Documentation

The relative-adele component at a finite place: 𝔸_K βŠ—[K] L β†’ K_v βŠ—[K] L.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
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] [FiniteDimensional K L] in
Lean source Β· statement
def relativeAdeleFiniteComponent
    (v : HeightOneSpectrum (π“ž K)) :
    RelativeAdeleRing K L →ₐ[K]
      v.adicCompletion K βŠ—[K] L
theorem

relativeAdeleFiniteComponent_tmul

L130 β†—
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
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] [FiniteDimensional K L] in
Lean source Β· statement
theorem relativeAdeleFiniteComponent_tmul
    (v : HeightOneSpectrum (π“ž K))
    (a : NumberField.AdeleRing (π“ž K) K) (x : L) :
    relativeAdeleFiniteComponent (K := K) (L := L) v
        (a βŠ—β‚œ[K] x) =
      a.2 v βŠ—β‚œ[K] x
theorem

map_norm_tensorProduct_baseChange

L142 β†—
Documentation

Determinant norm commutes with scalar extension along a homomorphism of coefficient algebras. This is the base-change identity needed to compare the global relative-idele norm with each local tensor norm.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
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] in
Lean source Β· statement
theorem map_norm_tensorProduct_baseChange
    {A : Type*} {B : Type*}
    [CommRing A] [CommRing B]
    [Algebra K A] [Algebra K B]
    [Nontrivial A] [Nontrivial B]
    (f : A →ₐ[K] B) (z : A βŠ—[K] L) :
    f (Algebra.norm A z) =
      Algebra.norm B
        (Algebra.TensorProduct.map f (AlgHom.id K L) z)
def

infiniteComponent

L200 β†—
RelativeIdeleGroup.infiniteComponent
Documentation

The unit-valued infinite component of a relative idele.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
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 RelativeIdeleGroup.infiniteComponent
    (v : InfinitePlace K) :
    RelativeIdeleGroup K L β†’*
      (v.Completion βŠ—[K] L)Λ£
theorem

infiniteComponent_coe

L210 β†—
RelativeIdeleGroup.infiniteComponent_coe
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
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] [FiniteDimensional K L] in
Lean source Β· statement
theorem RelativeIdeleGroup.infiniteComponent_coe
    (v : InfinitePlace K)
    (a : RelativeIdeleGroup K L) :
    ((RelativeIdeleGroup.infiniteComponent
        (K := K) (L := L) v a :
        (v.Completion βŠ—[K] L)Λ£) :
        v.Completion βŠ—[K] L) =
      relativeAdeleInfiniteComponent
        (K := K) (L := L) v
        (a : RelativeAdeleRing K L)
def

finiteComponent

L223 β†—
RelativeIdeleGroup.finiteComponent
Documentation

The unit-valued local component of a relative idele.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
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 RelativeIdeleGroup.finiteComponent
    (v : HeightOneSpectrum (π“ž K)) :
    RelativeIdeleGroup K L β†’*
      (v.adicCompletion K βŠ—[K] L)Λ£
theorem

finiteComponent_coe

L233 β†—
RelativeIdeleGroup.finiteComponent_coe
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
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] [FiniteDimensional K L] in
Lean source Β· statement
theorem RelativeIdeleGroup.finiteComponent_coe
    (v : HeightOneSpectrum (π“ž K))
    (a : RelativeIdeleGroup K L) :
    ((RelativeIdeleGroup.finiteComponent
        (K := K) (L := L) v a :
        (v.adicCompletion K βŠ—[K] L)Λ£) :
        v.adicCompletion K βŠ—[K] L) =
      relativeAdeleFiniteComponent
        (K := K) (L := L) v
        (a : RelativeAdeleRing K L)
def

localTensorNorm

L246 β†—
Documentation

The determinant norm on the local tensor algebra.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
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 localTensorNorm
    (v : HeightOneSpectrum (π“ž K)) :
    (v.adicCompletion K βŠ—[K] L)Λ£ β†’*
      (v.adicCompletion K)Λ£
theorem

finiteComponent_norm

L256 β†—
RelativeIdeleGroup.finiteComponent_norm
Documentation

The finite component of the global relative-idele norm is the determinant norm of the corresponding local tensor component.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
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 Β· statement
theorem RelativeIdeleGroup.finiteComponent_norm
    (v : HeightOneSpectrum (π“ž K))
    (a : RelativeIdeleGroup K L) :
    IdeleGroup.finiteComponent v
        (RelativeIdeleGroup.norm K L a) =
      localTensorNorm (K := K) (L := L) v
        (RelativeIdeleGroup.finiteComponent
          (K := K) (L := L) v a)
theorem

infiniteComponent_norm

L283 β†—
RelativeIdeleGroup.infiniteComponent_norm
Documentation

The infinite component of the global relative-idele norm is the determinant norm of the corresponding archimedean tensor component.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
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 Β· statement
theorem RelativeIdeleGroup.infiniteComponent_norm
    (v : InfinitePlace K)
    (a : RelativeIdeleGroup K L) :
    IdeleGroup.infiniteComponent v
        (RelativeIdeleGroup.norm K L a) =
      Units.map (Algebra.norm v.Completion)
        (RelativeIdeleGroup.infiniteComponent
          (K := K) (L := L) v a)
def

infiniteLocalIdeleInclusion

L308 β†—
Documentation

Scalar extension of an archimedean base-field unit into its local tensor algebra.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
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 infiniteLocalIdeleInclusion
    (v : InfinitePlace K) :
    v.CompletionΛ£ β†’*
      (v.Completion βŠ—[K] L)Λ£
def

infiniteLocalFieldIdeleInclusion

L319 β†—
Documentation

Scalar extension of an extension-field unit into an archimedean local tensor algebra.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
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 infiniteLocalFieldIdeleInclusion
    (v : InfinitePlace K) :
    LΛ£ β†’* (v.Completion βŠ—[K] L)Λ£
theorem

infiniteComponent_inclusion

L331 β†—
RelativeIdeleGroup.infiniteComponent_inclusion
Documentation

The infinite component of a globally included idele is scalar extension of its ordinary infinite component.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
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] [FiniteDimensional K L] in
Lean source Β· statement
theorem RelativeIdeleGroup.infiniteComponent_inclusion
    (v : InfinitePlace K)
    (a : IdeleGroup K) :
    RelativeIdeleGroup.infiniteComponent
        (K := K) (L := L) v
        (RelativeIdeleGroup.inclusion K L a) =
      infiniteLocalIdeleInclusion
        (K := K) (L := L) v
        (IdeleGroup.infiniteComponent v a)
theorem

infiniteComponent_principalIdele

L347 β†—
RelativeIdeleGroup.infiniteComponent_principalIdele
Documentation

The infinite component of a principal relative idele is the diagonal extension-field unit in the local tensor algebra.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
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] [FiniteDimensional K L] in
Lean source Β· statement
theorem RelativeIdeleGroup.infiniteComponent_principalIdele
    (v : InfinitePlace K) (x : LΛ£) :
    RelativeIdeleGroup.infiniteComponent
        (K := K) (L := L) v
        (RelativeIdeleGroup.principalIdele K L x) =
      infiniteLocalFieldIdeleInclusion
        (K := K) (L := L) v x
def

localIdeleInclusion

L359 β†—
Documentation

Scalar extension of a local base-field unit into the local tensor algebra.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
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 localIdeleInclusion
    (v : HeightOneSpectrum (π“ž K)) :
    (v.adicCompletion K)Λ£ β†’*
      (v.adicCompletion K βŠ—[K] L)Λ£
theorem

finiteComponent_inclusion

L372 β†—
RelativeIdeleGroup.finiteComponent_inclusion
Documentation

The local component of the globally included idele is the scalar extension of its ordinary local component.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
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] [FiniteDimensional K L] in
Lean source Β· statement
theorem RelativeIdeleGroup.finiteComponent_inclusion
    (v : HeightOneSpectrum (π“ž K))
    (a : IdeleGroup K) :
    RelativeIdeleGroup.finiteComponent
        (K := K) (L := L) v
        (RelativeIdeleGroup.inclusion K L a) =
      localIdeleInclusion (K := K) (L := L) v
        (IdeleGroup.finiteComponent v a)
def

localFieldIdeleInclusion

L385 β†—
Documentation

Scalar extension of an extension-field unit into the local tensor algebra.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
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 localFieldIdeleInclusion
    (v : HeightOneSpectrum (π“ž K)) :
    LΛ£ β†’* (v.adicCompletion K βŠ—[K] L)Λ£
theorem

finiteComponent_principalIdele

L397 β†—
RelativeIdeleGroup.finiteComponent_principalIdele
Documentation

The local component of a principal relative idele is the diagonal extension-field unit in the local tensor algebra.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
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] [FiniteDimensional K L] in
Lean source Β· statement
theorem RelativeIdeleGroup.finiteComponent_principalIdele
    (v : HeightOneSpectrum (π“ž K)) (x : LΛ£) :
    RelativeIdeleGroup.finiteComponent
        (K := K) (L := L) v
        (RelativeIdeleGroup.principalIdele K L x) =
      localFieldIdeleInclusion (K := K) (L := L) v x

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