NYLL
Module

BaseChange.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.BaseChange
26 declarations indexed from sourceView source ↗

Module documentation

Scalar extension from relative to ordinary ideles

The finite restricted-product comparison is combined here with the archimedean form of the canonical local tensor decomposition. Infinite places above a fixed infinite place of the base field are identified with exact extensions of its absolute value. Surjectivity is reduced through the finite normal closure to the Galois valuation-extension comparison.

Imports3
Imported by4

Declarations

def

infinitePlaceBelow

L40 ↗
Documentation

Restriction of an infinite place of L to the base 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 infinitePlaceBelow
    (W : InfinitePlace L) : InfinitePlace K
theorem

infinitePlaceBelow_self

L47 ↗
Documentation

Restricting an infinite place along the identity extension fixes it.

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 K] in
Lean source · statement
theorem infinitePlaceBelow_self
    (W : InfinitePlace K) :
    infinitePlaceBelow (K := K) W = W
theorem

infinitePlaceBelow_infinitePlaceBelow

L65 ↗
Documentation

Restriction of infinite places is transitive in a tower of number fields.

Source context 9 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]
section InfinitePlaceTower
variable {M : Type*}
    [Field M] [NumberField M]
    [Algebra K M] [Algebra M L]
    [IsScalarTower K M L]
omit [NumberField K] [NumberField L] [NumberField M]
    [FiniteDimensional K L] in
Lean source · statement
theorem infinitePlaceBelow_infinitePlaceBelow
    (W : InfinitePlace L) :
    infinitePlaceBelow (K := K)
        (infinitePlaceBelow (K := M) W) =
      infinitePlaceBelow (K := K) W
theorem

infinitePlaceCompletionMap_self_apply

L80 ↗
Documentation

The map on infinite-place completions induced by the identity field extension is the identity map.

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 K] in
Lean source · full declaration
theorem infinitePlaceCompletionMap_self_apply
    (W : InfinitePlace K)
    (x : W.Completion) :
    letI : W.1.LiesOver W.1 :=
      ⟨congrArg (fun q : InfinitePlace K => q.1)
        (infinitePlaceBelow_self (K := K) W)⟩
    NumberField.LiesOver.completionMap
        (v := W) (w := W) x = x := by
  let : W.1.LiesOver W.1 :=
    ⟨congrArg (fun q : InfinitePlace K => q.1)
      (infinitePlaceBelow_self (K := K) W)⟩
  refine InfinitePlace.Completion.induction_on W x ?_ ?_
  · exact isClosed_eq
      NumberField.LiesOver.continuous_completionMap
      continuous_id
  · intro y
    change
      NumberField.LiesOver.completionMap
          (y : W.Completion) =
        (y : W.Completion)
    rw [NumberField.LiesOver.completionMap_coe
      (v := W) (w := W) y]
    have hy :
        algebraMap (WithAbs W.1) (WithAbs W.1) y = y := by
      apply (WithAbs.equiv W.1).injective
      change
        algebraMap K K (WithAbs.equiv W.1 y) =
          WithAbs.equiv W.1 y
      rw [Algebra.algebraMap_self]
      rfl
    exact
      congrArg
        (fun z : WithAbs W.1 => (z : W.Completion)) hy
theorem

infinitePlaceCompletionMap_comp_apply

L116 ↗
Documentation

Completion maps at infinite places compose in a tower of number fields.

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 infinitePlaceCompletionMap_comp_apply
    {M : Type*}
    [Field M] [NumberField M]
    [Algebra K M] [Algebra M L]
    [IsScalarTower K M L]
    (W : InfinitePlace L)
    (x :
      (infinitePlaceBelow
        (K := K) W).Completion) :
    let V :=
      infinitePlaceBelow (K := M) W
    let v :=
      infinitePlaceBelow (K := K) W
    letI : V.1.LiesOver v.1 :=
      ⟨congrArg (fun q : InfinitePlace K => q.1)
        (infinitePlaceBelow_infinitePlaceBelow
          (K := K) (M := M) (L := L) W)⟩
    letI : W.1.LiesOver V.1 := ⟨rfl⟩
    letI : W.1.LiesOver v.1 := ⟨rfl⟩
    NumberField.LiesOver.completionMap
        (v := V) (w := W)
        (NumberField.LiesOver.completionMap
          (v := v) (w := V) x) =
      NumberField.LiesOver.completionMap
        (v := v) (w := W) x := by
  dsimp only
  let V :=
    infinitePlaceBelow (K := M) W
  let v :=
    infinitePlaceBelow (K := K) W
  let : V.1.LiesOver v.1 :=
    ⟨congrArg (fun q : InfinitePlace K => q.1)
      (infinitePlaceBelow_infinitePlaceBelow
        (K := K) (M := M) (L := L) W)⟩
  let : W.1.LiesOver V.1 := ⟨rfl⟩
  let : W.1.LiesOver v.1 := ⟨rfl⟩
  refine InfinitePlace.Completion.induction_on v x ?_ ?_
  · exact isClosed_eq
      ((NumberField.LiesOver.continuous_completionMap
          (v := V) (w := W)).comp
        (NumberField.LiesOver.continuous_completionMap
          (v := v) (w := V)))
      (NumberField.LiesOver.continuous_completionMap
        (v := v) (w := W))
  · intro y
    rw [NumberField.LiesOver.completionMap_coe
        (v := v) (w := V) y,
      NumberField.LiesOver.completionMap_coe
        (v := V) (w := W)
        (algebraMap (WithAbs v.1) (WithAbs V.1) y),
      NumberField.LiesOver.completionMap_coe
        (v := v) (w := W) y]
    apply congrArg
      (fun z : WithAbs W.1 => (z : W.Completion))
    apply (WithAbs.equiv W.1).injective
    change
      algebraMap M L
          (algebraMap K M (WithAbs.equiv v.1 y)) =
        algebraMap K L (WithAbs.equiv v.1 y)
    rw [IsScalarTower.algebraMap_apply K M L]
def

infinitePlaceAboveToExtension

L179 ↗
Documentation

An infinite place above w, regarded as an exact extension of the underlying 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
def infinitePlaceAboveToExtension
    (w : InfinitePlace K)
    (W : {W : InfinitePlace L //
      infinitePlaceBelow (K := K) W = w}) :
    AbsoluteValueExtension w.1 L
theorem

infinitePlaceAboveToExtension_surjective_of_isGalois

L194 ↗
Documentation

For a finite Galois extension, every extension of an infinite-place absolute value is represented by an infinite place above the base place.

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 K] [NumberField L] [FiniteDimensional K L] in
Lean source · statement
theorem
    infinitePlaceAboveToExtension_surjective_of_isGalois
    [IsGalois K L]
    (w : InfinitePlace K) :
    Function.Surjective
      (infinitePlaceAboveToExtension
        (K := K) (L := L) w)
def

infinitePlaceAboveEquivExtension

L230 ↗
Documentation

Infinite places of L above w are exactly the exact extensions of the absolute value represented by w.

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 infinitePlaceAboveEquivExtension
    (w : InfinitePlace K) :
    {W : InfinitePlace L //
      infinitePlaceBelow (K := K) W = w} ≃
      AbsoluteValueExtension w.1 L
theorem

infinitePlaceAboveEquivExtension_apply_val

L298 ↗
Documentation

The absolute value underlying the extension corresponding to an infinite place above w.

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 infinitePlaceAboveEquivExtension_apply_val
    (w : InfinitePlace K)
    (W : {W : InfinitePlace L //
      infinitePlaceBelow (K := K) W = w}) :
    (infinitePlaceAboveEquivExtension
      (K := K) (L := L) w W).1 = W.1.1
def

infiniteCompletionProductReindexAbove

L308 ↗
Documentation

Reindex the relative completion product by actual infinite places above w.

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 infiniteCompletionProductReindexAbove
    (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

infiniteCompletionProductEquivAbove

L330 ↗
Documentation

Replace the absolute-value completion in every factor by mathlib's concrete infinite-place completion.

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 infiniteCompletionProductEquivAbove
    (w : InfinitePlace K) :
    (∀ u : AbsoluteValueExtension w.1 L,
      u.1.Completionˣ) ≃*
      ∀ W : {W : InfinitePlace L //
          infinitePlaceBelow (K := K) W = w},
        W.1.Completionˣ
def

infinitePlaceTensorUnitsEquivAbove

L345 ↗
Documentation

The canonical local tensor decomposition for the actual archimedean tensor component, with codomain indexed by concrete infinite places above the 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 infinitePlaceTensorUnitsEquivAbove
    (w : InfinitePlace K) :
    (w.Completion ⊗[K] L)ˣ ≃*
      ∀ W : {W : InfinitePlace L //
          infinitePlaceBelow (K := K) W = w},
        W.1.Completionˣ
theorem

infinitePlaceTensorUnitsEquivAbove_apply

L366 ↗
Documentation

Evaluation formula for the archimedean relative-to-ordinary comparison at a concrete infinite place above the 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 infinitePlaceTensorUnitsEquivAbove_apply
    (w : InfinitePlace K)
    (z : (w.Completion ⊗[K] L)ˣ)
    (W : {W : InfinitePlace L //
      infinitePlaceBelow (K := K) W = w}) :
    infinitePlaceTensorUnitsEquivAbove
        (K := K) (L := L) w z W =
      Units.mapEquiv
          (InfinitePlace.Completion.equiv W.1).symm.toMulEquiv
        (localTensorUnitsEquivCompletionProduct
          w.1 w.isNontrivial
          (infinitePlaceLocalTensorUnitsEquiv
            (K := K) (L := L) w z)
        (infinitePlaceAboveEquivExtension
          (K := K) (L := L) w W))
theorem

infinitePlaceLocalTensorUnitsEquiv_infiniteLocalIdeleInclusion_coe

L388 ↗
Documentation

After replacing the concrete completion by the underlying absolute-value completion, scalar extension of a local unit is the pure tensor with right factor one.

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 K] [NumberField L] [FiniteDimensional K L] in
Lean source · statement
theorem infinitePlaceLocalTensorUnitsEquiv_infiniteLocalIdeleInclusion_coe
    (w : InfinitePlace K) (x : w.Completionˣ) :
    (infinitePlaceLocalTensorUnitsEquiv
        (K := K) (L := L) w
        (infiniteLocalIdeleInclusion
          (K := K) (L := L) w x) :
      LocalClassFieldTheory.LocalTensorAlgebra (L := L) w.1) =
      infinitePlaceCompletionAlgEquiv w
          (x : w.Completion) ⊗ₜ[K] (1 : L)
theorem

infinitePlaceTensorUnitsEquivAbove_localFieldIdeleInclusion

L401 ↗
Documentation

On a diagonal extension-field unit, the infinite local relative-to-ordinary comparison is the ordinary diagonal embedding.

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 infinitePlaceTensorUnitsEquivAbove_localFieldIdeleInclusion
    (w : InfinitePlace K)
    (W : {W : InfinitePlace L //
      infinitePlaceBelow (K := K) W = w})
    (x : Lˣ) :
    infinitePlaceTensorUnitsEquivAbove
        (K := K) (L := L) w
        (infiniteLocalFieldIdeleInclusion
          (K := K) (L := L) w x) W =
      Units.map
        (algebraMap L W.1.Completion)
        x
def

infinitePlaceAbovePiMulEquiv

L431 ↗
Documentation

Flatten the products over base infinite places and places above them to the product over all infinite places 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 infinitePlaceAbovePiMulEquiv :
    (∀ 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_mul' f g := by
    funext W
    rfl
def

relativeInfiniteTensorPiMulEquiv

L454 ↗
Documentation

The unrestricted product of all archimedean tensor-unit factors is the product of the concrete archimedean local unit groups 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 · statement
def relativeInfiniteTensorPiMulEquiv :
    (∀ w : InfinitePlace K,
      (w.Completion ⊗[K] L)ˣ) ≃*
      ∀ W : InfinitePlace L, W.Completionˣ
theorem

relativeInfiniteTensorPiMulEquiv_apply

L467 ↗
Documentation

Evaluation of the archimedean tensor-product comparison at an infinite place 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
theorem relativeInfiniteTensorPiMulEquiv_apply
    (f : ∀ w : InfinitePlace K, (w.Completion ⊗[K] L)ˣ)
    (W : InfinitePlace L) :
    relativeInfiniteTensorPiMulEquiv (K := K) (L := L) f W =
      infinitePlaceTensorUnitsEquivAbove
        (K := K) (L := L)
        (infinitePlaceBelow (K := K) W)
        (f (infinitePlaceBelow (K := K) W))
        ⟨W, rfl⟩
def

relativeInfiniteIdeleMulEquiv

L479 ↗
Documentation

The archimedean relative tensor factors form the ordinary infinite idele group 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 · statement
def relativeInfiniteIdeleMulEquiv :
    (∀ w : InfinitePlace K,
      (w.Completion ⊗[K] L)ˣ) ≃*
      InfiniteIdeleGroup L
theorem

finite_mul

L490 ↗
RelativeFiniteIdeleData.finite_mul
Documentation

Multiplication in the transported finite relative restricted product is pointwise on its local tensor factors.

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 RelativeFiniteIdeleData.finite_mul
    (a b : RelativeFiniteIdeleData (K := K) (L := L))
    (w : HeightOneSpectrum (𝓞 K)) :
    (a * b).finite w = a.finite w * b.finite w
def

toFiniteData

L508 ↗
RelativeLocalIdeleData.toFiniteData
Documentation

Forget the infinite component of restricted local idele 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 RelativeLocalIdeleData.toFiniteData
    (a : RelativeLocalIdeleData (K := K) (L := L)) :
    RelativeFiniteIdeleData (K := K) (L := L) where
  finite := a.finite
  eventually_integral := a.eventually_integral
  eventually_inverse_integral :=
    a.eventually_inverse_integral
theorem

toFiniteData_mul

L519 ↗
RelativeLocalIdeleData.toFiniteData_mul
Documentation

Passing relative local idele data to finite data preserves multiplication.

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 RelativeLocalIdeleData.toFiniteData_mul
    (a b : RelativeLocalIdeleData (K := K) (L := L)) :
    (a * b).toFiniteData =
      a.toFiniteData * b.toFiniteData
def

relativeLocalIdeleDataSplitMulEquiv

L532 ↗
Documentation

Split restricted local idele data into its unrestricted infinite part and finite restricted part.

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 relativeLocalIdeleDataSplitMulEquiv :
    RelativeLocalIdeleData (K := K) (L := L) ≃*
      ((∀ w : InfinitePlace K,
          (w.Completion ⊗[K] L)ˣ) ×
        RelativeFiniteIdeleData (K := K) (L := L)) where
  toFun a :=
    ⟨a.infinite, a.toFiniteData⟩
  invFun a :=
    { infinite := a.1
      finite := a.2.finite
      eventually_integral := a.2.eventually_integral
      eventually_inverse_integral :=
        a.2.eventually_inverse_integral }
  left_inv a := by
    apply RelativeLocalIdeleData.ext <;> rfl
  right_inv a := by
    rcases a with ⟨a, b⟩
    rfl
  map_mul' a b := by
    apply Prod.ext
    · funext w
      exact RelativeLocalIdeleData.infinite_mul
        (K := K) (L := L) a b w
    · exact RelativeLocalIdeleData.toFiniteData_mul
        (K := K) (L := L) a b
def

relativeIdeleBaseChangeMulEquiv

L560 ↗
Documentation

Scalar extension identifies the actual relative idele group I_K ⊗_K L with the ordinary idele group I_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 · statement
def relativeIdeleBaseChangeMulEquiv :
    RelativeIdeleGroup K L ≃* IdeleGroup L
theorem

relativeIdeleBaseChangeMulEquiv_infinite

L574 ↗
Documentation

The infinite component of the relative idele base-change 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 relativeIdeleBaseChangeMulEquiv_infinite
    (z : RelativeIdeleGroup K L) :
    (relativeIdeleBaseChangeMulEquiv
      (K := K) (L := L) z).1 =
      relativeInfiniteIdeleMulEquiv
        (K := K) (L := L)
        (relativeIdeleToLocalData
          (K := K) (L := L) z).infinite
theorem

relativeIdeleBaseChangeMulEquiv_finite

L587 ↗
Documentation

The finite component of the relative idele base-change 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 relativeIdeleBaseChangeMulEquiv_finite
    (z : RelativeIdeleGroup K L) :
    (relativeIdeleBaseChangeMulEquiv
      (K := K) (L := L) z).2 =
      relativeFiniteIdeleToFiniteIdele
        (K := K) (L := L)
        (relativeIdeleToLocalData
          (K := K) (L := L) z).toFiniteData

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