Outstanding tasks, V9

Stream: FLT

[Kevin Buzzard]

For "bottom-up FLT" my plan is to get the theorem TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.finiteDimensional in FLT/AutomorphicForm/QuaternionAlgebra/FiniteDimensional.lean sorry-free, write it up as a joint paper with everyone who made nontrivial contributions as a coauthor, and then park it and work on top-down for a while (starting in Jan). By "bottom-up FLT" I mean the adele, Haar character, Fujisaki lemma and Quaternion algebra miniprojects, all of which are nearing completion.

I've merged several of the relevant PRs over the last few days and now have a much clearer idea about what needs doing to get this over the line. Here they are. I'll use this thread to add people who want to claim tasks.
Edit: sorted into "done" and "in progress" and "unclaimed".

Unclaimed

[empty set!]

In progress

*) The sorry in MeasureTheory.addHaarScalarFactor_tensor_adeles_eq_oneon line 125 of FLT/HaarMeasure/HaarChar/AdeleRing.lean is Theorem 9.39 and has the following proof: the Haar character of phi equals the Haar character of det(phi) where phi is considered to be $\mathbb{Q}$-linear, and now this follows from earlier results. The details are actually quite long. Status: done in FLT#822 .

*) The claim NumberField.AdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul in FLT/HaarMeasure/HaarChar/AdeleRing.lean that left and right multiplication have the same Haar character on line 42 is Theorem 9.36 of the blueprint and follows from Theorem 9.31 and/or Corollary 9.33 (writing the global endomorphism as as product of local ones) and then Corollary 9.21. Status: claimed by Bryan Wang.

*) In FLT/Mathlib/LinearAlgebra/Determinant.lean there is [Algebra.IsCentral k B] [IsSimpleRing A] [IsSimpleRing B] : IsSimpleRing (A ⊗[k] B) which @Edison Xie has proved. Status: this is #26377 -- please review!

Done

*) There is padicEquiv_norm_eq in FLT/HaarMeasure/HaarChar/AdeleRing.lean stating that the isomorphism from $\mathbb{Q}$ completed at a height one prime to $\mathbb{Q}_p$ is an isometry. Status: Salvatore did this in FLT#816 .

*) In FLT/HaarMeasure/HaarChar/AddEquiv.lean there's the claim mulEquivHaarChar_restrictedProductCongrRight (and an associated additive claim) that if $\phi_i:G_i\to G_i$ are topological and algebraic isomorphisms of topological groups such that $\phi_i(C_i)=C_i$ for some collection $C_i\subseteq G_i$ of compact open subgroups, then the mulEquivHaarChar of the restricted product of the $\phi_i$ is equal to the product of the mulEquivHaarChars of the $\phi_i$. The proof is in the blueprint, it's theorem 9.31; the associated issue is FLT#552 and there is some preliminary work at FLT#562 . Status: FLT#562 is updated and merged!

*) MeasureTheory.ringHaarChar_adeles_units_rat_eq_one on line 61 of FLT/HaarMeasure/HaarChar/AdeleRing.lean should follow from the product formula for $\mathbb{Q}$. Status: done by Bryan.

*) There are three sorries in FLT/NumberField/Padics/RestrictedProduct.lean which have been PRed directly to mathlib by @Salvatore Mercuri ; these are resolved in FLT#810 .

*) The sorry inPadicInt.volume_coe in FLT/HaarMeasure/MeasurableSpacePadics.lean says that the measures PadicInt.instMeasureSpace on $\mathbb{Z}_p$ and Padic.instMeasureSpace on $\mathbb{Q}_p$ (both defined in the same file) are compatible. The maths proof is: both measures are defined to be Haar measure normalised such that $\Z_p$ has measure 1; the pullback of Haar measure under an open immersion is a Haar measure and they agree on $\Z_p$ so they agree everywhere. Status: done by Bryan Wang.

*) NumberField.AdeleRing.DivisionAlgebra.Aux.existsE in FLT/DivisionAlgebra/Finiteness.lean -- this boils down to some measure theory and cocompactness of $D$ in $D_{\mathbb{A}}$. Status: done in FLT#803 .

*) NumberField.FiniteAdeleRing.DivisionAlgebra.units_cocompact in FLT/DivisionAlgebra/Finiteness.lean -- done by @William Coram in FLT#796 .

*) The sorry in NumberField.AdeleRing.units_mem_ringHaarCharacter_ker in FLT/HaarMeasure/HaarChar/AdeleRing.lean should follow from the one on line 146. Status: DONE in FLT#790

*) the sorry in NumberField.AdeleRing.addEquivAddHaarChar_mulRight_unit_eq_one in FLT/HaarMeasure/HaarChar/AdeleRing.lean follows from the fact that right multiplication and left multiplication have the same Haar character (proved above). Status: solved in this commit.

*) NumberField.AdeleRing.DivisionAlgebra.Aux.E_noninjective_right in FLT/DivisionAlgebra/Finiteness.lean -- DONE

*) A module topology statement which will follow from typeclass inference when I get back to #29315 -- DONE

*) The sorries on lines 88 and 89 of FLT/HaarMeasure/HaarChar/AdeleRing.lean could be filled by observing that the map is $\mathbb{A}_K$-linear and that the $\mathbb{A}_L$-module topology is the $\mathbb{A}_K$-module topology, because $\mathbb{A}_L$ is a finite $\mathbb{A}_K$-module. DONE

*) line 110 of FLT/HaarMeasure/HaarChar/AdeleRing.lean is just an obscure way of saying that Q_p is locally compact. DONE by @Salvatore Mercuri in FLT#773.

*) This is the claim MeasureTheory.ringHaarChar_adeles_rat in FLT/HaarMeasure/HaarChar/AdeleRing.lean that multiplication by an element of $\mathbb{Q}^\times$ has haar character 1 on the adeles of $\mathbb{Q}$. The proof is: use the result from (2) and the product formula for the rationals. These are the sorries on line 120 and 124. Status: DONE by @Bryan Wang in FLT#774.

*) The sorries in ContinuousLinearEquiv.baseChange in FLT/HaarMeasure/HaarChar/AdeleRing.lean look trivial to me -- they're both "linear => continuous" for the module topology. Done by Ruben Van de Velde.

---

And that's it! Basically this is the culmination of all of the miniprojects which we have spent the first year of the project working hard on.

[Ruben Van de Velde]

5e is indeed trivial, will pr in a bit

[William Coram]

4) There are a few sorries in FLT/DivisionAlgebra/Finiteness.lean which William Coram has been working on. William -- which ones of these are you claiming and which ones are you going to offer up to others?

I have a WIP PR for NumberField.FiniteAdeleRing.DivisionAlgebra.units_cocompact so that is claimed by me.

But I would be happy if anyone wants to claim and attempt existsE and E_noninjective_right (the two remaining sorries at the start of the file). If no one fancies the challenge I can try and work on it again though.

[Salvatore Mercuri]

Kevin Buzzard said:

5c) line 110 is just an obscure way of saying that Q_p is locally compact. Salvatore Mercuri does your recent work make this easy?

Yep this follows immediately from the pending mathlib PR because we have LocallyCompactSpace ℚ_[p] . I'll sort a PR out.

We could also prove it directly for general number fields K since we also have v.adicCompletionIntegers K is compact.

[Kevin Buzzard]

My impression is that the result we need is this. If $D$ is a ring finite-dimensional over $\mathbb{Q}$ (example: $M_2(K)$ for $K$ a number field) then we know $D\otimes_{\mathbb{Q}}\mathbb{A}_{\mathbb{Q}}$ is a locally compact additive group, and we can look at left multiplication by an element $d$ of $D^\times$ and ask how it scales the Haar measure. The claim is that it scales it by a factor of 1, and the proof is that by general nonsense it scales it by the same number as multiplication by $q$ scales $\mathbb{A}_{\mathbb{Q}}$ where $q$ is the determinant of the $\mathbb{Q}$-linear map given by left multiplication by $d$ on $D$. This reduces everything to the product formula over $\mathbb{Q}$. So we might not need the case of general $K$ for this application, although of course there's no harm in proving it.

[Bryan Wang]

5d) This is the claim that multiplication by an element of $\mathbb{Q}^\times$ has haar character 1 on the adeles of $\mathbb{Q}$. The proof is: use the result from (2) and the product formula for the rationals. These are the sorries on line 120 and 124.

The sorry on line 120 is resolved in FLT#774, and I'll claim the sorry on line 124 as well.

[Kevin Buzzard]

By the way, there might be money available to work on the FLT project for someone who knows something about (or feels they're capable of learning about) the more advanced material in the proof, if anyone is looking for a job (right now) and is happy to move to London -- let me know. Don't particularly want to announce this in job postings as am slightly concerned will get bombarded by people who are not qualified.

[metakuntyyy]

Such a bummer that the UK is no longer in the EU...

[Kevin Buzzard]

Don't get me started (but this is off topic).

[Kevin Buzzard]

I've merged a few things today and updated the top post. We have a new (unclaimed) challenge:

padicUniformEquiv (v : HeightOneSpectrum (𝓞 ℚ)) :
    v.adicCompletion ℚ ≃ᵤ ℚ_[v.natGenerator] := sorry

left by @Salvatore Mercuri as a byproduct of FLT#773 . Things are ticking along nicely. Today I did a refactor of certain MeasurableSpace instances.

[Kevin Buzzard]

I'm working on this stuff full-time now and am cautiously optimistic of getting it over the line by Christmas.

[Salvatore Mercuri]

Kevin Buzzard said:

I've merged a few things today and updated the top post. We have a new (unclaimed) challenge:

padicUniformEquiv (v : HeightOneSpectrum (𝓞 ℚ)) :
    v.adicCompletion ℚ ≃ᵤ ℚ_[v.natGenerator] := sorry

left by Salvatore Mercuri as a byproduct of FLT#773 .

This one is also in the mathlib PR #30576 which is nearing merge now I think!

[Kevin Buzzard]

OK I updated!

[Kevin Buzzard]

I've unclaimed two of the things I'd claimed and which I'd hoped to knock off -- I have been distracted by this measure-theoretic challenge of writing down arbitrarily large compact subsets of $D\otimes_K\mathbb{A}_K$, which I might be making a meal of in FLT#803 , so I'm going to focus on that and get it over the line; I feel like we're close.

[Bryan Wang]

*) The claim NumberField.AdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul in FLT/HaarMeasure/HaarChar/AdeleRing.lean that left and right multiplication have the same Haar character on line 42 is Theorem 9.35 of the blueprint and follows from Theorem 9.31 and/or Corollary 9.32 (writing the global endomorphism as as product of local ones) and then Corollary 9.21. Status: unclaimed (was claimed by me but I'm focussing on FLT#803 for now)

I'd like to give Theorem 9.35 a go

[Kevin Buzzard]

I've merged FLT#796 -- the proof of the main compactness theorem, completed by William Coram (with some tidy-up by me) today.

Ooh, I forgot to update the blueprint; I'll do that now.

[Bryan Wang]

*) MeasureTheory.ringHaarChar_adeles_units_rat_eq_one on line 61 of FLT/HaarMeasure/HaarChar/AdeleRing.lean should follow from the product formula for $\mathbb{Q}$. Currently unclaimed.

I had some progress on ringHaarChar_adeles_units_rat_eq_one (now in draft PR FLT#805), where I reduced the statement to two statements which are mathematically equivalent to ringHaarChar_real and ringHaarChar_padic respectively.

However because of the way 𝔸 ℚ is set up we now have ringHaarChar applied to Rat.infinitePlace.Completion and p.adicCompletion ℚ instead of the ℝ and ℚ_[p] of ringHaarChar_real and ringHaarChar_padic respectively. It seems I'm back to the question of whether there's any easy way to relate these? (so as to apply e.g. addEquivAddHaarChar_eq_addEquivAddHaarChar_of_continuousAddEquiv)

[Kevin Buzzard]

For infinite places I was looking at all of this yesterday in far more generality; Rat.infinitePlace.Completion is both algebraically and isometrically isomorphic to $\R$ and all this is in mathlib.

[Kevin Buzzard]

See FLT/Mathlib/NumberTheory/NumberField/InfiniteAdeleRing.lean (note that it was changed 13 hours ago). You need things like Completion.isometryEquivRealOfIsReal and Completion.ringEquivRealOfIsReal.

[Kevin Buzzard]

import Mathlib

open NumberField InfinitePlace

lemma Rat.infinitePlace_isReal (v : InfinitePlace ℚ) : v.IsReal :=
  Subsingleton.elim v infinitePlace ▸ isReal_infinitePlace

variable (v : NumberField.InfinitePlace ℚ)

noncomputable example : v.Completion ≃ₜ+ ℝ :=
{
  __ := Completion.isometryEquivRealOfIsReal (Rat.infinitePlace_isReal v)
  __ := Completion.ringEquivRealOfIsReal (Rat.infinitePlace_isReal v)
  continuous_toFun := by
    show Continuous (Completion.isometryEquivRealOfIsReal (Rat.infinitePlace_isReal v))
    fun_prop
  continuous_invFun := by
    show Continuous (Completion.isometryEquivRealOfIsReal (Rat.infinitePlace_isReal v)).symm
    fun_prop
}

[Kevin Buzzard]

(this works for an arbitrary infinite place of $\mathbb{Q}$, not just our preferred one (they're all equal but they're not all defeq))

[Salvatore Mercuri]

Bryan Wang said:

However because of the way 𝔸 ℚ is set up we now have ringHaarChar applied to Rat.infinitePlace.Completion and p.adicCompletion ℚ instead of the ℝ and ℚ_[p] of ringHaarChar_real and ringHaarChar_padic respectively. It seems I'm back to the question of whether there's any easy way to relate these? (so as to apply e.g. addEquivAddHaarChar_eq_addEquivAddHaarChar_of_continuousAddEquiv)

For finite places, the continuous alg equiv v.adicCompletion ℚ ≃A[ℚ] ℚ_[v.natGenerator] should be in mathlib soon. So you could change the subscript a to capital A in IsDedekindDomain.HeightOneSpectrum.padicEquiv and move/import it as needed!

[Salvatore Mercuri]

Kevin Buzzard said:

import Mathlib

open NumberField InfinitePlace

lemma Rat.infinitePlace_isReal (v : InfinitePlace ℚ) : v.IsReal :=
  Subsingleton.elim v infinitePlace ▸ isReal_infinitePlace

variable (v : NumberField.InfinitePlace ℚ)

noncomputable example : v.Completion ≃ₜ+ ℝ :=
{
  __ := (Completion.isometryEquivRealOfIsReal (Rat.infinitePlace_isReal v)).toHomeomorph
  __ := Completion.ringEquivRealOfIsReal (Rat.infinitePlace_isReal v)
}

This also works to avoid having to directly prove continuity

[Bryan Wang]

Thank you very much! The real place is now done in FLT#805, and hopefully soon also the finite place (especially with #30576).

[Kevin Buzzard]

FLT#803 is compiling: this PR completes Chapter 10 of the blueprint! I'm going to tidy up the code and then merge. Recall the goal is all of chapters 8 to 11. At last count there were three unclaimed tasks and three in progress tasks. I'm busy for the next couple of days with family things but will probably be back on Sunday.

[Bryan Wang]

*) MeasureTheory.ringHaarChar_adeles_units_rat_eq_one on line 61 of FLT/HaarMeasure/HaarChar/AdeleRing.lean should follow from the product formula for $\mathbb{Q}$. Currently unclaimed.

This task is now done in FLT#805 (modulo some results in #30576)

[Kevin Buzzard]

Ooh! Bryan's work added an import and with it a new sorry! I'll add it to the unclaimed list at the top. It is PadicInt.volume_coe in FLT/HaarMeasure/MeasurableSpacePadics.lean and it says that the measures PadicInt.instMeasureSpace on $\mathbb{Z}_p$ and Padic.instMeasureSpace on $\mathbb{Q}_p$ (both defined in the same file) are compatible.

[Kevin Buzzard]

The maths proof is: both measures are defined to be Haar measure normalised such that $\Z_p$ has measure 1; the pullback of Haar measure under an open immersion is a Haar measure and they agree on $\Z_p$ so they agree everywhere.

[Salvatore Mercuri]

#30576 is in!

[Kevin Buzzard]

Yeah I already started the bump :-) (but I am not sure if I can finish it today and I'm busy all day tomorrow, for reasons that Salvatore can work out if he remembers, so it might not hit until Sunday). I can push how far I got...

[Kevin Buzzard]

FLT#808 , a small chance I'll get to it later today, otherwise it will be Sunday afternoon.

[Aayush Rajasekaran]

I'm happy to get FLT#808 over the finish line now, looks like it should be fairly straightforward.

[Ruben Van de Velde]

I'm looking at it, fwiw

[Aayush Rajasekaran]

@Ruben Van de Velde Sorry, didn't see your message! #809 should be all that's needed, but I might be missing things.

[Aayush Rajasekaran]

This change is the only one I wasn't too sure about.

[Kevin Buzzard]

I pushed what I think is a better change (I removed the instance prio hack above the result and added some shortcut instances which perhaps should be in mathlib itself). Everything else is great -- thanks a lot for your help! I'm awaiting CI and then we can merge.

Edit: merged; I'm now filling in some FLT sorries.

[Kevin Buzzard]

OK FLT#810 removes the three remaining sorries in FLT/NumberField/Padics/RestrictedProduct.lean now we have them upstream. There is also padicEquiv_norm_eq in FLT/HaarMeasure/HaarChar/AdeleRing.lean and this needs more than the topological construction in #30576 -- it needs an isometry. So I've not been able to immediately close it. @Salvatore Mercuri or @Bryan Wang do you see how to prove padicEquiv_norm_eq given what we now have in FLT? Shall I merge FLT#810 ?

[Bryan Wang]

*) The sorry inPadicInt.volume_coe in FLT/HaarMeasure/MeasurableSpacePadics.lean says that the measures PadicInt.instMeasureSpace  on $\mathbb{Z}_p$ and Padic.instMeasureSpace on $\mathbb{Q}_p$ (both defined in the same file) are compatible. The maths proof is: both measures are defined to be Haar measure normalised such that $\Z_p$ has measure 1; the pullback of Haar measure under an open immersion is a Haar measure and they agree on $\Z_p$ so they agree everywhere.

This sorry is filled in FLT#811!

[Kevin Buzzard]

I've also merged 810. I should hopefully have some time today and when I do I'll choose a random unclaimed thing and start on it. Edit: I claimed the Haar character on restricted product sorry.

[Salvatore Mercuri]

For padicEquiv_norm_eq, we'll have to show that the underlying valuations on the two sides are equal (I think by direct calculation). At the moment we only have that they are equivalent. I can give this a go!

[Kevin Buzzard]

The valuations take values in Zm0 so hopefully it's just a case of showing that p has valuation 1 on both sides?

[Kevin Buzzard]

I've resurrected FLT#562 and it's now sorry-free. I've also claimed the last unclaimed task so now everything is claimed! Will finite-dimensionality of quaternionic modular forms be sorry-free by the end of 2025?

[Kevin Buzzard]

buzzard@brutus:~/FLT$ lake build FLT/AutomorphicForm/QuaternionAlgebra/FiniteDimensional.lean
warning: manifest out of date: git revision of dependency 'mathlib' changed; use `lake update mathlib` to update it
⚠ [3322/3340] Built FLT.Mathlib.LinearAlgebra.Determinant
warning: FLT/Mathlib/LinearAlgebra/Determinant.lean:49:0: declaration uses 'sorry'
⚠ [3338/3340] Built FLT.HaarMeasure.HaarChar.AdeleRing
warning: FLT/HaarMeasure/HaarChar/AdeleRing.lean:41:6: declaration uses 'sorry'
warning: FLT/HaarMeasure/HaarChar/AdeleRing.lean:65:6: declaration uses 'sorry'
warning: FLT/HaarMeasure/HaarChar/AdeleRing.lean:122:6: declaration uses 'sorry'
Build completed successfully (3340 jobs).
buzzard@brutus:~/FLT$

The first sorry is #26377 a PR by @Edison Xie (tensor product of simple algebras is simple), the second I believe @Bryan Wang is thinking about (haar character of left and right multiplication by a unit are the same in the central simple case), the third I believe @Salvatore Mercuri is thinking about (padicEquiv is an isometry) and I'll take on the last one (which looks pretty gnarly but maybe there's a better proof?).

[Thomas Browning]

Kevin Buzzard said:

Status: this is #26377 -- please review!

It looks like #26377 is blocked by #26368 which has been awaiting-author since August

[Kevin Buzzard]

Yeah Edison has been focussing on class field theory since around that time. @Edison Xie are you out there? Neither of those PRs mentioned above are on the queue right now and this is fast becoming the only thing stopping us from announcing the culmination of a year's work. Do you have the time to get them back on the queue?

[Kevin Buzzard]

Even if you can just get the result compiling with today's mathlib this would be enough, because then I can just make FLT depend on your branch and we'll be able to claim victory. I can't go back to a previous mathlib commit though (I know it used to compile) because this would break FLT in lots of places.

[Edison Xie]

Thomas Browning said:

Kevin Buzzard said:

Status: this is #26377 -- please review!

It looks like #26377 is blocked by #26368 which has been awaiting-author since August

someone (@Kenny Lau ) has suggested I should use a different method (which shouldn't involve #26368) and I've discussed with him about this last week (and he left me with a false sorry) so I'm still thinking about this one, but at least I have a working proof under current mathlib :-)

[Edison Xie]

sorry for keeping everyone waiting I'll soon sort things out

[Kevin Buzzard]

It's ok there are three other series and there's a serious risk that I'll get swallowed up by Christmas things before I finish mine...

[Bryan Wang]

Perhaps somewhat related to #26377, do we already have something along the lines of

open scoped TensorProduct.RightActions in
instance (k A B : Type*) [Field k] [CommSemiring A] [Ring B]
    [Algebra k A] [Algebra k B]
    [Algebra.IsCentral k B] [IsSimpleRing B] :
    Algebra.IsCentral A (B ⊗[k] A) := sorry

it seems to be needed for Theorem 9.35.

[Edison Xie]

we have the field version of this (i.e when A is a field)

[Edison Xie]

I might have it when A is CommRing I'm not sure

[Bryan Wang]

Edison Xie said:

we have the field version of this (i.e when A is a field)

great, that's all we need!

[Edison Xie]

@Kevin Buzzard #26377 now passes CI, I'm trying to get it independent from #26368 but meanwhile we have a working version!

[Kevin Buzzard]

OK FLT#822 should be compiling right now, which removes one of the final three sorrys. @Bryan Wang are you still interested in working on lemma NumberField.AdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul? I can take it on if you want.

@Edison Xie it appears that #26377 depends on #26368 which has merge conflicts; as a result neither of these PRs are on the queue so they're not getting reviews and are just rotting more. Are you able to fix up #26368 ?

These (the mathlib PRs and the left_mul_eq_right_mul result) are the only two things which are left for the finite-dimensionality claim, once FLT#822 is merged, and once we have that claim then I think we can write a paper.

[Bryan Wang]

Kevin Buzzard said:

Bryan Wang are you still interested in working on lemma NumberField.AdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul? I can take it on if you want.

Yes, I can still work on isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul! I made a brief start last week but then became 'busy with the holidays' :laughing:, apologies about that. But I will have much more time in the coming days.

In fact this theorem suffers from the same problem you outlined in the other thread, namely that one has to manipulate $V \otimes_{\mathbb{Q}} \mathbb{A}$, but I guess I hadn't ploughed through enough yet last week to realise how difficult it was going to be :rolling_on_the_floor_laughing:. Hopefully with your new approach in FLT#822 I can also give a new proof of this theorem in the same spirit (edit: actually maybe not, since the automorphism in this theorem is not the base change of one over the ground field), and if so then I should have progress by this weekend or so.

[Edison Xie]

Kevin Buzzard said:

Edison Xie it appears that #26377 depends on #26368 which has merge conflicts; as a result neither of these PRs are on the queue so they're not getting reviews and are just rotting more. Are you able to fix up #26368 ?

will do shortly!

[Kevin Buzzard]

@Edison Xie another alternative is that you just extract the work and PR it to FLT

[Kevin Buzzard]

I'll be far less fussy about merging it

[Kevin Buzzard]

Bryan Wang said:

Kevin Buzzard said:

Bryan Wang are you still interested in working on lemma NumberField.AdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul? I can take it on if you want.

In fact this theorem suffers from the same problem you outlined in the other thread, namely that one has to manipulate $V \otimes_{\mathbb{Q}} \mathbb{A}$, but I guess I hadn't ploughed through enough yet last week to realise how difficult it was going to be :rolling_on_the_floor_laughing:.

Oh yikes you're right! It might be worth thinking about the mathematics of this before ploughing ahead. I don't think you can use the hack I used (going via a completely different route) because I don't see any reason right now that once you've picked a basis l_u is a finite product of elementary and diagonal matrices (although it might be true). One thing I can't immediately see how to avoid is this issue of moving from $B\otimes_{K}\mathbb{A}_K$ to $\prod'_v B\otimes_KK_v$, noting that this isomorphism needs to be both algebraic and a homeomorphism. I don't know how much of this is already in FLT (I find myself completely unable to keep track of what is already done because I forgot what I merged 6 months ago).

I am wondering whether we should take a step back here and try and prove some more basic claims but I will need to think about exactly what it is we should be doing here and I am one day into 4 days of family commitments so don't really have time to think.

[Kevin Buzzard]

We have several theorems of the form "doing X to the factors and then taking the restricted product is the same (both algebraically and topologically) as doing X to the restricted product" (for example "taking units") but "tensoring over K with B" is difficult to put into this paradigm because it's difficult to explain what you mean by tensoring a local pair $(K_v,\mathcal{O}_v)$ with $B$ over $K$ because $R_v$ is not a $K$-module.

[Kevin Buzzard]

Looking at the proof of Fujisaki I don't really see a way around this lemma either. It's certainly true but perhaps it will take longer to prove than I had appreciated.

[Kevin Buzzard]

Somehow the subtlety is the following. We know that $\mathbb{A}_\mathbb{Q}^f$ (the finite adeles of $\mathbb{Q}$) is $\prod'_p[\mathbb{Q}_p,\Z_p]$, the restricted product of $\mathbb{Q}_p$ with respect to the compact open subgroups $\Z_p$. This ring is a $\mathbb{Q}$-algebra. Now say $V$ is a $\mathbb{Q}$-module. "Obviously" $V\otimes_{\mathbb{Q}}\mathbb{A}_{\mathbb{Q}}^f$ is also a restricted product -- but of what? The local factors are $V\otimes_{\mathbb{Q}}\mathbb{Q}_p$ but what are the subgroups? They cannot be specified using $V$ alone; one needs to choose a lattice in $V$ and tensor over $\Z$ instead of $\mathbb{Q}$, and then observe that the answer is independent of the choice of lattice because any two lattices are equal away from a finite set of places.

[Bryan Wang]

Kevin Buzzard said:

Looking at the proof of Fujisaki I don't really see a way around this lemma either.

Yeah, I tried for a while to see if we could do without this lemma, or at least get away with a weaker form of it (I believe it is only used once), but that didn't seem too promising

[Kevin Buzzard]

It would not surprise me if we could reduce to the case where $B$ is a matrix algebra by some finite base change argument (tensor up to $L$ and you're raising factors to some $[L:K]$ power, but $\R_{>0}$ has unique $$n$$th roots for all $n\geq1$). So here is a concrete question: if $u\in GL_n(\mathbb{A}_K)$ or even $GL_n(R)$ for any locally compact second-countable Hausdorff topological commutative ring $R$, do left and multiplication by $u$ on $M_n(R)$ have the same Haar character? Equivalently, does conjugation by $u$ on $M_n(R)$ have Haar character 1? (it's an additive automorphism of an additive locally compact group). It's probably not hard to reduce to the case where $R$ is the finite adeles (I think we have all the preliminaries to reduce to this case in FLT already) so we can reduce to the case where $R$ has a compact open subring. I'm desperately trying to refrain from saying the word "restricted product" here but avoiding doing so might force us to have to answer the mathoverflow question https://mathoverflow.net/questions/506537/how-does-an-automorphism-of-a-free-module-scale-haar-measure .

[Kevin Buzzard]

You don't happen to know what the first $K$-group of an adele ring is, do you? :-)

[Edison Xie]

Kevin Buzzard said:

Edison Xie another alternative is that you just extract the work and PR it to FLT

I could do both but I want it in mathlib eventually so might as well do that now :-)

[Edison Xie]

ok I'm happy to announce that #26377 is now independent from any other PRs!

[Edison Xie]

it now passes CI, could I get some review pls?