NYLL
Module

SinglePlace.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.SinglePlace
35 declarations indexed from sourceView source ↗

Module documentation

Ideles supported at one place

Local-to-global diagrams use the canonical embedding of a local multiplicative group into the idele group. This file constructs that embedding at finite places and the corresponding one-component relative idele.

Imports3
Imported by18

Declarations

def

infinitePlaceValue

L34 ↗
IdeleGroup.infinitePlaceValue
Documentation

The dependent archimedean value which is x at v and 1 elsewhere.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
variable {K : Type*} [Field K] [NumberField K]
open scoped Classical in
Lean source · statement
def infinitePlaceValue
    (v : InfinitePlace K)
    (x : v.Completionˣ) :
    (w : InfinitePlace K) → w.Completionˣ
theorem

infinitePlaceValue_same

L44 ↗
IdeleGroup.infinitePlaceValue_same
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
variable {K : Type*} [Field K] [NumberField K]
omit [NumberField K] in
Lean source · statement
theorem infinitePlaceValue_same
    (v : InfinitePlace K)
    (x : v.Completionˣ) :
    infinitePlaceValue v x v = x
theorem

infinitePlaceValue_of_ne

L54 ↗
IdeleGroup.infinitePlaceValue_of_ne
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
variable {K : Type*} [Field K] [NumberField K]
omit [NumberField K] in
Lean source · statement
theorem infinitePlaceValue_of_ne
    (v w : InfinitePlace K)
    (x : v.Completionˣ)
    (h : w ≠ v) :
    infinitePlaceValue v x w = 1
def

infinitePlaceIdele

L65 ↗
IdeleGroup.infinitePlaceIdele
Documentation

The idele whose v-component is prescribed and whose other components are 1, for an archimedean place v.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
variable {K : Type*} [Field K] [NumberField K]
Lean source · full declaration
def infinitePlaceIdele
    (v : InfinitePlace K) :
    v.Completionˣ →* IdeleGroup K where
  toFun x :=
    (ContinuousMulEquiv.piUnits.symm
      (infinitePlaceValue v x), 1)
  map_one' := by
    have hvalue : infinitePlaceValue v 1 = 1 := by
      funext w
      by_cases hw : w = v
      · subst w
        exact infinitePlaceValue_same v 1
      · exact infinitePlaceValue_of_ne v w 1 hw
    apply Prod.ext
    · change
        ContinuousMulEquiv.piUnits.symm
            (infinitePlaceValue v 1) = 1
      rw [hvalue, map_one]
    · simp
  map_mul' x y := by
    have hvalue :
        infinitePlaceValue v (x * y) =
          infinitePlaceValue v x * infinitePlaceValue v y := by
      funext w
      by_cases hw : w = v
      · subst w
        simp
      · simp [infinitePlaceValue_of_ne v w x hw,
          infinitePlaceValue_of_ne v w y hw,
          infinitePlaceValue_of_ne v w (x * y) hw]
    apply Prod.ext
    · change
        ContinuousMulEquiv.piUnits.symm
            (infinitePlaceValue v (x * y)) =
          ContinuousMulEquiv.piUnits.symm
              (infinitePlaceValue v x) *
            ContinuousMulEquiv.piUnits.symm
              (infinitePlaceValue v y)
      rw [hvalue, map_mul]
    · simp
theorem

continuous_infinitePlaceIdele

L107 ↗
IdeleGroup.continuous_infinitePlaceIdele
Documentation

Inserting a unit at one archimedean place is continuous.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
variable {K : Type*} [Field K] [NumberField K]
Lean source · statement
theorem continuous_infinitePlaceIdele
    (v : InfinitePlace K) :
    Continuous (infinitePlaceIdele v)
def

infinitePlaceIdeleContinuous

L127 ↗
IdeleGroup.infinitePlaceIdeleContinuous
Documentation

The continuous homomorphism inserting a unit at one archimedean place.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
variable {K : Type*} [Field K] [NumberField K]
Lean source · full declaration
def infinitePlaceIdeleContinuous
    (v : InfinitePlace K) :
    v.Completionˣ →ₜ* IdeleGroup K where
  __ := infinitePlaceIdele v
  continuous_toFun := continuous_infinitePlaceIdele v
theorem

infinitePlaceIdeleContinuous_apply

L134 ↗
IdeleGroup.infinitePlaceIdeleContinuous_apply
Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
variable {K : Type*} [Field K] [NumberField K]
Lean source · statement
theorem infinitePlaceIdeleContinuous_apply
    (v : InfinitePlace K) (x : v.Completionˣ) :
    infinitePlaceIdeleContinuous v x =
      infinitePlaceIdele v x
theorem

infinitePlaceIdele_infiniteComponent_same

L143 ↗
IdeleGroup.infinitePlaceIdele_infiniteComponent_same
Documentation

An archimedean one-place idele recovers its prescribed component at the supporting place.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
variable {K : Type*} [Field K] [NumberField K]
Lean source · statement
theorem infinitePlaceIdele_infiniteComponent_same
    (v : InfinitePlace K)
    (x : v.Completionˣ) :
    IdeleGroup.infiniteComponent v
        (infinitePlaceIdele v x) = x
theorem

infinitePlaceIdele_infiniteComponent_of_ne

L158 ↗
IdeleGroup.infinitePlaceIdele_infiniteComponent_of_ne
Documentation

An archimedean one-place idele has component one at every other archimedean place.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
variable {K : Type*} [Field K] [NumberField K]
Lean source · statement
theorem infinitePlaceIdele_infiniteComponent_of_ne
    (v w : InfinitePlace K)
    (x : v.Completionˣ)
    (h : w ≠ v) :
    IdeleGroup.infiniteComponent w
        (infinitePlaceIdele v x) = 1
theorem

infinitePlaceIdele_finiteComponent

L174 ↗
IdeleGroup.infinitePlaceIdele_finiteComponent
Documentation

An archimedean one-place idele has component one at 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
namespace IdeleGroup
variable {K : Type*} [Field K] [NumberField K]
Lean source · statement
theorem infinitePlaceIdele_finiteComponent
    (v : InfinitePlace K)
    (w : HeightOneSpectrum (𝓞 K))
    (x : v.Completionˣ) :
    IdeleGroup.finiteComponent w
        (infinitePlaceIdele v x) = 1
def

infinitePlaceIdeleClass

L184 ↗
IdeleGroup.infinitePlaceIdeleClass
Documentation

Insert one archimedean-place element and then pass to the idele class group.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
variable {K : Type*} [Field K] [NumberField K]
Lean source · statement
def infinitePlaceIdeleClass
    (v : InfinitePlace K) :
    v.Completionˣ →* IdeleClassGroup K
def

finitePlaceValue

L193 ↗
IdeleGroup.finitePlaceValue
Documentation

The dependent local value which is x at v and 1 elsewhere.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
variable {K : Type*} [Field K] [NumberField K]
open scoped Classical in
Lean source · statement
def finitePlaceValue
    (v : HeightOneSpectrum (𝓞 K))
    (x : (v.adicCompletion K)ˣ)
    (w : HeightOneSpectrum (𝓞 K)) :
    (w.adicCompletion K)ˣ
theorem

finitePlaceValue_same

L201 ↗
IdeleGroup.finitePlaceValue_same
Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
variable {K : Type*} [Field K] [NumberField K]
Lean source · statement
theorem finitePlaceValue_same
    (v : HeightOneSpectrum (𝓞 K))
    (x : (v.adicCompletion K)ˣ) :
    finitePlaceValue v x v = x
theorem

finitePlaceValue_of_ne

L208 ↗
IdeleGroup.finitePlaceValue_of_ne
Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
variable {K : Type*} [Field K] [NumberField K]
Lean source · statement
theorem finitePlaceValue_of_ne
    (v w : HeightOneSpectrum (𝓞 K))
    (x : (v.adicCompletion K)ˣ)
    (h : w ≠ v) :
    finitePlaceValue v x w = 1
def

finitePlaceIdele

L217 ↗
IdeleGroup.finitePlaceIdele
Documentation

The idele whose v-component is prescribed and whose other components are 1.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
variable {K : Type*} [Field K] [NumberField K]
Lean source · full declaration
def finitePlaceIdele
    (v : HeightOneSpectrum (𝓞 K)) :
    (v.adicCompletion K)ˣ →* IdeleGroup K where
  toFun x :=
    (1,
      ⟨finitePlaceValue v x, by
        have hAway :
            ∀ᶠ w : HeightOneSpectrum (𝓞 K) in Filter.cofinite,
              w ≠ v := by
          rw [Filter.eventually_cofinite]
          simp
        filter_upwards [hAway] with w hw
        rw [finitePlaceValue_of_ne v w x hw]
        exact Subgroup.one_mem _⟩)
  map_one' := by
    apply Prod.ext
    · rfl
    · apply RestrictedProduct.ext
      intro w
      change finitePlaceValue v 1 w = (1 : (w.adicCompletion K)ˣ)
      by_cases hw : w = v
      · subst w
        simp
      · simp [finitePlaceValue_of_ne v w 1 hw]
  map_mul' x y := by
    apply Prod.ext
    · simp
    · apply RestrictedProduct.ext
      intro w
      change finitePlaceValue v (x * y) w =
        finitePlaceValue v x w * finitePlaceValue v y w
      by_cases hw : w = v
      · subst w
        simp
      · simp [finitePlaceValue_of_ne v w x hw,
          finitePlaceValue_of_ne v w y hw,
          finitePlaceValue_of_ne v w (x * y) hw]
theorem

finitePlaceIdele_finiteComponent_same

L258 ↗
IdeleGroup.finitePlaceIdele_finiteComponent_same
Documentation

A finite-place idele recovers its prescribed component at the supporting place.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
variable {K : Type*} [Field K] [NumberField K]
Lean source · statement
theorem finitePlaceIdele_finiteComponent_same
    (v : HeightOneSpectrum (𝓞 K))
    (x : (v.adicCompletion K)ˣ) :
    IdeleGroup.finiteComponent v
        (finitePlaceIdele v x) = x
theorem

finitePlaceIdele_finiteComponent_of_ne

L267 ↗
IdeleGroup.finitePlaceIdele_finiteComponent_of_ne
Documentation

A finite-place idele has component one at every other 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
namespace IdeleGroup
variable {K : Type*} [Field K] [NumberField K]
Lean source · statement
theorem finitePlaceIdele_finiteComponent_of_ne
    (v w : HeightOneSpectrum (𝓞 K))
    (x : (v.adicCompletion K)ˣ)
    (h : w ≠ v) :
    IdeleGroup.finiteComponent w
        (finitePlaceIdele v x) = 1
theorem

finitePlaceIdele_infiniteComponent

L277 ↗
IdeleGroup.finitePlaceIdele_infiniteComponent
Documentation

A finite-place idele has component one at every infinite place.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
variable {K : Type*} [Field K] [NumberField K]
Lean source · statement
theorem finitePlaceIdele_infiniteComponent
    (v : HeightOneSpectrum (𝓞 K))
    (w : InfinitePlace K)
    (x : (v.adicCompletion K)ˣ) :
    IdeleGroup.infiniteComponent w
        (finitePlaceIdele v x) = 1
def

finitePlaceIdeleClass

L287 ↗
IdeleGroup.finitePlaceIdeleClass
Documentation

Insert one finite-place element and then pass to the idele class group.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
variable {K : Type*} [Field K] [NumberField K]
Lean source · statement
def finitePlaceIdeleClass
    (v : HeightOneSpectrum (𝓞 K)) :
    (v.adicCompletion K)ˣ →* IdeleClassGroup K
def

relativeInfinitePlaceValue

L308 ↗
RelativeIdeleGroup.relativeInfinitePlaceValue
Documentation

The dependent archimedean tensor value which is z at v and 1 elsewhere.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace RelativeIdeleGroup
section Relative
variable
    {K : Type*} [Field K] [NumberField K]
    {L : Type*} [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
open scoped Classical in
Lean source · statement
def relativeInfinitePlaceValue
    (v : InfinitePlace K)
    (z : (v.Completion ⊗[K] L)ˣ)
    (w : InfinitePlace K) :
    (w.Completion ⊗[K] L)ˣ
theorem

relativeInfinitePlaceValue_same

L317 ↗
RelativeIdeleGroup.relativeInfinitePlaceValue_same
Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace RelativeIdeleGroup
section Relative
variable
    {K : Type*} [Field K] [NumberField K]
    {L : Type*} [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField K] [NumberField L] [FiniteDimensional K L] in
Lean source · statement
theorem relativeInfinitePlaceValue_same
    (v : InfinitePlace K)
    (z : (v.Completion ⊗[K] L)ˣ) :
    relativeInfinitePlaceValue (L := L) v z v = z
theorem

relativeInfinitePlaceValue_of_ne

L325 ↗
RelativeIdeleGroup.relativeInfinitePlaceValue_of_ne
Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace RelativeIdeleGroup
section Relative
variable
    {K : Type*} [Field K] [NumberField K]
    {L : Type*} [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField K] [NumberField L] [FiniteDimensional K L] in
Lean source · statement
theorem relativeInfinitePlaceValue_of_ne
    (v w : InfinitePlace K)
    (z : (v.Completion ⊗[K] L)ˣ)
    (h : w ≠ v) :
    relativeInfinitePlaceValue (L := L) v z w = 1
def

relativeInfinitePlaceData

L333 ↗
RelativeIdeleGroup.relativeInfinitePlaceData
Documentation

Restricted local tensor data supported at one archimedean place.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace RelativeIdeleGroup
section Relative
variable
    {K : Type*} [Field K] [NumberField K]
    {L : Type*} [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source · full declaration
def relativeInfinitePlaceData
    (v : InfinitePlace K)
    (z : (v.Completion ⊗[K] L)ˣ) :
    RelativeLocalIdeleData (K := K) (L := L) where
  infinite w := relativeInfinitePlaceValue (L := L) v z w
  finite _ := 1
  eventually_integral i := by
    have hBase :=
      (relativeIdeleToLocalData
        (K := K) (L := L)
        (1 : RelativeIdeleGroup K L)).eventually_integral i
    filter_upwards [hBase] with w hw
    have hOne :
        (relativeIdeleToLocalData
          (K := K) (L := L)
          (1 : RelativeIdeleGroup K L)).finite w = 1 := by
      change
        RelativeIdeleGroup.finiteComponent
            (K := K) (L := L) w
            (1 : RelativeIdeleGroup K L) = 1
      exact map_one _
    rw [hOne] at hw
    exact hw
  eventually_inverse_integral i := by
    have hBase :=
      (relativeIdeleToLocalData
        (K := K) (L := L)
        (1 : RelativeIdeleGroup K L)).eventually_inverse_integral i
    filter_upwards [hBase] with w hw
    have hOne :
        (relativeIdeleToLocalData
          (K := K) (L := L)
          (1 : RelativeIdeleGroup K L)).finite w = 1 := by
      change
        RelativeIdeleGroup.finiteComponent
            (K := K) (L := L) w
            (1 : RelativeIdeleGroup K L) = 1
      exact map_one _
    rw [hOne] at hw
    exact hw
def

relativeInfinitePlaceIdele

L375 ↗
RelativeIdeleGroup.relativeInfinitePlaceIdele
Documentation

A relative idele supported at the single archimedean place v.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace RelativeIdeleGroup
section Relative
variable
    {K : Type*} [Field K] [NumberField K]
    {L : Type*} [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source · statement
def relativeInfinitePlaceIdele
    (v : InfinitePlace K)
    (z : (v.Completion ⊗[K] L)ˣ) :
    RelativeIdeleGroup K L
theorem

relativeInfinitePlaceIdele_infiniteComponent_same

L387 ↗
RelativeIdeleGroup.relativeInfinitePlaceIdele_infiniteComponent_same
Documentation

A relative archimedean one-place idele recovers its prescribed tensor component at the supporting place.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace RelativeIdeleGroup
section Relative
variable
    {K : Type*} [Field K] [NumberField K]
    {L : Type*} [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source · statement
theorem relativeInfinitePlaceIdele_infiniteComponent_same
    (v : InfinitePlace K)
    (z : (v.Completion ⊗[K] L)ˣ) :
    RelativeIdeleGroup.infiniteComponent
        (K := K) (L := L) v
        (relativeInfinitePlaceIdele (K := K) (L := L) v z) =
      z
theorem

relativeInfinitePlaceIdele_infiniteComponent_of_ne

L402 ↗
RelativeIdeleGroup.relativeInfinitePlaceIdele_infiniteComponent_of_ne
Documentation

A relative archimedean one-place idele has component one at every other archimedean place.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace RelativeIdeleGroup
section Relative
variable
    {K : Type*} [Field K] [NumberField K]
    {L : Type*} [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source · statement
theorem relativeInfinitePlaceIdele_infiniteComponent_of_ne
    (v w : InfinitePlace K)
    (z : (v.Completion ⊗[K] L)ˣ)
    (h : w ≠ v) :
    RelativeIdeleGroup.infiniteComponent
        (K := K) (L := L) w
        (relativeInfinitePlaceIdele (K := K) (L := L) v z) =
      1
theorem

relativeInfinitePlaceIdele_finiteComponent

L418 ↗
RelativeIdeleGroup.relativeInfinitePlaceIdele_finiteComponent
Documentation

A relative archimedean one-place idele has component one at every finite place.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace RelativeIdeleGroup
section Relative
variable
    {K : Type*} [Field K] [NumberField K]
    {L : Type*} [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source · statement
theorem relativeInfinitePlaceIdele_finiteComponent
    (v : InfinitePlace K)
    (w : HeightOneSpectrum (𝓞 K))
    (z : (v.Completion ⊗[K] L)ˣ) :
    RelativeIdeleGroup.finiteComponent
        (K := K) (L := L) w
        (relativeInfinitePlaceIdele (K := K) (L := L) v z) =
      1
def

relativeFinitePlaceValue

L433 ↗
RelativeIdeleGroup.relativeFinitePlaceValue
Documentation

The dependent local tensor value which is z at v and 1 elsewhere.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace RelativeIdeleGroup
section Relative
variable
    {K : Type*} [Field K] [NumberField K]
    {L : Type*} [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
open scoped Classical in
Lean source · statement
def relativeFinitePlaceValue
    (v : HeightOneSpectrum (𝓞 K))
    (z : (v.adicCompletion K ⊗[K] L)ˣ)
    (w : HeightOneSpectrum (𝓞 K)) :
    (w.adicCompletion K ⊗[K] L)ˣ
theorem

relativeFinitePlaceValue_same

L442 ↗
RelativeIdeleGroup.relativeFinitePlaceValue_same
Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace RelativeIdeleGroup
section Relative
variable
    {K : Type*} [Field K] [NumberField K]
    {L : Type*} [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] [FiniteDimensional K L] in
Lean source · statement
theorem relativeFinitePlaceValue_same
    (v : HeightOneSpectrum (𝓞 K))
    (z : (v.adicCompletion K ⊗[K] L)ˣ) :
    relativeFinitePlaceValue (L := L) v z v = z
theorem

relativeFinitePlaceValue_of_ne

L450 ↗
RelativeIdeleGroup.relativeFinitePlaceValue_of_ne
Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace RelativeIdeleGroup
section Relative
variable
    {K : Type*} [Field K] [NumberField K]
    {L : Type*} [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] [FiniteDimensional K L] in
Lean source · statement
theorem relativeFinitePlaceValue_of_ne
    (v w : HeightOneSpectrum (𝓞 K))
    (z : (v.adicCompletion K ⊗[K] L)ˣ)
    (h : w ≠ v) :
    relativeFinitePlaceValue (L := L) v z w = 1
def

relativeFinitePlaceData

L458 ↗
RelativeIdeleGroup.relativeFinitePlaceData
Documentation

Restricted local data supported at one finite place.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace RelativeIdeleGroup
section Relative
variable
    {K : Type*} [Field K] [NumberField K]
    {L : Type*} [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source · full declaration
def relativeFinitePlaceData
    (v : HeightOneSpectrum (𝓞 K))
    (z : (v.adicCompletion K ⊗[K] L)ˣ) :
    RelativeLocalIdeleData (K := K) (L := L) where
  infinite _ := 1
  finite w := relativeFinitePlaceValue (L := L) v z w
  eventually_integral i := by
    have hBase :=
      (relativeIdeleToLocalData
        (K := K) (L := L)
        (1 : RelativeIdeleGroup K L)).eventually_integral i
    have hAway :
        ∀ᶠ w : HeightOneSpectrum (𝓞 K) in Filter.cofinite,
          w ≠ v := by
      rw [Filter.eventually_cofinite]
      simp
    filter_upwards [hBase, hAway] with w hw hne
    have hOne :
        (relativeIdeleToLocalData
          (K := K) (L := L)
          (1 : RelativeIdeleGroup K L)).finite w = 1 := by
      change
        RelativeIdeleGroup.finiteComponent
            (K := K) (L := L) w
            (1 : RelativeIdeleGroup K L) = 1
      exact map_one _
    rw [hOne] at hw
    simpa [relativeFinitePlaceValue_of_ne
      (L := L) v w z hne] using hw
  eventually_inverse_integral i := by
    have hBase :=
      (relativeIdeleToLocalData
        (K := K) (L := L)
        (1 : RelativeIdeleGroup K L)).eventually_inverse_integral i
    have hAway :
        ∀ᶠ w : HeightOneSpectrum (𝓞 K) in Filter.cofinite,
          w ≠ v := by
      rw [Filter.eventually_cofinite]
      simp
    filter_upwards [hBase, hAway] with w hw hne
    have hOne :
        (relativeIdeleToLocalData
          (K := K) (L := L)
          (1 : RelativeIdeleGroup K L)).finite w = 1 := by
      change
        RelativeIdeleGroup.finiteComponent
            (K := K) (L := L) w
            (1 : RelativeIdeleGroup K L) = 1
      exact map_one _
    rw [hOne] at hw
    simpa [relativeFinitePlaceValue_of_ne
      (L := L) v w z hne] using hw
def

relativeFinitePlaceIdele

L512 ↗
RelativeIdeleGroup.relativeFinitePlaceIdele
Documentation

A relative idele supported at the single finite place v.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace RelativeIdeleGroup
section Relative
variable
    {K : Type*} [Field K] [NumberField K]
    {L : Type*} [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source · statement
def relativeFinitePlaceIdele
    (v : HeightOneSpectrum (𝓞 K))
    (z : (v.adicCompletion K ⊗[K] L)ˣ) :
    RelativeIdeleGroup K L
theorem

relativeFinitePlaceIdele_finiteComponent_same

L524 ↗
RelativeIdeleGroup.relativeFinitePlaceIdele_finiteComponent_same
Documentation

A relative finite-place idele recovers its prescribed tensor component at the supporting place.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace RelativeIdeleGroup
section Relative
variable
    {K : Type*} [Field K] [NumberField K]
    {L : Type*} [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source · statement
theorem relativeFinitePlaceIdele_finiteComponent_same
    (v : HeightOneSpectrum (𝓞 K))
    (z : (v.adicCompletion K ⊗[K] L)ˣ) :
    RelativeIdeleGroup.finiteComponent
        (K := K) (L := L) v
        (relativeFinitePlaceIdele (K := K) (L := L) v z) =
      z
theorem

relativeFinitePlaceIdele_finiteComponent_of_ne

L539 ↗
RelativeIdeleGroup.relativeFinitePlaceIdele_finiteComponent_of_ne
Documentation

A relative finite-place idele has component one at every other finite place.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace RelativeIdeleGroup
section Relative
variable
    {K : Type*} [Field K] [NumberField K]
    {L : Type*} [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source · statement
theorem relativeFinitePlaceIdele_finiteComponent_of_ne
    (v w : HeightOneSpectrum (𝓞 K))
    (z : (v.adicCompletion K ⊗[K] L)ˣ)
    (h : w ≠ v) :
    RelativeIdeleGroup.finiteComponent
        (K := K) (L := L) w
        (relativeFinitePlaceIdele (K := K) (L := L) v z) =
      1
theorem

relativeFinitePlaceIdele_infiniteComponent

L555 ↗
RelativeIdeleGroup.relativeFinitePlaceIdele_infiniteComponent
Documentation

A relative finite-place idele has component one at every infinite place.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace RelativeIdeleGroup
section Relative
variable
    {K : Type*} [Field K] [NumberField K]
    {L : Type*} [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source · statement
theorem relativeFinitePlaceIdele_infiniteComponent
    (v : HeightOneSpectrum (𝓞 K))
    (w : InfinitePlace K)
    (z : (v.adicCompletion K ⊗[K] L)ˣ) :
    RelativeIdeleGroup.infiniteComponent
        (K := K) (L := L) w
        (relativeFinitePlaceIdele (K := K) (L := L) v z) =
      1

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