Module

AdeleBaseChange.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.AdeleBaseChange

37 declarations indexed from sourceView source ↗

Module documentation

Scalar extension from relative to ordinary adeles

This file upgrades the relative-to-ordinary idele comparison to the underlying adele rings. The additive structure is needed to transport determinant norms in a field tower.

Imports2

Imported by4

def

finitePlaceTensorRingEquivAboveAdic

L38 ↗

Documentation

The finite local tensor algebra, decomposed into the concrete adic completions above the chosen base place.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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 finitePlaceTensorRingEquivAboveAdic
    (w : HeightOneSpectrum (𝓞 K)) :
    (w.adicCompletion K ⊗[K] L) ≃+*
      ∀ W : {W : HeightOneSpectrum (𝓞 L) //
          finitePlaceBelow (K := K) W = w},
        W.1.adicCompletion L

theorem

finitePlaceTensorRingEquivAboveAdic_apply_extension

L86 ↗

Documentation

Evaluation of the finite-place tensor equivalence at an extension of the given adic absolute value.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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 finitePlaceTensorRingEquivAboveAdic_apply_extension
    (w : HeightOneSpectrum (𝓞 K))
    (x : w.adicCompletion K ⊗[K] L)
    (u : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K w) L) :
    finitePlaceTensorRingEquivAboveAdic
        (K := K) (L := L) w x
        (finitePlaceExtensionEquivAbove
          (K := K) (L := L) w u) =
      finitePlaceExtensionAdicCompletionRingEquiv
          (K := K) (L := L) w u
        (finitePlaceLocalTensorDecompositionComponent
          (K := K) (L := L) w u x)

theorem

finitePlaceTensorRingEquivAboveAdic_tmul

L114 ↗

Documentation

On a pure tensor, the finite-place relative-to-ordinary comparison is the canonical completion map on the local coefficient multiplied by the diagonal image of the extension-field factor.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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 finitePlaceTensorRingEquivAboveAdic_tmul
    (w : HeightOneSpectrum (𝓞 K))
    (W : {W : HeightOneSpectrum (𝓞 L) //
      finitePlaceBelow (K := K) W = w})
    (a : w.adicCompletion K)
    (x : L) :
    finitePlaceTensorRingEquivAboveAdic
        (K := K) (L := L) w
        (a ⊗ₜ[K] x) W =
      finitePlaceAdicCompletionMap K L w W a *
        algebraMap L (W.1.adicCompletion L) x

def

infiniteCompletionRingProductReindexAbove

L143 ↗

Documentation

Reindex the archimedean relative-tensor product by concrete places above w, before replacing the completion wrappers.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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 infiniteCompletionRingProductReindexAbove
    (w : InfinitePlace K) :
    (∀ u : AbsoluteValueExtension w.1 L,
      u.1.Completion) ≃+*
      ∀ W : {W : InfinitePlace L //
          infinitePlaceBelow (K := K) W = w},
        W.1.1.Completion

def

infinitePlaceTensorRingEquivAbove

L169 ↗

Documentation

The archimedean local tensor algebra, decomposed into the concrete infinite completions above the chosen base place.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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 infinitePlaceTensorRingEquivAbove
    (w : InfinitePlace K) :
    (w.Completion ⊗[K] L) ≃+*
      ∀ W : {W : InfinitePlace L //
          infinitePlaceBelow (K := K) W = w},
        W.1.Completion

theorem

infinitePlaceTensorRingEquivAbove_apply

L193 ↗

Documentation

Evaluation of the infinite-place tensor equivalence at a place above the chosen base place.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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 infinitePlaceTensorRingEquivAbove_apply
    (w : InfinitePlace K)
    (z : w.Completion ⊗[K] L)
    (W : {W : InfinitePlace L //
      infinitePlaceBelow (K := K) W = w}) :
    infinitePlaceTensorRingEquivAbove
        (K := K) (L := L) w z W =
      (InfinitePlace.Completion.equiv W.1).symm
        (completionTensorDecomposition_left
          w.1 w.isNontrivial
          (infinitePlaceLocalTensorAlgEquiv
            (K := K) (L := L) w z)
          (infinitePlaceAboveEquivExtension
            (K := K) (L := L) w W))

theorem

infinitePlaceTensorRingEquivAbove_tmul

L212 ↗

Documentation

On a pure tensor, the infinite-place relative-to-ordinary comparison is the canonical completion map on the local coefficient multiplied by the diagonal image of the extension-field factor.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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

theorem infinitePlaceTensorRingEquivAbove_tmul
    (w : InfinitePlace K)
    (W : {W : InfinitePlace L //
      infinitePlaceBelow (K := K) W = w})
    (a : w.Completion)
    (x : L) :
    letI : W.1.1.LiesOver w.1 :=
      ⟨congrArg (fun q : InfinitePlace K => q.1) W.2⟩
    infinitePlaceTensorRingEquivAbove
        (K := K) (L := L) w
        (a ⊗ₜ[K] x) W =
      NumberField.LiesOver.completionMap
          (v := w) (w := W.1) a *
        algebraMap L W.1.Completion x := by
  let : W.1.1.LiesOver w.1 :=
    ⟨congrArg (fun q : InfinitePlace K => q.1) W.2⟩
  rw [infinitePlaceTensorRingEquivAbove_apply]
  change
    (InfinitePlace.Completion.equiv W.1).symm
        (completionTensorDecomposition_left
          w.1 w.isNontrivial
          ((infinitePlaceCompletionAlgEquiv w a) ⊗ₜ[K] x)
          (infinitePlaceAboveToExtension
            (K := K) (L := L) w W)) =
      NumberField.LiesOver.completionMap
          (v := w) (w := W.1) a *
        algebraMap L W.1.Completion x
  dsimp only [infinitePlaceAboveToExtension]
  rw [completionTensorDecomposition_left_tmul_apply, map_mul]
  congr 1

def

finitePlaceAbovePiRingEquiv

L245 ↗

Documentation

Flatten the products over finite base places and places above them to the product over all finite places of the extension field.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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 finitePlaceAbovePiRingEquiv :
    (∀ w : HeightOneSpectrum (𝓞 K),
      ∀ W : {W : HeightOneSpectrum (𝓞 L) //
          finitePlaceBelow (K := K) W = w},
        W.1.adicCompletion L) ≃+*
      ∀ W : HeightOneSpectrum (𝓞 L),
        W.adicCompletion L where
  toFun f W :=
    f (finitePlaceBelow (K := K) W) ⟨W, rfl⟩
  invFun f w W := f W.1
  left_inv f := by
    funext w W
    rcases W with ⟨W, hW⟩
    subst w
    rfl
  right_inv f := by
    funext W
    rfl
  map_add' f g := by
    funext W
    rfl
  map_mul' f g := by
    funext W
    rfl

def

relativeFiniteTensorPiRingEquiv

L272 ↗

Documentation

All finite local tensor rings, flattened to the concrete finite completion family of the extension field.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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 relativeFiniteTensorPiRingEquiv :
    (∀ w : HeightOneSpectrum (𝓞 K),
      w.adicCompletion K ⊗[K] L) ≃+*
      ∀ W : HeightOneSpectrum (𝓞 L),
        W.adicCompletion L

theorem

relativeFiniteTensorPiRingEquiv_apply

L285 ↗

Documentation

Coordinate formula for the relative finite tensor product equivalence.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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 relativeFiniteTensorPiRingEquiv_apply
    (x : ∀ w : HeightOneSpectrum (𝓞 K),
      w.adicCompletion K ⊗[K] L)
    (W : HeightOneSpectrum (𝓞 L)) :
    relativeFiniteTensorPiRingEquiv
        (K := K) (L := L) x W =
      finitePlaceTensorRingEquivAboveAdic
        (K := K) (L := L)
        (finitePlaceBelow (K := K) W)
        (x (finitePlaceBelow (K := K) W)) ⟨W, rfl⟩

theorem

relativeFiniteTensorPiRingEquiv_symm_apply

L300 ↗

Documentation

Coordinate formula for the inverse relative finite tensor product equivalence.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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

theorem relativeFiniteTensorPiRingEquiv_symm_apply
    (y : ∀ W : HeightOneSpectrum (𝓞 L),
      W.adicCompletion L)
    (w : HeightOneSpectrum (𝓞 K)) :
    (relativeFiniteTensorPiRingEquiv
        (K := K) (L := L)).symm y w =
      (finitePlaceTensorRingEquivAboveAdic
        (K := K) (L := L) w).symm
        (fun W => y W.1) :=
  rfl

def

infinitePlaceAbovePiRingEquiv

L313 ↗

Documentation

Flatten the products over infinite base places and places above them to the product over all infinite places of the extension field.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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 infinitePlaceAbovePiRingEquiv :
    (∀ w : InfinitePlace K,
      ∀ W : {W : InfinitePlace L //
          infinitePlaceBelow (K := K) W = w},
        W.1.Completion) ≃+*
      ∀ W : InfinitePlace L, W.Completion where
  toFun f W :=
    f (infinitePlaceBelow (K := K) W) ⟨W, rfl⟩
  invFun f w W := f W.1
  left_inv f := by
    funext w W
    rcases W with ⟨W, hW⟩
    subst w
    rfl
  right_inv f := by
    funext W
    rfl
  map_add' f g := by
    funext W
    rfl
  map_mul' f g := by
    funext W
    rfl

def

relativeInfiniteTensorPiRingEquiv

L339 ↗

Documentation

All infinite local tensor rings, flattened to the concrete infinite completion family of the extension field.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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 relativeInfiniteTensorPiRingEquiv :
    (∀ w : InfinitePlace K,
      w.Completion ⊗[K] L) ≃+*
      ∀ W : InfinitePlace L, W.Completion

theorem

relativeInfiniteTensorPiRingEquiv_apply

L351 ↗

Documentation

Coordinate formula for the relative infinite tensor product equivalence.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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 relativeInfiniteTensorPiRingEquiv_apply
    (x : ∀ w : InfinitePlace K,
      w.Completion ⊗[K] L)
    (W : InfinitePlace L) :
    relativeInfiniteTensorPiRingEquiv
        (K := K) (L := L) x W =
      infinitePlaceTensorRingEquivAbove
        (K := K) (L := L)
        (infinitePlaceBelow (K := K) W)
        (x (infinitePlaceBelow (K := K) W)) ⟨W, rfl⟩

theorem

relativeInfiniteTensorPiRingEquiv_symm_apply

L366 ↗

Documentation

Coordinate formula for the inverse relative infinite tensor product equivalence.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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

theorem relativeInfiniteTensorPiRingEquiv_symm_apply
    (y : ∀ W : InfinitePlace L, W.Completion)
    (w : InfinitePlace K) :
    (relativeInfiniteTensorPiRingEquiv
        (K := K) (L := L)).symm y w =
      (infinitePlaceTensorRingEquivAbove
        (K := K) (L := L) w).symm
        (fun W => y W.1) :=
  rfl

theorem

relativeLocalTensorDecompositionIntegralAt_iff_aboveAdicRing

L378 ↗

Documentation

Integrality in the relative-tensor factors is exactly integrality of every concrete finite completion coordinate.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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 relativeLocalTensorDecompositionIntegralAt_iff_aboveAdicRing
    (w : HeightOneSpectrum (𝓞 K))
    (x : w.adicCompletion K ⊗[K] L) :
    RelativeLocalTensorDecompositionIntegralAt
        (K := K) (L := L) w x ↔
      ∀ W : {W : HeightOneSpectrum (𝓞 L) //
          finitePlaceBelow (K := K) W = w},
        finitePlaceTensorRingEquivAboveAdic
            (K := K) (L := L) w x W ∈
          W.1.adicCompletionIntegers L

theorem

relativeAdele_finiteComponent_basisIntegral_of_notMem

L415 ↗

Documentation

Outside its coefficient support, a relative adele finite component belongs to the fixed local basis lattice.

Source context 7 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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 relativeAdele_finiteComponent_basisIntegral_of_notMem
    (z : RelativeAdeleRing K L)
    (w : HeightOneSpectrum (𝓞 K))
    (hw : w ∉ relativeAdeleCoefficientSupport
      (K := K) (L := L) z) :
    RelativeBasisIntegralAt
      (K := K) (L := L) w
      (relativeAdeleFiniteComponent
        (K := K) (L := L) w z)

theorem

relativeAdele_eventually_aboveAdicIntegral

L442 ↗

Documentation

A relative adele becomes integral in every concrete completion above almost every finite base place.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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 relativeAdele_eventually_aboveAdicIntegral
    (z : RelativeAdeleRing K L) :
    ∀ᶠ w : HeightOneSpectrum (𝓞 K) in Filter.cofinite,
      ∀ W : {W : HeightOneSpectrum (𝓞 L) //
          finitePlaceBelow (K := K) W = w},
        finitePlaceTensorRingEquivAboveAdic
            (K := K) (L := L) w
            (relativeAdeleFiniteComponent
              (K := K) (L := L) w z) W ∈
          W.1.adicCompletionIntegers L

def

relativeAdeleToAdele

L468 ↗

Documentation

The forward ring-level scalar-extension map on adeles.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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 relativeAdeleToAdele
    (z : RelativeAdeleRing K L) :
    NumberField.AdeleRing (𝓞 L) L

theorem

relativeAdeleToAdele_infinite

L500 ↗

Documentation

The infinite component of the underlying adele of a relative adele.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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 relativeAdeleToAdele_infinite
    (z : RelativeAdeleRing K L)
    (W : InfinitePlace L) :
    (relativeAdeleToAdele
      (K := K) (L := L) z).1 W =
      infinitePlaceTensorRingEquivAbove
        (K := K) (L := L)
        (infinitePlaceBelow (K := K) W)
        (relativeAdeleInfiniteComponent
          (K := K) (L := L)
          (infinitePlaceBelow (K := K) W) z) ⟨W, rfl⟩

theorem

relativeAdeleToAdele_finite

L515 ↗

Documentation

The finite component of the underlying adele of a relative adele.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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 relativeAdeleToAdele_finite
    (z : RelativeAdeleRing K L)
    (W : HeightOneSpectrum (𝓞 L)) :
    (relativeAdeleToAdele
      (K := K) (L := L) z).2 W =
      finitePlaceTensorRingEquivAboveAdic
        (K := K) (L := L)
        (finitePlaceBelow (K := K) W)
        (relativeAdeleFiniteComponent
          (K := K) (L := L)
          (finitePlaceBelow (K := K) W) z) ⟨W, rfl⟩

def

finiteAdeleRelativeTensorFamily

L530 ↗

Documentation

Pull the finite coordinates of an ordinary adele back to the relative local tensor family.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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 finiteAdeleRelativeTensorFamily
    (y : IsDedekindDomain.FiniteAdeleRing (𝓞 L) L) :
    ∀ w : HeightOneSpectrum (𝓞 K),
      w.adicCompletion K ⊗[K] L

theorem

finiteAdeleRelativeTensorFamily_eventually_basisIntegral

L539 ↗

Documentation

The pulled-back finite tensor family is basis-integral at almost every finite place.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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 finiteAdeleRelativeTensorFamily_eventually_basisIntegral
    (y : IsDedekindDomain.FiniteAdeleRing (𝓞 L) L) :
    ∀ᶠ w : HeightOneSpectrum (𝓞 K) in Filter.cofinite,
      RelativeBasisIntegralAt
        (K := K) (L := L) w
        (finiteAdeleRelativeTensorFamily
          (K := K) (L := L) y w)

def

adeleToRelativeLocalAdeleData

L576 ↗

Documentation

Pull an ordinary adele back to restricted relative local data.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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 adeleToRelativeLocalAdeleData
    (y : NumberField.AdeleRing (𝓞 L) L) :
    RelativeLocalAdeleData (K := K) (L := L) where
  infinite :=
    (relativeInfiniteTensorPiRingEquiv
      (K := K) (L := L)).symm (fun W => y.1 W)
  finite :=
    finiteAdeleRelativeTensorFamily
      (K := K) (L := L) y.2
  eventually_integral i :=
    (finiteAdeleRelativeTensorFamily_eventually_basisIntegral
      (K := K) (L := L) y.2).mono fun w hw =>
        relativeBasisIntegralAt_repr_mem
          (K := K) (L := L) w _ hw i

def

adeleToRelativeAdele

L592 ↗

Documentation

The inverse ring-level scalar-extension map on adeles.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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 adeleToRelativeAdele
    (y : NumberField.AdeleRing (𝓞 L) L) :
    RelativeAdeleRing K L

theorem

adeleToRelativeAdele_infiniteComponent

L603 ↗

Documentation

The infinite component of the relative adele reconstructed from an ordinary adele.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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

theorem adeleToRelativeAdele_infiniteComponent
    (y : NumberField.AdeleRing (𝓞 L) L)
    (w : InfinitePlace K) :
    relativeAdeleInfiniteComponent
        (K := K) (L := L) w
        (adeleToRelativeAdele
          (K := K) (L := L) y) =
      (relativeInfiniteTensorPiRingEquiv
        (K := K) (L := L)).symm
        (fun W => y.1 W) w := by
  rw [adeleToRelativeAdele,
    relativeAdeleOfLocalData_infiniteComponent]
  rfl

theorem

adeleToRelativeAdele_finiteComponent

L620 ↗

Documentation

The finite component of the relative adele reconstructed from an ordinary adele.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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

theorem adeleToRelativeAdele_finiteComponent
    (y : NumberField.AdeleRing (𝓞 L) L)
    (w : HeightOneSpectrum (𝓞 K)) :
    relativeAdeleFiniteComponent
        (K := K) (L := L) w
        (adeleToRelativeAdele
          (K := K) (L := L) y) =
      (relativeFiniteTensorPiRingEquiv
        (K := K) (L := L)).symm
        (fun W => y.2 W) w := by
  rw [adeleToRelativeAdele,
    relativeAdeleOfLocalData_finiteComponent]
  rfl

def

relativeAdeleBaseChangeRingEquiv

L636 ↗

Documentation

Scalar extension identifies the relative adele ring over K with the ordinary adele ring of L.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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 relativeAdeleBaseChangeRingEquiv :
    RelativeAdeleRing K L ≃+*
      NumberField.AdeleRing (𝓞 L) L where
  toFun :=
    relativeAdeleToAdele (K := K) (L := L)
  invFun :=
    adeleToRelativeAdele (K := K) (L := L)
  left_inv z := by
    apply relativeAdele_ext_of_components
    · intro w
      rw [adeleToRelativeAdele_infiniteComponent]
      change
        (relativeInfiniteTensorPiRingEquiv
          (K := K) (L := L)).symm
            (relativeInfiniteTensorPiRingEquiv
              (K := K) (L := L)
              (fun w =>
                relativeAdeleInfiniteComponent
                  (K := K) (L := L) w z)) w =
          relativeAdeleInfiniteComponent
            (K := K) (L := L) w z
      rw [(relativeInfiniteTensorPiRingEquiv
        (K := K) (L := L)).symm_apply_apply]
    · intro w
      rw [adeleToRelativeAdele_finiteComponent]
      change
        (relativeFiniteTensorPiRingEquiv
          (K := K) (L := L)).symm
            (relativeFiniteTensorPiRingEquiv
              (K := K) (L := L)
              (fun w =>
                relativeAdeleFiniteComponent
                  (K := K) (L := L) w z)) w =
          relativeAdeleFiniteComponent
            (K := K) (L := L) w z
      rw [(relativeFiniteTensorPiRingEquiv
        (K := K) (L := L)).symm_apply_apply]
  right_inv y := by
    apply Prod.ext
    · funext W
      rw [relativeAdeleToAdele_infinite,
        adeleToRelativeAdele_infiniteComponent]
      change
        relativeInfiniteTensorPiRingEquiv
            (K := K) (L := L)
            ((relativeInfiniteTensorPiRingEquiv
              (K := K) (L := L)).symm
              (fun W => y.1 W)) W =
          y.1 W
      rw [(relativeInfiniteTensorPiRingEquiv
        (K := K) (L := L)).apply_symm_apply]
    · apply DFunLike.coe_injective
      funext W
      change
        relativeFiniteTensorPiRingEquiv
            (K := K) (L := L)
            (fun w =>
              relativeAdeleFiniteComponent
                (K := K) (L := L) w
                (adeleToRelativeAdele
                  (K := K) (L := L) y)) W =
          y.2 W
      rw [show
        (fun w =>
          relativeAdeleFiniteComponent
            (K := K) (L := L) w
            (adeleToRelativeAdele
              (K := K) (L := L) y)) =
          (relativeFiniteTensorPiRingEquiv
            (K := K) (L := L)).symm
            (fun W => y.2 W) by
          funext w
          exact adeleToRelativeAdele_finiteComponent
            (K := K) (L := L) y w]
      rw [(relativeFiniteTensorPiRingEquiv
        (K := K) (L := L)).apply_symm_apply]
  map_add' x y := by
    apply Prod.ext
    · funext W
      change
        relativeInfiniteTensorPiRingEquiv
            (K := K) (L := L)
            (fun w =>
              relativeAdeleInfiniteComponent
                (K := K) (L := L) w (x + y)) W =
          relativeInfiniteTensorPiRingEquiv
              (K := K) (L := L)
              (fun w =>
                relativeAdeleInfiniteComponent
                  (K := K) (L := L) w x) W +
            relativeInfiniteTensorPiRingEquiv
              (K := K) (L := L)
              (fun w =>
                relativeAdeleInfiniteComponent
                  (K := K) (L := L) w y) W
      rw [show
        (fun w =>
          relativeAdeleInfiniteComponent
            (K := K) (L := L) w (x + y)) =
          (fun w =>
            relativeAdeleInfiniteComponent
              (K := K) (L := L) w x) +
          (fun w =>
            relativeAdeleInfiniteComponent
              (K := K) (L := L) w y) by
          funext w
          exact map_add _ _ _,
        map_add]
      rfl
    · apply Subtype.ext
      funext W
      change
        relativeFiniteTensorPiRingEquiv
            (K := K) (L := L)
            (fun w =>
              relativeAdeleFiniteComponent
                (K := K) (L := L) w (x + y)) W =
          relativeFiniteTensorPiRingEquiv
              (K := K) (L := L)
              (fun w =>
                relativeAdeleFiniteComponent
                  (K := K) (L := L) w x) W +
            relativeFiniteTensorPiRingEquiv
              (K := K) (L := L)
              (fun w =>
                relativeAdeleFiniteComponent
                  (K := K) (L := L) w y) W
      rw [show
        (fun w =>
          relativeAdeleFiniteComponent
            (K := K) (L := L) w (x + y)) =
          (fun w =>
            relativeAdeleFiniteComponent
              (K := K) (L := L) w x) +
          (fun w =>
            relativeAdeleFiniteComponent
              (K := K) (L := L) w y) by
          funext w
          exact map_add _ _ _,
        map_add]
      rfl
  map_mul' x y := by
    apply Prod.ext
    · funext W
      change
        relativeInfiniteTensorPiRingEquiv
            (K := K) (L := L)
            (fun w =>
              relativeAdeleInfiniteComponent
                (K := K) (L := L) w (x * y)) W =
          relativeInfiniteTensorPiRingEquiv
              (K := K) (L := L)
              (fun w =>
                relativeAdeleInfiniteComponent
                  (K := K) (L := L) w x) W *
            relativeInfiniteTensorPiRingEquiv
              (K := K) (L := L)
              (fun w =>
                relativeAdeleInfiniteComponent
                  (K := K) (L := L) w y) W
      rw [show
        (fun w =>
          relativeAdeleInfiniteComponent
            (K := K) (L := L) w (x * y)) =
          (fun w =>
            relativeAdeleInfiniteComponent
              (K := K) (L := L) w x) *
          (fun w =>
            relativeAdeleInfiniteComponent
              (K := K) (L := L) w y) by
          funext w
          exact map_mul _ _ _,
        map_mul]
      rfl
    · apply Subtype.ext
      funext W
      change
        relativeFiniteTensorPiRingEquiv
            (K := K) (L := L)
            (fun w =>
              relativeAdeleFiniteComponent
                (K := K) (L := L) w (x * y)) W =
          relativeFiniteTensorPiRingEquiv
              (K := K) (L := L)
              (fun w =>
                relativeAdeleFiniteComponent
                  (K := K) (L := L) w x) W *
            relativeFiniteTensorPiRingEquiv
              (K := K) (L := L)
              (fun w =>
                relativeAdeleFiniteComponent
                  (K := K) (L := L) w y) W
      rw [show
        (fun w =>
          relativeAdeleFiniteComponent
            (K := K) (L := L) w (x * y)) =
          (fun w =>
            relativeAdeleFiniteComponent
              (K := K) (L := L) w x) *
          (fun w =>
            relativeAdeleFiniteComponent
              (K := K) (L := L) w y) by
          funext w
          exact map_mul _ _ _,
        map_mul]
      rfl

theorem

relativeAdeleBaseChangeRingEquiv_finiteComponent_tmul

L846 ↗

Documentation

Finite-coordinate formula for scalar extension of a pure relative adele tensor.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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 relativeAdeleBaseChangeRingEquiv_finiteComponent_tmul
    (a : NumberField.AdeleRing (𝓞 K) K)
    (x : L)
    (W : HeightOneSpectrum (𝓞 L)) :
    (relativeAdeleBaseChangeRingEquiv
        (K := K) (L := L) (a ⊗ₜ[K] x)).2 W =
      finitePlaceAdicCompletionMap K L
          (finitePlaceBelow (K := K) W) ⟨W, rfl⟩
          (a.2 (finitePlaceBelow (K := K) W)) *
        algebraMap L (W.adicCompletion L) x

theorem

relativeAdeleBaseChangeRingEquiv_infiniteComponent_tmul

L872 ↗

Documentation

Infinite-coordinate formula for scalar extension of a pure relative adele tensor.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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

theorem relativeAdeleBaseChangeRingEquiv_infiniteComponent_tmul
    (a : NumberField.AdeleRing (𝓞 K) K)
    (x : L)
    (W : InfinitePlace L) :
    let v := infinitePlaceBelow (K := K) W
    letI : W.1.LiesOver v.1 := ⟨rfl⟩
    (relativeAdeleBaseChangeRingEquiv
        (K := K) (L := L) (a ⊗ₜ[K] x)).1 W =
      NumberField.LiesOver.completionMap
          (v := v) (w := W) (a.1 v) *
        algebraMap L W.Completion x := by
  let v := infinitePlaceBelow (K := K) W
  let : W.1.LiesOver v.1 := ⟨rfl⟩
  change
    infinitePlaceTensorRingEquivAbove
        (K := K) (L := L) v
        (a.1 v ⊗ₜ[K] x) ⟨W, rfl⟩ =
      NumberField.LiesOver.completionMap
          (v := v) (w := W) (a.1 v) *
        algebraMap L W.Completion x
  exact
    infinitePlaceTensorRingEquivAbove_tmul
      (K := K) (L := L) v ⟨W, rfl⟩ (a.1 v) x

theorem

finitePlaceTensorRingEquivAboveAdic_tmul_one

L898 ↗

Documentation

A diagonal extension-field element has its expected concrete finite component under the ring comparison.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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 finitePlaceTensorRingEquivAboveAdic_tmul_one
    (w : HeightOneSpectrum (𝓞 K))
    (W : {W : HeightOneSpectrum (𝓞 L) //
      finitePlaceBelow (K := K) W = w})
    (x : L) :
    finitePlaceTensorRingEquivAboveAdic
        (K := K) (L := L) w
        ((1 : w.adicCompletion K) ⊗ₜ[K] x) W =
      algebraMap L (W.1.adicCompletion L) x

theorem

infinitePlaceTensorRingEquivAbove_tmul_one

L918 ↗

Documentation

A diagonal extension-field element has its expected concrete archimedean component under the ring comparison.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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 infinitePlaceTensorRingEquivAbove_tmul_one
    (w : InfinitePlace K)
    (W : {W : InfinitePlace L //
      infinitePlaceBelow (K := K) W = w})
    (x : L) :
    infinitePlaceTensorRingEquivAbove
        (K := K) (L := L) w
        ((1 : w.Completion) ⊗ₜ[K] x) W =
      algebraMap L W.1.Completion x

theorem

relativeAdeleBaseChangeRingEquiv_fieldInclusion

L943 ↗

Documentation

The ring comparison carries the diagonal copy of L to the ordinary diagonal adele.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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 relativeAdeleBaseChangeRingEquiv_fieldInclusion
    (x : L) :
    relativeAdeleBaseChangeRingEquiv
        (K := K) (L := L)
        ((1 : NumberField.AdeleRing (𝓞 K) K) ⊗ₜ[K] x) =
      algebraMap L (NumberField.AdeleRing (𝓞 L) L) x

theorem

finitePlaceTensorUnitsEquivAboveAdic_coe

L987 ↗

Documentation

The finite local unit comparison is induced by the corresponding ring equivalence.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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 finitePlaceTensorUnitsEquivAboveAdic_coe
    (w : HeightOneSpectrum (𝓞 K))
    (x : (w.adicCompletion K ⊗[K] L)ˣ)
    (W : {W : HeightOneSpectrum (𝓞 L) //
      finitePlaceBelow (K := K) W = w}) :
    ((finitePlaceTensorUnitsEquivAboveAdic
        (K := K) (L := L) w x W :
        (W.1.adicCompletion L)ˣ) :
        W.1.adicCompletion L) =
      finitePlaceTensorRingEquivAboveAdic
        (K := K) (L := L) w
        (x : w.adicCompletion K ⊗[K] L) W

theorem

relativeFiniteTensorPiMulEquiv_coe

L1008 ↗

Documentation

The flattened finite unit comparison is induced by the flattened finite ring comparison.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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

theorem relativeFiniteTensorPiMulEquiv_coe
    (x : ∀ w : HeightOneSpectrum (𝓞 K),
      (w.adicCompletion K ⊗[K] L)ˣ)
    (W : HeightOneSpectrum (𝓞 L)) :
    ((relativeFiniteTensorPiMulEquiv
        (K := K) (L := L) x W :
        (W.adicCompletion L)ˣ) :
        W.adicCompletion L) =
      relativeFiniteTensorPiRingEquiv
        (K := K) (L := L)
        (fun w =>
          (x w : w.adicCompletion K ⊗[K] L)) W := by
  rw [relativeFiniteTensorPiMulEquiv_apply,
    relativeFiniteTensorPiRingEquiv_apply]
  exact finitePlaceTensorUnitsEquivAboveAdic_coe
    (K := K) (L := L)
    (finitePlaceBelow (K := K) W)
    (x (finitePlaceBelow (K := K) W)) ⟨W, rfl⟩

theorem

relativeIdeleBaseChangeMulEquiv_eq_ringUnits

L1029 ↗

Documentation

The previously constructed idele comparison is the unit-group map induced by the ring comparison.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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 relativeIdeleBaseChangeMulEquiv_eq_ringUnits
    (z : RelativeIdeleGroup K L) :
    IdeleGroup.equivAdeleRingUnits
        (relativeIdeleBaseChangeMulEquiv
          (K := K) (L := L) z) =
      Units.mapEquiv
        (relativeAdeleBaseChangeRingEquiv
          (K := K) (L := L)).toMulEquiv z

theorem

relativeIdeleBaseChangeMulEquiv_principalIdele

L1073 ↗

Documentation

The relative-to-ordinary comparison sends the extension-field diagonal to the ordinary diagonal idele.

Source context 6 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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 relativeIdeleBaseChangeMulEquiv_principalIdele
    (x : Lˣ) :
    relativeIdeleBaseChangeMulEquiv
        (K := K) (L := L)
        (RelativeIdeleGroup.principalIdele K L x) =
      IdeleGroup.principalIdele L x

Module documentation

Scalar extension from relative to ordinary adeles

Declarations