isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul

Stream: FLT

[Kevin Buzzard]

I'm travelling until Monday but let me try and write down where we are. The lemma in the title, Theorem 10.36 as I type, is basically all that is left for the finiteness result which many people have been working towards since basically when the grant started 1.25 years ago. It's the claim that if $B$ is a finite-dimensional central simple algebra over a number field $K$, if $B_{\mathbb{A}}:=B\otimes_K\mathbb{A}_K$ is the corresponding second-countable locally-compact topological ring (it's free of finite rank over $\mathbb{A}_K$ so give it the module topology), and if $u\in B_{\mathbb{A}}^\times$, then left and right multiplication by $u$ scale Haar measure on $B_{\mathbb{A}}$ by the same amount.

First note that this claim that left multiplication and right multiplication scale things in the same way is not completely formal. The example at the beginning of section 10.5 of the FLT notes shows that even for an algebra finite-dimensional over the real numbers, left and right multiplication by a unit don't always scale Haar measure by the same factor, because they might not have the same determinant. However for central simple algebras the result is true, and this is because such algebras are only a finite base extension away from matrix algebras, and for matrix algebras over a field one can do a concrete calculation to check that left and right multiplication by a matrix have the same determinant and thus scale Haar measure by the same amount. See for example Lemma 10.20 which proves the result for fields. That lemma is formalized.

I had imagined that proving the adelic result would be simple from the field result; adeles are restricted products of fields and we have already proved that Haar characters of restricted products are products of the Haar characters of the factors, which I had imagined would reduce the adelic claim to the field claim. But there are subtleties here. My previous experience with results of the form "doing something to factors and then taking the restricted product is the same as taking the restricted product and then doing something to that" was that these things were a real joy to prove. But "taking tensor products over $K$" is not one of those things because it doesn't make sense to tensor local data with a $K$-algebra because the integer ring is not a $K$-module.

My first attempt to get around this was FLT#820, an unfinished PR where I attempted to tensor over the integers of $K$ instead. I think that in theory this approach could be pushed through but it will involve making a bunch more API, and given that I'm going to be starting on something totally different after this finiteness theorem is proved I'm not particularly motivated to do this (although I might end up having to). One key thing which we'll need (and which we may or may not have) is that if $\Lambda$ is a finite free $\mathbb{O}_K$-module then the obvious isomorphism $\Lambda\otimes_{\mathcal{O}_K}\mathbb{A}_K^f=\prod'_{v<\infty}[\Lambda\otimes_{\mathcal{O}_K}K_v;\Lambda\otimes_{\mathcal{O}_K}\mathcal{O}_v]$ is a homeomorphism, where the LHS gets the $\mathbb{A}_K^f$-module topology, and the RHS gets the restricted product topology. This is just the sort of "invisible mathematics" which I had never even noticed was an issue until I started formalizing this stuff; there cannot be an error here because if there were a subtlety then it would have surfaced decades ago, but it still needs checking.

So I would kind of like to avoid this, and although I've not really got time to think right now, IIRC I did at some stage think about "raising to the $$n$$th power" commuting with restricted product (edit: indeed I did). In particular here is a proof that $(\mathbb{A}_K^f)^n=\prod'_{v<\infty}[K_v^n;\mathcal{O}_v^n]$ topologically. So I'm wondering if a less painful way to the proof we need is to immediately pick a basis for $B/K$ and try and get a formula for the Haar character of left/right multiplication of the unit as products of local factors; this will I hope enable us to avoid having to descend to the integral level which will I think basically halve the amount of fiddly work which we need to do.

[Kevin Buzzard]

The other things we need to do is to get from the finite adeles to the full adeles, and William Coram had to deal with this in his work on the finiteness result. In particular see https://github.com/ImperialCollegeLondon/FLT/blob/68842d4145ce6a62206855c1dcd806c5a08c93e5/FLT/DivisionAlgebra/Finiteness.lean#L338 for the claim that D tensor adele ring is homeomorphic and additively isomorphic to (D tensor finite adeles) x (D tensor infinite adeles). This stuff is all in the wrong place I guess; it should be moved earlier because I conjecture that we can't import that file in the file where the sorry we're trying to fill is. But perhaps the relevant ideas are there.

In summary then;

(1) I'm unlikely to do anything myself on this until Monday 5th but on Monday 5th I will be working on this for several hours a day
(2) I think we should avoid having to tensor with integer rings and instead follow the proof in the blueprint and pick a basis
(3) There are two independent problems; going from adeles to finite x infinite, and going from finite to product of p-adic; the first should be inspired by D𝔸_prodRight''.

[Kevin Buzzard]

@Bryan Wang I did get a chance to think about this a bit today: I think this code might help:

import Mathlib

namespace RestrictedProduct

variable {ι : Type*} [DecidableEq ι] {R : Type*} [Semiring R] (A : ι → Type*) {𝓕 : Filter ι}
    {S : ι → Type*}
    [(i : ι) → SetLike (S i) (A i)] {B : (i : ι) → S i} (j : ι) [(i : ι) → AddCommMonoid (A i)]
    [(i : ι) → Module R (A i)] [∀ (i : ι), AddSubmonoidClass (S i) (A i)]

example (j : ι) : Πʳ i, [A i, B i] →+ A j := evalAddMonoidHom A j

noncomputable def singleAddMonoidHom (j : ι) : A j →+ Πʳ i, [A i, B i] where
  toFun x := ⟨Pi.single j x, sorry⟩
  map_zero' := sorry
  map_add' _ _ := sorry

variable [∀ i, TopologicalSpace (A i)]
def evalContinuousAddMonoidHom (j : ι) : Πʳ i, [A i, B i] →ₜ+ A j := {
  __ := evalAddMonoidHom A j
  continuous_toFun := continuous_eval j
}

noncomputable def singleContinuousAddMonoidHom (j : ι) : A j →ₜ+ Πʳ i, [A i, B i] where
  __ := singleAddMonoidHom A j
  continuous_toFun := by
    -- presumably true -- could assume B i is open if necessary
    sorry

end RestrictedProduct

namespace ContinuousLinearMap

open scoped TensorProduct

def rTensor {R : Type*} {M N : Type*} (V : Type*)
    [Semiring M] [Semiring N] [CommRing R] [Algebra R M] [Algebra R N]
    [TopologicalSpace M] [TopologicalSpace N] (φ : M →L[R] N)
    [AddCommGroup V] [Module R V] [Module.Finite R V] [Module.Free R V]
    [TopologicalSpace (M ⊗[R] V)] [IsModuleTopology M (M ⊗[R] V)]
    [TopologicalSpace (N ⊗[R] V)] [IsModuleTopology N (N ⊗[R] V)] :
    (M ⊗[R] V) →L[R] (N ⊗[R] V) := {
  __ := LinearMap.rTensor V φ.toLinearMap
  cont := sorry -- this is OK because if we pick a basis then topologically and
  -- algebraically it's φ^n : M^n -> N^n
  }

lemma rTensor_id_apply {R : Type*} {M : Type*} (V : Type*)
    [Semiring M] [CommRing R] [Algebra R M]
    [TopologicalSpace M]
    [AddCommGroup V] [Module R V] [Module.Finite R V] [Module.Free R V]
    [TopologicalSpace (M ⊗[R] V)] [IsModuleTopology M (M ⊗[R] V)] (x : M ⊗[R] V) :
    rTensor V (.id R M) x = x := by
  simp [rTensor]

lemma rTensor_id {R : Type*} {M : Type*} (V : Type*)
    [Semiring M] [CommRing R] [Algebra R M]
    [TopologicalSpace M]
    [AddCommGroup V] [Module R V] [Module.Finite R V] [Module.Free R V]
    [TopologicalSpace (M ⊗[R] V)] [IsModuleTopology M (M ⊗[R] V)] :
    rTensor V (.id R M) = .id R (M ⊗[R] V) := by
  ext x
  apply rTensor_id_apply

lemma rTensor_comp_apply {R : Type*} {M N P : Type*} (V : Type*)
    [Semiring M] [Semiring N] [Semiring P] [CommRing R] [Algebra R M] [Algebra R N] [Algebra R P]
    [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace P] (φ : M →L[R] N)
    (ψ : N →L[R] P) [AddCommGroup V] [Module R V] [Module.Finite R V] [Module.Free R V]
    [TopologicalSpace (M ⊗[R] V)] [IsModuleTopology M (M ⊗[R] V)]
    [TopologicalSpace (N ⊗[R] V)] [IsModuleTopology N (N ⊗[R] V)]
    [TopologicalSpace (P ⊗[R] V)] [IsModuleTopology P (P ⊗[R] V)]
    (x : M ⊗[R] V) :
    rTensor V (ψ.comp φ) x = rTensor V ψ (rTensor V φ x) := by
  simp [rTensor, LinearMap.rTensor, TensorProduct.map_map]

lemma rTensor_comp {R : Type*} {M N P : Type*} (V : Type*)
    [Semiring M] [Semiring N] [Semiring P] [CommRing R] [Algebra R M] [Algebra R N] [Algebra R P]
    [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace P] (φ : M →L[R] N)
    (ψ : N →L[R] P) [AddCommGroup V] [Module R V] [Module.Finite R V] [Module.Free R V]
    [TopologicalSpace (M ⊗[R] V)] [IsModuleTopology M (M ⊗[R] V)]
    [TopologicalSpace (N ⊗[R] V)] [IsModuleTopology N (N ⊗[R] V)]
    [TopologicalSpace (P ⊗[R] V)] [IsModuleTopology P (P ⊗[R] V)] :
    rTensor V (ψ.comp φ) = (rTensor V ψ).comp (rTensor V φ) := by
  ext
  apply rTensor_comp_apply

end ContinuousLinearMap

namespace IsDedekindDomain.FiniteAdeleRing

open scoped RestrictedProduct

variable (R : Type*) [CommRing R] [IsDedekindDomain R] [DecidableEq (HeightOneSpectrum R)]

variable (K : Type*) [Field K] [Algebra R K] [IsFractionRing R K]

def evalContinuousAlgebraMap (j : HeightOneSpectrum R) :
    FiniteAdeleRing R K →A[K] j.adicCompletion K := {
  __ := RestrictedProduct.evalContinuousAddMonoidHom _ j
  map_one' := sorry
  map_mul' := sorry
  commutes' := sorry
  cont := RestrictedProduct.continuous_eval j -- this should be automatic -- why is this
                                              -- field not called continuous_toFun??
    }

noncomputable def singleContinuousLinearMap (j : HeightOneSpectrum R) :
    j.adicCompletion K →L[K] FiniteAdeleRing R K := {
  __ := RestrictedProduct.singleContinuousAddMonoidHom _ j
  map_smul' := sorry
    }

lemma evalContinuousAlgebraMap_singleContinuousLinearMap (j : HeightOneSpectrum R)
    (xj : j.adicCompletion K) :
    (evalContinuousAlgebraMap R K j) (singleContinuousLinearMap R K j xj) = xj :=
  Pi.single_eq_same j xj

open TensorProduct

variable (V : Type*) [AddCommGroup V] [Module K V] [FiniteDimensional K V]

-- rabbithole instances
attribute [instance 900] UniformSpace.Completion.instSMul
    UniformSpace.Completion.instModule

-- shortcut instance
noncomputable instance (p : HeightOneSpectrum R) :
  Module (p.adicCompletion K) (p.adicCompletion K ⊗[K] V) := leftModule

variable
    [TopologicalSpace (FiniteAdeleRing R K ⊗[K] V)]
    [IsModuleTopology (FiniteAdeleRing R K) (FiniteAdeleRing R K ⊗[K] V)]
    [∀ (p : HeightOneSpectrum R), TopologicalSpace (p.adicCompletion K ⊗[K] V)]
    [∀ (p : HeightOneSpectrum R), IsModuleTopology (p.adicCompletion K) (p.adicCompletion K ⊗[K] V)]

-- all these are still slow but at least they don't time out

--variable (p : HeightOneSpectrum R) in
--#synth SMulCommClass K (p.adicCompletion K) (p.adicCompletion K)

--variable (p : HeightOneSpectrum R) in
--#synth Module (HeightOneSpectrum.adicCompletion K p) (HeightOneSpectrum.adicCompletion K p)

open IsDedekindDomain NumberField

noncomputable def TensorProduct.localcomponent (p : HeightOneSpectrum R)
    (φ : FiniteAdeleRing R K ⊗[K] V →L[FiniteAdeleRing R K]
      FiniteAdeleRing R K ⊗[K] V) :
    p.adicCompletion K ⊗[K] V →L[K] p.adicCompletion K ⊗[K] V := by
  let bar1 := (ContinuousLinearMap.rTensor V
    (evalContinuousAlgebraMap R K p).toContinuousLinearMap)
  let bar2 : FiniteAdeleRing R K ⊗[K] V →L[K] FiniteAdeleRing R K ⊗[K] V := {
    __ := φ.toLinearMap.restrictScalars K
  }
  let bar3 := (ContinuousLinearMap.rTensor V (singleContinuousLinearMap R K p))
  refine bar1.comp (bar2.comp bar3)

lemma TensorProduct.localcomponent_apply
    (φ : FiniteAdeleRing R K ⊗[K] V →L[FiniteAdeleRing R K] FiniteAdeleRing R K ⊗[K] V)
    (x : FiniteAdeleRing R K ⊗[K] V) (p : HeightOneSpectrum R) :
    (ContinuousLinearMap.rTensor V
      (evalContinuousAlgebraMap R K p).toContinuousLinearMap) (φ x) =
    TensorProduct.localcomponent R K V p φ ((ContinuousLinearMap.rTensor V
      (evalContinuousAlgebraMap R K p).toContinuousLinearMap) x) := by
  -- use rTensor_comp_apply, rTensor_id_apply, evalContinuousAlgebraMap_singleContinuousLinearMap
  -- I think
  sorry

end FiniteAdeleRing

end IsDedekindDomain

[Bryan Wang]

Is the idea to express addEquivAddHaarChar φ in terms of addEquivAddHaarChar (TensorProduct.localcomponent φ)?

[Kevin Buzzard]

That was my idea yes. We want to use the theorem that says that the haar character of a restricted product is the finprod of the haar characters and I haven't really had the time to think it out but I'm hoping that the code above will help us to show that multiplication by the adelic unit is the restricted product of multiplication by the local components

[Bryan Wang]

Two sorries (both to do with choosing bases) left:

import Mathlib

namespace RestrictedProduct

variable {ι : Type*} [DecidableEq ι] {R : Type*} [Semiring R] (A : ι → Type*) {𝓕 : Filter ι}
    {S : ι → Type*}
    [(i : ι) → SetLike (S i) (A i)] {B : (i : ι) → S i} (j : ι) [(i : ι) → AddCommMonoid (A i)]
    [(i : ι) → Module R (A i)] [∀ (i : ι), AddSubmonoidClass (S i) (A i)]

example (j : ι) : Πʳ i, [A i, B i] →+ A j := evalAddMonoidHom A j

noncomputable def singleAddMonoidHom (j : ι) : A j →+ Πʳ i, [A i, B i] where
  toFun x := ⟨Pi.single j x, by
    simpa using (Set.finite_singleton j).subset fun i _ ↦ by by_cases h : i = j <;> simp_all⟩
  map_zero' := by ext; simp
  map_add' _ _ := by ext; simp [Pi.single_add]

variable [∀ i, TopologicalSpace (A i)]
def evalContinuousAddMonoidHom (j : ι) : Πʳ i, [A i, B i] →ₜ+ A j := {
  __ := evalAddMonoidHom A j
  continuous_toFun := continuous_eval j
}

open Filter in
noncomputable def singleContinuousAddMonoidHom (j : ι) : A j →ₜ+ Πʳ i, [A i, B i] where
  __ := singleAddMonoidHom A j
  continuous_toFun := by
    let S : Set ι := {j}ᶜ
    let single' : A j → Πʳ i, [A i, B i]_[𝓟 S] :=
      fun x ↦ ⟨Pi.single j x,
        eventually_principal.mpr
        fun i hi ↦ by simp [Pi.single_eq_of_ne (Set.mem_compl_singleton_iff.mp hi)]⟩
    have : Continuous single' := by
      simpa [continuous_rng_of_principal] using continuous_single j
    apply (isEmbedding_inclusion_principal
      (le_principal_iff.mpr (Set.finite_singleton j).compl_mem_cofinite)).continuous.comp this

lemma singleContinuousAddMonoidHom_apply_same {j : ι} (x : A j) :
    (singleContinuousAddMonoidHom A j x : Πʳ i, [A i, B i]) j = x := by
  convert Pi.single_apply j x j; simp

lemma singleContinuousAddMonoidHom_apply_of_ne {j i : ι} (h : i ≠ j) (x : A j) :
    (singleContinuousAddMonoidHom A j x : Πʳ i, [A i, B i]) i = 0 := by
  simpa using Pi.single_eq_of_ne h x

end RestrictedProduct

namespace ContinuousLinearMap

open scoped TensorProduct

def rTensor {R : Type*} {M N : Type*} (V : Type*)
    [Semiring M] [Semiring N] [CommRing R] [Algebra R M] [Algebra R N]
    [TopologicalSpace M] [TopologicalSpace N] (φ : M →L[R] N)
    [AddCommGroup V] [Module R V] [Module.Finite R V] [Module.Free R V]
    [TopologicalSpace (M ⊗[R] V)] [IsModuleTopology M (M ⊗[R] V)]
    [TopologicalSpace (N ⊗[R] V)] [IsModuleTopology N (N ⊗[R] V)] :
    (M ⊗[R] V) →L[R] (N ⊗[R] V) := {
  __ := LinearMap.rTensor V φ.toLinearMap
  cont := sorry -- this is OK because if we pick a basis then topologically and
  -- algebraically it's φ^n : M^n -> N^n
  }

lemma rTensor_id_apply {R : Type*} {M : Type*} (V : Type*)
    [Semiring M] [CommRing R] [Algebra R M]
    [TopologicalSpace M]
    [AddCommGroup V] [Module R V] [Module.Finite R V] [Module.Free R V]
    [TopologicalSpace (M ⊗[R] V)] [IsModuleTopology M (M ⊗[R] V)] (x : M ⊗[R] V) :
    rTensor V (.id R M) x = x := by
  simp [rTensor]

lemma rTensor_id {R : Type*} {M : Type*} (V : Type*)
    [Semiring M] [CommRing R] [Algebra R M]
    [TopologicalSpace M]
    [AddCommGroup V] [Module R V] [Module.Finite R V] [Module.Free R V]
    [TopologicalSpace (M ⊗[R] V)] [IsModuleTopology M (M ⊗[R] V)] :
    rTensor V (.id R M) = .id R (M ⊗[R] V) := by
  ext x
  apply rTensor_id_apply

lemma rTensor_comp_apply {R : Type*} {M N P : Type*} (V : Type*)
    [Semiring M] [Semiring N] [Semiring P] [CommRing R] [Algebra R M] [Algebra R N] [Algebra R P]
    [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace P] (φ : M →L[R] N)
    (ψ : N →L[R] P) [AddCommGroup V] [Module R V] [Module.Finite R V] [Module.Free R V]
    [TopologicalSpace (M ⊗[R] V)] [IsModuleTopology M (M ⊗[R] V)]
    [TopologicalSpace (N ⊗[R] V)] [IsModuleTopology N (N ⊗[R] V)]
    [TopologicalSpace (P ⊗[R] V)] [IsModuleTopology P (P ⊗[R] V)]
    (x : M ⊗[R] V) :
    rTensor V (ψ.comp φ) x = rTensor V ψ (rTensor V φ x) := by
  simp [rTensor, LinearMap.rTensor, TensorProduct.map_map]

lemma rTensor_comp {R : Type*} {M N P : Type*} (V : Type*)
    [Semiring M] [Semiring N] [Semiring P] [CommRing R] [Algebra R M] [Algebra R N] [Algebra R P]
    [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace P] (φ : M →L[R] N)
    (ψ : N →L[R] P) [AddCommGroup V] [Module R V] [Module.Finite R V] [Module.Free R V]
    [TopologicalSpace (M ⊗[R] V)] [IsModuleTopology M (M ⊗[R] V)]
    [TopologicalSpace (N ⊗[R] V)] [IsModuleTopology N (N ⊗[R] V)]
    [TopologicalSpace (P ⊗[R] V)] [IsModuleTopology P (P ⊗[R] V)] :
    rTensor V (ψ.comp φ) = (rTensor V ψ).comp (rTensor V φ) := by
  ext
  apply rTensor_comp_apply

end ContinuousLinearMap

namespace IsDedekindDomain.FiniteAdeleRing

open scoped RestrictedProduct

variable (R : Type*) [CommRing R] [IsDedekindDomain R] [DecidableEq (HeightOneSpectrum R)]

variable (K : Type*) [Field K] [Algebra R K] [IsFractionRing R K]

def evalContinuousAlgebraMap (j : HeightOneSpectrum R) :
    FiniteAdeleRing R K →A[K] j.adicCompletion K := {
  __ := RestrictedProduct.evalContinuousAddMonoidHom _ j
  map_one' := rfl
  map_mul' _ _ := rfl
  commutes' _ := rfl
  cont := RestrictedProduct.continuous_eval j -- this should be automatic -- why is this
                                              -- field not called continuous_toFun??
    }

noncomputable def singleContinuousLinearMap (j : HeightOneSpectrum R) :
    j.adicCompletion K →L[K] FiniteAdeleRing R K := {
  __ := RestrictedProduct.singleContinuousAddMonoidHom _ j
  map_smul' k x := by
    open RestrictedProduct in
    ext i; by_cases! h : i = j <;> conv_lhs => change singleContinuousAddMonoidHom _ j (k • x) i
    · rw [h, singleContinuousAddMonoidHom_apply_same]
      simp [FiniteAdeleRing, Algebra.smul_def, singleContinuousAddMonoidHom_apply_same]
      left; rfl -- this can probably be avoided but it works for now..
    · rw [singleContinuousAddMonoidHom_apply_of_ne _ h _]
      simp [FiniteAdeleRing, Algebra.smul_def, singleContinuousAddMonoidHom_apply_of_ne _ h _]
    }

lemma evalContinuousAlgebraMap_singleContinuousLinearMap (j : HeightOneSpectrum R)
    (xj : j.adicCompletion K) :
    (evalContinuousAlgebraMap R K j) (singleContinuousLinearMap R K j xj) = xj :=
  Pi.single_eq_same j xj

open TensorProduct

variable (V : Type*) [AddCommGroup V] [Module K V] [FiniteDimensional K V]

-- rabbithole instances
attribute [instance 900] UniformSpace.Completion.instSMul
    UniformSpace.Completion.instModule

-- shortcut instance
noncomputable instance (p : HeightOneSpectrum R) :
  Module (p.adicCompletion K) (p.adicCompletion K ⊗[K] V) := leftModule

variable
    [TopologicalSpace (FiniteAdeleRing R K ⊗[K] V)]
    [IsModuleTopology (FiniteAdeleRing R K) (FiniteAdeleRing R K ⊗[K] V)]
    [∀ (p : HeightOneSpectrum R), TopologicalSpace (p.adicCompletion K ⊗[K] V)]
    [∀ (p : HeightOneSpectrum R), IsModuleTopology (p.adicCompletion K) (p.adicCompletion K ⊗[K] V)]

-- all these are still slow but at least they don't time out

--variable (p : HeightOneSpectrum R) in
--#synth SMulCommClass K (p.adicCompletion K) (p.adicCompletion K)

--variable (p : HeightOneSpectrum R) in
--#synth Module (HeightOneSpectrum.adicCompletion K p) (HeightOneSpectrum.adicCompletion K p)

open IsDedekindDomain NumberField

noncomputable def TensorProduct.localcomponent (p : HeightOneSpectrum R)
    (φ : FiniteAdeleRing R K ⊗[K] V →L[FiniteAdeleRing R K]
      FiniteAdeleRing R K ⊗[K] V) :
    p.adicCompletion K ⊗[K] V →L[K] p.adicCompletion K ⊗[K] V := by
  let bar1 := (ContinuousLinearMap.rTensor V
    (evalContinuousAlgebraMap R K p).toContinuousLinearMap)
  let bar2 : FiniteAdeleRing R K ⊗[K] V →L[K] FiniteAdeleRing R K ⊗[K] V := {
    __ := φ.toLinearMap.restrictScalars K
  }
  let bar3 := (ContinuousLinearMap.rTensor V (singleContinuousLinearMap R K p))
  refine bar1.comp (bar2.comp bar3)

lemma TensorProduct.localcomponent_apply
    (φ : FiniteAdeleRing R K ⊗[K] V →L[FiniteAdeleRing R K] FiniteAdeleRing R K ⊗[K] V)
    (x : FiniteAdeleRing R K ⊗[K] V) (p : HeightOneSpectrum R) :
    (ContinuousLinearMap.rTensor V
      (evalContinuousAlgebraMap R K p).toContinuousLinearMap) (φ x) =
    TensorProduct.localcomponent R K V p φ ((ContinuousLinearMap.rTensor V
      (evalContinuousAlgebraMap R K p).toContinuousLinearMap) x) := by
  -- the crux is to show that if `x` is in the kernel of `(ContinuousLinearMap.rTensor V (evalContinuousAlgebraMap R K p).toContinuousLinearMap)`,
  -- then so too is `φ x`.
  -- to do so I think one needs to use that `FiniteAdeleRing R K ⊗[K] V` is finite free `FiniteAdeleRing R K`-module
  -- and the `FiniteAdeleRing R K`-linearity of `φ`
  simp [localcomponent, ← ContinuousLinearMap.rTensor_comp_apply]
  sorry

end FiniteAdeleRing

end IsDedekindDomain

[Bryan Wang]

In FLT#823 I perform the reduction from adeles to finite x infinite.

[Bryan Wang]

FLT#823 is now sorry-free and builds, so we are reduced to just the finite adeles.

[Bryan Wang]

Unfortunately I won't have as much time to work on the finite adele case over the next few days (because of a conference), but I can work on it intermittently and/or try to fill any sorries that may arise in the process.

[Kevin Buzzard]

This is great thanks, I think I have a plan for the finite Adele case and have time over the next few days to work on it

[Kevin Buzzard]

(heads-up: that code above is now sorry-free and I'm figuring out whether it will solve our problems)

[Bryan Wang]

I should have some time over the weekend and the next few days to work on this again, let me know if there's anything I can help with!

[Kevin Buzzard]

You can see where I've got to in the PR I have. I've reduced the question to a statement about equality of haar characters of two endomorphisms of an actual restricted product but right now these endomorphisms are not yet expressed as products of local endomorphisms. I left a few trivial sorries. When I'm at a computer I can try and break down what's left into more than one chunk. The key next step is the claim that these functions I've created from A^n to A^n are products of local components and for this I'll use my previous merged PR but unfortunately I've got no public explanation of all this and I won't be at a computer for several hours.