NYLL
Module

RestrictedProduct.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Adele.RestrictedProduct
28 declarations indexed from sourceView source β†—

Module documentation

The restricted local product of a relative adele algebra

Using the chosen finite K-basis of L, a family of local tensor components comes from 𝔸_K βŠ—[K] L precisely when each basis coefficient is integral at almost every finite place. Applying the same condition to a family of local units and to its pointwise inverse gives an exact restricted-product model of the relative idele group.

This construction is independent of the later identification of the chosen-basis lattice with the product of local integer rings.

Imports2
Imported by4

Declarations

structure

RelativeLocalAdeleData

L41 β†—
Documentation

A family of local tensor elements whose chosen-basis coefficients are integral at almost every finite place.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source Β· full declaration
structure RelativeLocalAdeleData where
  /-- The family of archimedean local tensor components. -/
  infinite :
    βˆ€ w : InfinitePlace K,
      w.Completion βŠ—[K] L
  /-- The family of finite local tensor components. -/
  finite :
    βˆ€ w : HeightOneSpectrum (π“ž K),
      w.adicCompletion K βŠ—[K] L
  /-- Every chosen-basis coefficient of the finite family 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) i ∈
          w.adicCompletionIntegers K
theorem

ext

L64 β†—
RelativeLocalAdeleData.ext
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· statement
theorem RelativeLocalAdeleData.ext
    {a b : RelativeLocalAdeleData (K := K) (L := L)}
    (hinfinite : a.infinite = b.infinite)
    (hfinite : a.finite = b.finite) :
    a = b
def

relativeLocalAdeleCoefficient

L75 β†—
Documentation

The i-th base-adele coefficient assembled from local tensor coordinates.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source Β· statement
def relativeLocalAdeleCoefficient
    (a : RelativeLocalAdeleData (K := K) (L := L))
    (i : RelativeAdeleBasisIndex (K := K) (L := L)) :
    NumberField.AdeleRing (π“ž K) K
theorem

relativeLocalAdeleCoefficient_infinite

L95 β†—
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· statement
theorem relativeLocalAdeleCoefficient_infinite
    (a : RelativeLocalAdeleData (K := K) (L := L))
    (i : RelativeAdeleBasisIndex (K := K) (L := L))
    (w : InfinitePlace K) :
    (relativeLocalAdeleCoefficient
      (K := K) (L := L) a i).1 w =
      (Algebra.TensorProduct.basis
          w.Completion
          (relativeExtensionBasis
            (K := K) (L := L))).repr
          (a.infinite w) i
theorem

relativeLocalAdeleCoefficient_finite

L110 β†—
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· statement
theorem relativeLocalAdeleCoefficient_finite
    (a : RelativeLocalAdeleData (K := K) (L := L))
    (i : RelativeAdeleBasisIndex (K := K) (L := L))
    (w : HeightOneSpectrum (π“ž K)) :
    (relativeLocalAdeleCoefficient
      (K := K) (L := L) a i).2 w =
      (Algebra.TensorProduct.basis
          (w.adicCompletion K)
          (relativeExtensionBasis
            (K := K) (L := L))).repr
          (a.finite w) i
def

relativeAdeleOfLocalData

L125 β†—
Documentation

Assemble a restricted family of local tensor elements into a relative adele.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source Β· statement
def relativeAdeleOfLocalData
    (a : RelativeLocalAdeleData (K := K) (L := L)) :
    RelativeAdeleRing K L
theorem

relativeAdeleOfLocalData_infiniteComponent

L135 β†—
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· statement
theorem relativeAdeleOfLocalData_infiniteComponent
    (a : RelativeLocalAdeleData (K := K) (L := L))
    (w : InfinitePlace K) :
    relativeAdeleInfiniteComponent
        (K := K) (L := L) w
        (relativeAdeleOfLocalData
          (K := K) (L := L) a) =
      a.infinite w
theorem

relativeAdeleOfLocalData_finiteComponent

L162 β†—
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· statement
theorem relativeAdeleOfLocalData_finiteComponent
    (a : RelativeLocalAdeleData (K := K) (L := L))
    (w : HeightOneSpectrum (π“ž K)) :
    relativeAdeleFiniteComponent
        (K := K) (L := L) w
        (relativeAdeleOfLocalData
          (K := K) (L := L) a) =
      a.finite w
def

relativeAdeleToLocalData

L189 β†—
Documentation

Extract every local tensor component of a relative adele, together with the restrictedness supplied by its base-adele coefficients.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source Β· full declaration
def relativeAdeleToLocalData
    (z : RelativeAdeleRing K L) :
    RelativeLocalAdeleData (K := K) (L := L) where
  infinite w :=
    relativeAdeleInfiniteComponent
      (K := K) (L := L) w z
  finite w :=
    relativeAdeleFiniteComponent
      (K := K) (L := L) w z
  eventually_integral i := by
    filter_upwards [
      (relativeAdeleCoefficient
        (K := K) (L := L) z i).2.2] with w hw
    rw [relativeAdeleFiniteComponent_basis_repr]
    change
      (relativeAdeleCoefficient
        (K := K) (L := L) z i).2.1 w ∈
          w.adicCompletionIntegers K at hw ⊒
    exact hw
theorem

relativeAdeleOfLocalData_toLocalData

L211 β†—
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· statement
theorem relativeAdeleOfLocalData_toLocalData
    (z : RelativeAdeleRing K L) :
    relativeAdeleOfLocalData
        (K := K) (L := L)
        (relativeAdeleToLocalData
          (K := K) (L := L) z) =
      z
theorem

relativeAdeleToLocalData_ofLocalData

L230 β†—
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· statement
theorem relativeAdeleToLocalData_ofLocalData
    (a : RelativeLocalAdeleData (K := K) (L := L)) :
    relativeAdeleToLocalData
        (K := K) (L := L)
        (relativeAdeleOfLocalData
          (K := K) (L := L) a) =
      a
def

relativeAdeleEquivLocalData

L259 β†—
Documentation

Coordinatewise restricted local tensor families are exactly relative adeles.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source Β· full declaration
def relativeAdeleEquivLocalData :
    RelativeAdeleRing K L ≃
      RelativeLocalAdeleData (K := K) (L := L) where
  toFun :=
    relativeAdeleToLocalData (K := K) (L := L)
  invFun :=
    relativeAdeleOfLocalData (K := K) (L := L)
  left_inv :=
    relativeAdeleOfLocalData_toLocalData
      (K := K) (L := L)
  right_inv :=
    relativeAdeleToLocalData_ofLocalData
      (K := K) (L := L)
structure

RelativeLocalIdeleData

L275 β†—
Documentation

A restricted family of local tensor units. Restrictedness is required both for the family and for its pointwise inverse.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source Β· full declaration
structure RelativeLocalIdeleData where
  /-- The family of archimedean local tensor units. -/
  infinite :
    βˆ€ w : InfinitePlace K,
      (w.Completion βŠ—[K] L)Λ£
  /-- The family of finite local tensor units. -/
  finite :
    βˆ€ w : HeightOneSpectrum (π“ž K),
      (w.adicCompletion K βŠ—[K] L)Λ£
  /-- Every chosen-basis coefficient of the finite family 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 chosen-basis coefficient of the pointwise inverse finite
  family 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

L310 β†—
RelativeLocalIdeleData.ext
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· statement
theorem RelativeLocalIdeleData.ext
    {a b : RelativeLocalIdeleData (K := K) (L := L)}
    (hinfinite : a.infinite = b.infinite)
    (hfinite : a.finite = b.finite) :
    a = b
def

value

L320 β†—
RelativeLocalIdeleData.value
Documentation

Forget local invertibility while retaining the value family.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source Β· full declaration
def RelativeLocalIdeleData.value
    (a : RelativeLocalIdeleData (K := K) (L := L)) :
    RelativeLocalAdeleData (K := K) (L := L) where
  infinite w := a.infinite w
  finite w := a.finite w
  eventually_integral := a.eventually_integral
def

inverse

L328 β†—
RelativeLocalIdeleData.inverse
Documentation

The pointwise inverse family as restricted local adele data.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source Β· full declaration
def RelativeLocalIdeleData.inverse
    (a : RelativeLocalIdeleData (K := K) (L := L)) :
    RelativeLocalAdeleData (K := K) (L := L) where
  infinite w :=
    (↑((a.infinite w)⁻¹) :
      w.Completion βŠ—[K] L)
  finite w :=
    (↑((a.finite w)⁻¹) :
      w.adicCompletion K βŠ—[K] L)
  eventually_integral := a.eventually_inverse_integral
def

relativeIdeleToLocalData

L341 β†—
Documentation

Extract the complete restricted local-unit family of a relative idele.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source Β· full declaration
def relativeIdeleToLocalData
    (z : RelativeIdeleGroup K L) :
    RelativeLocalIdeleData (K := K) (L := L) where
  infinite w :=
    RelativeIdeleGroup.infiniteComponent
      (K := K) (L := L) w z
  finite w :=
    RelativeIdeleGroup.finiteComponent
      (K := K) (L := L) w z
  eventually_integral i := by
    filter_upwards [
      (relativeAdeleCoefficient
        (K := K) (L := L)
      (z : RelativeAdeleRing K L) i).2.2] with w hw
    rw [RelativeIdeleGroup.finiteComponent_coe,
      relativeAdeleFiniteComponent_basis_repr]
    change
      (relativeAdeleCoefficient
        (K := K) (L := L)
        (z : RelativeAdeleRing K L) i).2.1 w ∈
          w.adicCompletionIntegers K at hw ⊒
    exact hw
  eventually_inverse_integral i := by
    filter_upwards [
      (relativeAdeleCoefficient
        (K := K) (L := L)
      ((z⁻¹ : RelativeIdeleGroup K L) :
          RelativeAdeleRing K L) i).2.2] with w hw
    rw [← map_inv
      (RelativeIdeleGroup.finiteComponent
        (K := K) (L := L) w) z,
      RelativeIdeleGroup.finiteComponent_coe,
      relativeAdeleFiniteComponent_basis_repr]
    change
      (relativeAdeleCoefficient
        (K := K) (L := L)
        ((z⁻¹ : RelativeIdeleGroup K L) :
          RelativeAdeleRing K L) i).2.1 w ∈
          w.adicCompletionIntegers K at hw ⊒
    exact hw
def

relativeIdeleOfLocalData

L383 β†—
Documentation

Assemble a restricted local-unit family into a relative idele.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source Β· statement
def relativeIdeleOfLocalData
    (a : RelativeLocalIdeleData (K := K) (L := L)) :
    RelativeIdeleGroup K L
theorem

relativeIdeleOfLocalData_infiniteComponent

L418 β†—
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· statement
theorem relativeIdeleOfLocalData_infiniteComponent
    (a : RelativeLocalIdeleData (K := K) (L := L))
    (w : InfinitePlace K) :
    RelativeIdeleGroup.infiniteComponent
        (K := K) (L := L) w
        (relativeIdeleOfLocalData
          (K := K) (L := L) a) =
      a.infinite w
theorem

relativeIdeleOfLocalData_finiteComponent

L444 β†—
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· statement
theorem relativeIdeleOfLocalData_finiteComponent
    (a : RelativeLocalIdeleData (K := K) (L := L))
    (w : HeightOneSpectrum (π“ž K)) :
    RelativeIdeleGroup.finiteComponent
        (K := K) (L := L) w
        (relativeIdeleOfLocalData
          (K := K) (L := L) a) =
      a.finite w
theorem

relativeIdeleOfLocalData_toLocalData

L470 β†—
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· statement
theorem relativeIdeleOfLocalData_toLocalData
    (z : RelativeIdeleGroup K L) :
    relativeIdeleOfLocalData
        (K := K) (L := L)
        (relativeIdeleToLocalData
          (K := K) (L := L) z) =
      z
theorem

relativeIdeleToLocalData_ofLocalData

L508 β†—
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· statement
theorem relativeIdeleToLocalData_ofLocalData
    (a : RelativeLocalIdeleData (K := K) (L := L)) :
    relativeIdeleToLocalData
        (K := K) (L := L)
        (relativeIdeleOfLocalData
          (K := K) (L := L) a) =
      a
def

relativeIdeleEquivLocalData

L537 β†—
Documentation

The relative idele group is exactly the coordinate-restricted product of all local tensor unit groups.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source Β· full declaration
def relativeIdeleEquivLocalData :
    RelativeIdeleGroup K L ≃
      RelativeLocalIdeleData (K := K) (L := L) where
  toFun :=
    relativeIdeleToLocalData (K := K) (L := L)
  invFun :=
    relativeIdeleOfLocalData (K := K) (L := L)
  left_inv :=
    relativeIdeleOfLocalData_toLocalData
      (K := K) (L := L)
  right_inv :=
    relativeIdeleToLocalData_ofLocalData
      (K := K) (L := L)
instance

relativeLocalIdeleDataGroup

L553 β†—
Documentation

The group structure on the restricted local product, transported through its proved equivalence with the relative idele group.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source Β· statement
instance relativeLocalIdeleDataGroup :
    Group
      (RelativeLocalIdeleData
        (K := K) (L := L))
def

relativeIdeleMulEquivLocalData

L562 β†—
Documentation

The restricted local-product equivalence as a multiplicative equivalence.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source Β· statement
def relativeIdeleMulEquivLocalData :
    RelativeIdeleGroup K L ≃*
      RelativeLocalIdeleData (K := K) (L := L)
theorem

relativeIdeleMulEquivLocalData_apply

L570 β†—
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· statement
theorem relativeIdeleMulEquivLocalData_apply
    (z : RelativeIdeleGroup K L) :
    relativeIdeleMulEquivLocalData
        (K := K) (L := L) z =
      relativeIdeleToLocalData
        (K := K) (L := L) z
theorem

infinite_mul

L580 β†—
RelativeLocalIdeleData.infinite_mul
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· statement
theorem RelativeLocalIdeleData.infinite_mul
    (a b : RelativeLocalIdeleData (K := K) (L := L))
    (w : InfinitePlace K) :
    (a * b).infinite w =
      a.infinite w * b.infinite w
theorem

finite_mul

L607 β†—
RelativeLocalIdeleData.finite_mul
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· statement
theorem RelativeLocalIdeleData.finite_mul
    (a b : RelativeLocalIdeleData (K := K) (L := L))
    (w : HeightOneSpectrum (π“ž K)) :
    (a * b).finite w =
      a.finite w * b.finite w

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