NYLL
Module

Coordinates.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Adele.Coordinates
9 declarations indexed from sourceView source β†—

Module documentation

Coordinate assembly for relative adeles

The chosen finite K-basis of L identifies 𝔸_K βŠ—[K] L with a finite family of base adeles. The support file constructs and controls the forward coefficients; this file supplies the inverse assembly map. It is the global reconstruction half needed when local tensor components have first been chosen place by place.

Imports1
Imported by2

Declarations

def

relativeAdeleCoefficientLinearEquiv

L37 β†—
Documentation

A relative adele is linearly equivalent to its finite family of base-adele coefficients in the chosen extension basis.

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 relativeAdeleCoefficientLinearEquiv :
    RelativeAdeleRing K L ≃ₗ[
      NumberField.AdeleRing (π“ž K) K]
      (RelativeAdeleBasisIndex (K := K) (L := L) β†’
        NumberField.AdeleRing (π“ž K) K)
theorem

relativeAdeleCoefficientLinearEquiv_apply

L46 β†—
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 relativeAdeleCoefficientLinearEquiv_apply
    (z : RelativeAdeleRing K L)
    (i : RelativeAdeleBasisIndex (K := K) (L := L)) :
    relativeAdeleCoefficientLinearEquiv
        (K := K) (L := L) z i =
      relativeAdeleCoefficient
        (K := K) (L := L) z i
def

relativeAdeleOfCoefficients

L56 β†—
Documentation

Assemble a finite family of base adeles into a relative adele.

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 relativeAdeleOfCoefficients
    (a :
      RelativeAdeleBasisIndex (K := K) (L := L) β†’
        NumberField.AdeleRing (π“ž K) K) :
    RelativeAdeleRing K L
theorem

relativeAdeleCoefficient_ofCoefficients

L66 β†—
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 relativeAdeleCoefficient_ofCoefficients
    (a :
      RelativeAdeleBasisIndex (K := K) (L := L) β†’
        NumberField.AdeleRing (π“ž K) K)
    (i : RelativeAdeleBasisIndex (K := K) (L := L)) :
    relativeAdeleCoefficient
        (K := K) (L := L)
        (relativeAdeleOfCoefficients
          (K := K) (L := L) a) i =
      a i
theorem

relativeAdeleOfCoefficients_coefficients

L86 β†—
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 relativeAdeleOfCoefficients_coefficients
    (z : RelativeAdeleRing K L) :
    relativeAdeleOfCoefficients
        (K := K) (L := L)
        (relativeAdeleCoefficient
          (K := K) (L := L) z) =
      z
theorem

relativeAdeleOfCoefficients_finiteComponent

L105 β†—
Documentation

Finite-place evaluation of an assembled relative adele is the corresponding tensor sum of its coefficient components.

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 relativeAdeleOfCoefficients_finiteComponent
    (a :
      RelativeAdeleBasisIndex (K := K) (L := L) β†’
        NumberField.AdeleRing (π“ž K) K)
    (w : HeightOneSpectrum (π“ž K)) :
    relativeAdeleFiniteComponent
        (K := K) (L := L) w
        (relativeAdeleOfCoefficients
          (K := K) (L := L) a) =
      βˆ‘ i : RelativeAdeleBasisIndex (K := K) (L := L),
        (a i).2 w βŠ—β‚œ[K]
          relativeExtensionBasis
            (K := K) (L := L) i
theorem

relativeAdeleOfCoefficients_infiniteComponent

L126 β†—
Documentation

Infinite-place evaluation of an assembled relative adele is the corresponding tensor sum of its coefficient components.

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 relativeAdeleOfCoefficients_infiniteComponent
    (a :
      RelativeAdeleBasisIndex (K := K) (L := L) β†’
        NumberField.AdeleRing (π“ž K) K)
    (w : InfinitePlace K) :
    relativeAdeleInfiniteComponent
        (K := K) (L := L) w
        (relativeAdeleOfCoefficients
          (K := K) (L := L) a) =
      βˆ‘ i : RelativeAdeleBasisIndex (K := K) (L := L),
        (a i).1 w βŠ—β‚œ[K]
          relativeExtensionBasis
            (K := K) (L := L) i
def

relativeIdeleOfCoefficientFamilies

L147 β†—
Documentation

Assemble mutually inverse coordinate families into an actual relative idele. The inverse equation is checked after global coordinate assembly, so no invertibility is hidden in the definition.

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 relativeIdeleOfCoefficientFamilies
    (a b :
      RelativeAdeleBasisIndex (K := K) (L := L) β†’
        NumberField.AdeleRing (π“ž K) K)
    (hab :
      relativeAdeleOfCoefficients
          (K := K) (L := L) a *
        relativeAdeleOfCoefficients
          (K := K) (L := L) b = 1) :
    RelativeIdeleGroup K L
theorem

relativeIdeleOfCoefficientFamilies_coe

L166 β†—
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 relativeIdeleOfCoefficientFamilies_coe
    (a b :
      RelativeAdeleBasisIndex (K := K) (L := L) β†’
        NumberField.AdeleRing (π“ž K) K)
    (hab :
      relativeAdeleOfCoefficients
          (K := K) (L := L) a *
        relativeAdeleOfCoefficients
          (K := K) (L := L) b = 1) :
    ((relativeIdeleOfCoefficientFamilies
        (K := K) (L := L) a b hab :
      RelativeIdeleGroup K L) :
        RelativeAdeleRing K L) =
      relativeAdeleOfCoefficients
        (K := K) (L := L) a

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