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

*) 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 . Currently unclaimed.

*) 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.

*) The sorry in MeasureTheory.addHaarScalarFactor_tensor_adeles_eq_oneon line 125 of FLT/HaarMeasure/HaarChar/AdeleRing.lean is Theorem 9.38 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: unclaimed

*) 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.

In progress

*) 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: 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!

*) There are three sorries in FLT/NumberField/Padics/RestrictedProduct.lean which have been PRed directly to mathlib by @Salvatore Mercuri ; there is also padicEquiv_norm_eq in FLT/HaarMeasure/HaarChar/AdeleRing.lean in there; so please review #30576 ! (many people do not realise that anyone is welcome to review mathlib PRs).

Done

*) 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.