Module

FiniteRestrictedProductBaseChange.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Adele.FiniteRestrictedProductBaseChange

24 declarations indexed from sourceView source ↗

Module documentation

Finite restricted products under scalar extension

This file flattens the finite local tensor factors of a relative idele over K into the ordinary finite-place factors of L. The local map is The canonical local tensor decomposition followed by the comparison between an exact-extension completion and the concrete adic completion at its centre.

The main point is restrictedness: coefficientwise restrictedness in a fixed K-basis of L is equivalent, up to the already isolated finite comparison set, to the usual valuation-ring-unit condition at almost every finite place of L.

Imports3

Imported by3

def

piCongrLeftMulEquiv

L45 ↗

Documentation

Reindex a dependent product along an equivalence, retaining its coordinatewise multiplicative structure.

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 piCongrLeftMulEquiv
    {ι ι' : Type*} (M : ι' → Type*)
    [∀ i, Mul (M i)] (e : ι ≃ ι') :
    (∀ i, M (e i)) ≃* ∀ j, M j where
  toEquiv := Equiv.piCongrLeft M e
  map_mul' f g := by
    funext j
    obtain ⟨i, rfl⟩ := e.surjective j
    change
      Equiv.piCongrLeft M e (f * g) (e i) =
        Equiv.piCongrLeft M e f (e i) *
          Equiv.piCongrLeft M e g (e i)
    rw [Equiv.piCongrLeft_apply_apply,
      Equiv.piCongrLeft_apply_apply,
      Equiv.piCongrLeft_apply_apply]
    rfl

def

finitePlaceTensorUnitsEquivAboveAdic

L65 ↗

Documentation

At one finite place of K, the canonical local tensor decomposition followed by completion comparison identifies the tensor-unit group with the product of the concrete adic unit groups at all finite places of L above it.

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 finitePlaceTensorUnitsEquivAboveAdic
    (w : HeightOneSpectrum (𝓞 K)) :
    (w.adicCompletion K ⊗[K] L)ˣ ≃*
      ∀ W : {W : HeightOneSpectrum (𝓞 L) //
          finitePlaceBelow (K := K) W = w},
        (W.1.adicCompletion L)ˣ

theorem

finitePlaceTensorUnitsEquivAboveAdic_apply_extension

L89 ↗

Documentation

Evaluation of the finite-place tensor units 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 finitePlaceTensorUnitsEquivAboveAdic_apply_extension
    (w : HeightOneSpectrum (𝓞 K))
    (x : (w.adicCompletion K ⊗[K] L)ˣ)
    (u : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K w) L) :
    finitePlaceTensorUnitsEquivAboveAdic
        (K := K) (L := L) w x
        (finitePlaceExtensionEquivAbove
          (K := K) (L := L) w u) =
      Units.mapEquiv
          (finitePlaceExtensionAdicCompletionRingEquiv
            (K := K) (L := L) w u).toMulEquiv
        (finitePlaceLocalTensorDecompositionUnitsComponent
          (K := K) (L := L) w u x)

theorem

finitePlaceTensorUnitsEquivAboveAdic_localFieldIdeleInclusion

L125 ↗

Documentation

On a diagonal extension-field unit, the finite 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 finitePlaceTensorUnitsEquivAboveAdic_localFieldIdeleInclusion
    (w : HeightOneSpectrum (𝓞 K))
    (W : {W : HeightOneSpectrum (𝓞 L) //
      finitePlaceBelow (K := K) W = w})
    (x : Lˣ) :
    finitePlaceTensorUnitsEquivAboveAdic
        (K := K) (L := L) w
        (localFieldIdeleInclusion
          (K := K) (L := L) w x) W =
      Units.map
        (FinitePlace.embedding (K := L) W.1)
        x

def

finitePlaceAbovePiMulEquiv

L159 ↗

Documentation

Flatten products first over finite places of K and then over places above them into one product over all finite 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 finitePlaceAbovePiMulEquiv :
    (∀ 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_mul' f g := by
    funext W
    rfl

def

relativeFiniteTensorPiMulEquiv

L183 ↗

Documentation

The unrestricted product of all finite local tensor-unit groups is the unrestricted product of all concrete finite 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 relativeFiniteTensorPiMulEquiv :
    (∀ w : HeightOneSpectrum (𝓞 K),
      (w.adicCompletion K ⊗[K] L)ˣ) ≃*
      ∀ W : HeightOneSpectrum (𝓞 L),
        (W.adicCompletion L)ˣ

theorem

relativeFiniteTensorPiMulEquiv_apply

L196 ↗

Documentation

Coordinate formula for the relative finite tensor units 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 relativeFiniteTensorPiMulEquiv_apply
    (x : ∀ w : HeightOneSpectrum (𝓞 K),
      (w.adicCompletion K ⊗[K] L)ˣ)
    (W : HeightOneSpectrum (𝓞 L)) :
    relativeFiniteTensorPiMulEquiv
        (K := K) (L := L) x W =
      finitePlaceTensorUnitsEquivAboveAdic
        (K := K) (L := L)
        (finitePlaceBelow (K := K) W)
        (x (finitePlaceBelow (K := K) W)) ⟨W, rfl⟩

theorem

relativeFiniteTensorPiMulEquiv_symm_apply

L211 ↗

Documentation

Coordinate formula for the inverse relative finite tensor units 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 relativeFiniteTensorPiMulEquiv_symm_apply
    (y : ∀ W : HeightOneSpectrum (𝓞 L),
      (W.adicCompletion L)ˣ)
    (w : HeightOneSpectrum (𝓞 K)) :
    (relativeFiniteTensorPiMulEquiv
        (K := K) (L := L)).symm y w =
      (finitePlaceTensorUnitsEquivAboveAdic
        (K := K) (L := L) w).symm
        (fun W => y W.1) :=
  rfl

theorem

unitsMapEquiv_mem_units_iff

L225 ↗

Documentation

A multiplicative equivalence carries units of one submonoid to units of another exactly when it carries their underlying elements between the two submonoids.

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 unitsMapEquiv_mem_units_iff
    {R S : Type*} [CommMonoid R] [CommMonoid S]
    (e : R ≃* S) (A : Submonoid R) (B : Submonoid S)
    (h : ∀ y : R, e y ∈ B ↔ y ∈ A)
    (x : Rˣ) :
    Units.mapEquiv e x ∈ B.units ↔ x ∈ A.units

theorem

relativeLocalTensorDecompositionIntegralUnitAt_iff_aboveAdic

L248 ↗

Documentation

The local tensor unit is integral in every relative-tensor factor exactly when its flattened concrete components are local integer units at every finite 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 relativeLocalTensorDecompositionIntegralUnitAt_iff_aboveAdic
    (w : HeightOneSpectrum (𝓞 K))
    (x : (w.adicCompletion K ⊗[K] L)ˣ) :
    RelativeLocalTensorDecompositionIntegralUnitAt
        (K := K) (L := L) w x ↔
      ∀ W : {W : HeightOneSpectrum (𝓞 L) //
          finitePlaceBelow (K := K) W = w},
        finitePlaceTensorUnitsEquivAboveAdic
            (K := K) (L := L) w x W ∈
          (W.1.adicCompletionIntegers L).units

theorem

eventually_finitePlace_iff_eventually_all_above

L308 ↗

Documentation

Cofinite quantification over finite places of L is equivalent to cofinite quantification over finite places of K, uniformly over every 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 eventually_finitePlace_iff_eventually_all_above
    (P : ∀ _W : HeightOneSpectrum (𝓞 L), Prop) :
    (∀ᶠ W : HeightOneSpectrum (𝓞 L) in Filter.cofinite, P W) ↔
      ∀ᶠ w : HeightOneSpectrum (𝓞 K) in Filter.cofinite,
        ∀ W : {W : HeightOneSpectrum (𝓞 L) //
          finitePlaceBelow (K := K) W = w},
          P W.1

structure

RelativeFiniteIdeleData

L365 ↗

Documentation

The finite part of the relative restricted local product. This is the source model whose flattening is the ordinary finite 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 · full declaration

structure RelativeFiniteIdeleData where
  /-- The unit in each finite local tensor factor. -/
  finite :
    ∀ w : HeightOneSpectrum (𝓞 K),
      (w.adicCompletion K ⊗[K] L)ˣ
  /-- Every basis coordinate of the finite component is integral at
  all but finitely many places. -/
  eventually_integral :
    ∀ i : RelativeAdeleBasisIndex (K := K) (L := L),
      ∀ᶠ w : HeightOneSpectrum (𝓞 K) in Filter.cofinite,
        (Algebra.TensorProduct.basis
            (w.adicCompletion K)
            (relativeExtensionBasis
              (K := K) (L := L))).repr
            (finite w : w.adicCompletion K ⊗[K] L) i ∈
          w.adicCompletionIntegers K
  /-- Every basis coordinate of the inverse finite component is integral
  at all but finitely many places. -/
  eventually_inverse_integral :
    ∀ i : RelativeAdeleBasisIndex (K := K) (L := L),
      ∀ᶠ w : HeightOneSpectrum (𝓞 K) in Filter.cofinite,
        (Algebra.TensorProduct.basis
            (w.adicCompletion K)
            (relativeExtensionBasis
              (K := K) (L := L))).repr
            (↑((finite w)⁻¹) :
              w.adicCompletion K ⊗[K] L) i ∈
          w.adicCompletionIntegers K

theorem

ext

L398 ↗

RelativeFiniteIdeleData.ext

Documentation

Relative finite idele data are equal when their finite components are equal.

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 RelativeFiniteIdeleData.ext
    {a b : RelativeFiniteIdeleData (K := K) (L := L)}
    (hfinite : a.finite = b.finite) :
    a = b

def

toLocalData

L408 ↗

RelativeFiniteIdeleData.toLocalData

Documentation

Adjoin the trivial infinite family, so that the established relative idele support theorem can be applied to finite restricted 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 RelativeFiniteIdeleData.toLocalData
    (a : RelativeFiniteIdeleData (K := K) (L := L)) :
    RelativeLocalIdeleData (K := K) (L := L) where
  infinite _ := 1
  finite := a.finite
  eventually_integral := a.eventually_integral
  eventually_inverse_integral := a.eventually_inverse_integral

theorem

eventually_aboveAdicUnit

L418 ↗

RelativeFiniteIdeleData.eventually_aboveAdicUnit

Documentation

A finite relative restricted family is integral in every concrete completion factor over almost every base 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 RelativeFiniteIdeleData.eventually_aboveAdicUnit
    (a : RelativeFiniteIdeleData (K := K) (L := L)) :
    ∀ᶠ w : HeightOneSpectrum (𝓞 K) in Filter.cofinite,
      ∀ W : {W : HeightOneSpectrum (𝓞 L) //
          finitePlaceBelow (K := K) W = w},
        finitePlaceTensorUnitsEquivAboveAdic
            (K := K) (L := L) w (a.finite w) W ∈
          (W.1.adicCompletionIntegers L).units

def

relativeFiniteIdeleToFiniteIdele

L442 ↗

Documentation

Flatten a finite relative restricted family into an ordinary finite idele 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 relativeFiniteIdeleToFiniteIdele
    (a : RelativeFiniteIdeleData (K := K) (L := L)) :
    FiniteIdeleGroup L

theorem

relativeFiniteIdeleToFiniteIdele_apply

L462 ↗

Documentation

Evaluation of the map from relative finite idele data to finite ideles.

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 relativeFiniteIdeleToFiniteIdele_apply
    (a : RelativeFiniteIdeleData (K := K) (L := L))
    (W : HeightOneSpectrum (𝓞 L)) :
    relativeFiniteIdeleToFiniteIdele
        (K := K) (L := L) a W =
      relativeFiniteTensorPiMulEquiv
        (K := K) (L := L) a.finite W

def

finiteIdeleRelativeTensorFamily

L473 ↗

Documentation

Pull an ordinary finite idele back to the unrestricted family of finite tensor-unit 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

def finiteIdeleRelativeTensorFamily
    (y : FiniteIdeleGroup L) :
    ∀ w : HeightOneSpectrum (𝓞 K),
      (w.adicCompletion K ⊗[K] L)ˣ

theorem

finiteIdeleRelativeTensorFamily_eventually_basisIntegralUnit

L482 ↗

Documentation

The pulled-back tensor family is basis-integral, together with its inverse, at almost every finite place of K.

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 finiteIdeleRelativeTensorFamily_eventually_basisIntegralUnit
    (y : FiniteIdeleGroup L) :
    ∀ᶠ w : HeightOneSpectrum (𝓞 K) in Filter.cofinite,
      RelativeBasisIntegralUnitAt
        (K := K) (L := L) w
        (finiteIdeleRelativeTensorFamily
          (K := K) (L := L) y w)

def

finiteIdeleToRelativeFiniteIdeleData

L524 ↗

Documentation

Pull an ordinary finite idele back to finite relative restricted 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 finiteIdeleToRelativeFiniteIdeleData
    (y : FiniteIdeleGroup L) :
    RelativeFiniteIdeleData (K := K) (L := L) where
  finite :=
    finiteIdeleRelativeTensorFamily
      (K := K) (L := L) y
  eventually_integral i :=
    (finiteIdeleRelativeTensorFamily_eventually_basisIntegralUnit
      (K := K) (L := L) y).mono fun w hw =>
        relativeBasisIntegralAt_repr_mem
          (K := K) (L := L) w _ hw.1 i
  eventually_inverse_integral i :=
    (finiteIdeleRelativeTensorFamily_eventually_basisIntegralUnit
      (K := K) (L := L) y).mono fun w hw =>
        relativeBasisIntegralAt_repr_mem
          (K := K) (L := L) w _ hw.2 i

def

relativeFiniteIdeleEquiv

L543 ↗

Documentation

The finite relative restricted product is the ordinary finite idele group 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 relativeFiniteIdeleEquiv :
    RelativeFiniteIdeleData (K := K) (L := L) ≃
      FiniteIdeleGroup L where
  toFun :=
    relativeFiniteIdeleToFiniteIdele
      (K := K) (L := L)
  invFun :=
    finiteIdeleToRelativeFiniteIdeleData
      (K := K) (L := L)
  left_inv a := by
    apply RelativeFiniteIdeleData.ext
    change
      (relativeFiniteTensorPiMulEquiv
        (K := K) (L := L)).symm
          (relativeFiniteTensorPiMulEquiv
            (K := K) (L := L) a.finite) =
        a.finite
    exact
      (relativeFiniteTensorPiMulEquiv
        (K := K) (L := L)).symm_apply_apply a.finite
  right_inv y := by
    apply Subtype.ext
    change
      relativeFiniteTensorPiMulEquiv
          (K := K) (L := L)
          ((relativeFiniteTensorPiMulEquiv
            (K := K) (L := L)).symm (fun W => y W)) =
        fun W => y W
    exact
      (relativeFiniteTensorPiMulEquiv
        (K := K) (L := L)).apply_symm_apply (fun W => y W)

instance

relativeFiniteIdeleDataGroup

L577 ↗

Documentation

The transported group structure on the finite relative restricted product.

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

instance relativeFiniteIdeleDataGroup :
    Group (RelativeFiniteIdeleData (K := K) (L := L))

def

relativeFiniteIdeleMulEquiv

L584 ↗

Documentation

The finite restricted-product comparison as a multiplicative 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

def relativeFiniteIdeleMulEquiv :
    RelativeFiniteIdeleData (K := K) (L := L) ≃*
      FiniteIdeleGroup L

theorem

relativeFiniteIdeleMulEquiv_apply

L593 ↗

Documentation

The relative finite idele equivalence agrees with the underlying finite-idele map.

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 relativeFiniteIdeleMulEquiv_apply
    (a : RelativeFiniteIdeleData (K := K) (L := L)) :
    relativeFiniteIdeleMulEquiv
        (K := K) (L := L) a =
      relativeFiniteIdeleToFiniteIdele
        (K := K) (L := L) a

Module documentation

Finite restricted products under scalar extension

Declarations