Outstanding Tasks, V3

Stream: FLT

[Kevin Buzzard]

See here for V2.

Outstanding Tasks, V3.

Overview of where we're going

OK so the FLT project seems to have found its first goal: to state the modularity lifting theorem we're going to prove. Mario argues that this could be done in one week flat if we just got on with it, but some things will need thought and organisation, and I don't have time for that right now because I'm in marking hell (remember the grant hasn't started yet!).

But something which is turning out to be much easier to run is the construction of an example of a Galois representation and an automorphic form which match up in accordance with the Langlands Philosophy. This is a great sub-goal because working out the example will inform what kinds of API for the things we're making.

The V3 tasks:

1) We need the Hurwitz quaternions, the lattice $\Z\oplus\Z i\oplus\Z j\oplus\Z \frac{1+i+j+k}{2}$. This could be made as a standalone structure like docs#QuaternionAlgebra , in which case you need to make all the API for the ring structure. Alternatively you can make it as a subring of the usual quaternions, and here I'd recommend defining it as the ring closure of {1,i,j,omega} (which I think is defined to be the mul closure of the add group closure) and then proving it's the add group closure.

If we go down the structure route (and possibly any route) then my guess is that the $\Z$-basis $\{1,\omega,i,\omega i\}$ will be nicest to work with I think, and $i\omega=\overline{\omega i}$.

Whichever route we go down, we also need the definitions of trace and norm. For bonus points you can prove $x^2-t(x)x+N(x)=0$ because we'll probably need it at some point.

2) However they're made, we need to be good enough at arithmetic to push this argument through: if $a,b$ are Hurwitz quaternions and $b\not=0$ then we can write $a=qb+r$ with $N(r)<N(b)$, and we can also write $a=bq'+r'$ with $N(r')<N(b).$ Maths proof: do the division in the usual quaternions and let q be the nearest Hurwitz integer to the answer; there is always one whose distance less than one away.

3) Using this, prove that all left and right orders of the Hurwitz quaternions are principal. Proof: choose an element of smallest norm and use 2.

4) (the big one): Prove that if $R$ is the Hurwitz quaternions and $D=R\otimes\mathbb{Q}$ then $\widehat{D}^\times=D^\times \widehat{R}^\times.$ Proof forthcoming in LaTeX.

[Kevin Buzzard]

(deleted)

[Ruben Van de Velde]

I tried to work out the multiplication in FLT#74

[Ruben Van de Velde]

Ruben Van de Velde said:

I tried to work out the multiplication in FLT#74

I tried to convince myself that I got the details right in FLT#75

[Mitchell Lee]

Hello, can I finish the proof that matrix rings are central simple algebras?

[Ruben Van de Velde]

That would be great!

[Mitchell Lee]

https://github.com/ImperialCollegeLondon/FLT/pull/77

[Milton Lin]

Hi all, I'm new to this Lean and am interested to contributing to section 7.2,
https://imperialcollegelondon.github.io/FLT/blueprint/ch_bestiary.html#a0000000036
I wonder if this is possible?

[Ruben Van de Velde]

Correct me if I'm wrong, but I think there's no lean code at all for that chapter yet. If you're new, it might be best to try to fill in a proof for a theorem whose statement is already formalized and where you've got an English proof to follow

[Milton Lin]

Hi Ruben, thanks ! Ok, I suppose 6.1
is a good place to start?

[Chris Birkbeck]

I agree, starting with the open tasks is probably a good idea if you are new to lean. the stuff in chapter 7 is probably still a ways off.

[Josha Dekker]

Doesn’t 6.1 already have a leanok?

[Milton Lin]

Sorry, I meant 6.2*

[Ruben Van de Velde]

6.2 has an open pull request

[Ruben Van de Velde]

FLT#77

[Milton Lin]

Ah sorry, so is the procedure to contribute here :

1. search for a statement that is not yet formalized
2. check the pull requests
3. ask in this chat?
   Just to clarify , as I don't see this documented

[Johan Commelin]

These threads also contain lists of tasks that are ready + people reacting that they "claim" one of those tasks.

[Johan Commelin]

So keeping an eye on these zulip threads is likely helpful

[Milton Lin]

Nice, as of now I dont see anyone working on 5.16 , could I work on this? Edit: if anyone searches this in future, feel free to take it - I wanted to argue Q is flat over Z, but now maybe it better first workout localization of rings is flat.

[Kevin Buzzard]

The morally correct way to prove that one is to figure out whether mathlib has flat iff torsion-free for Z-modules and that tensoring by a flat module preserves injectively , but there's probably a low-level approach as well

[Kevin Buzzard]

Sorry, I'm not really able to run the project right now because I have marking to worry about

[Ruben Van de Velde]

But yes, asking here is the safest approach

[Junyan Xu]

Another approach is to use isLocalizedModule_iff_isBaseChange to show that $\widehat{\mathbb{Q}}$, as a ℚ-module, is the localization of the ℤ-module $\widehat{\mathbb{Z}}$ w.r.t. the submonoid nonZeroDivisors ℤ. The localization map is injective because $\widehat{\mathbb{Z}}$ is torsion-free by IsLocalizedModule.eq_zero_iff. As a bonus, you also get that $\widehat{\mathbb{Q}}$ is the localization of $\widehat{\mathbb{Z}}$ w.r.t. the image of the submonoid nonZeroDivisors ℤ in $\widehat{\mathbb{Z}}$ by isLocalizedModule_iff_isLocalization'.

[Ruben Van de Velde]

Is $conj (xy) = conj(x) conj(y)$ actually supposed to be true for quaternions?

[Mario Carneiro]

Does conj negate all the imaginaries? (yes)

[Mario Carneiro]

if so then no, -k = conj(k) = conj(ij) != conj(i)conj(j) = (-i)(-j) = ij = k

[Mario Carneiro]

I believe it is true with a commutation, conj(xy) = conj(y)conj(x)

[Ruben Van de Velde]

Okay, that explains why lean didn't believe me

[Junyan Xu]

Should we use star instead of conj? StarRing has star_mul : ∀ (r s : R), star (r * s) = star s * star r as a field.

[Kevin Buzzard]

Sounds like a much better fit then!

[Ruben Van de Velde]

Done in FLT#79 for when you get out of grading

[Mitchell Lee]

Hi, I strongly feel that it would be easier to develop the Hurwitz quaternions as a subtype of the ($\mathbb{Q}$)-quaternions than to develop them as a standalone structure. This gets you the coercions for free, and you don't have to redefine multiplication and star. Rather, you only have to prove that the set is closed under multiplication and star, and you can use docs#StarSubalgebra, which automatically gives it the structure of a star ring.

[Ruben Van de Velde]

Maybe a parallel development could be informative

[Kevin Buzzard]

I'd happily have both in FLT so we can experiment.

[Kevin Buzzard]

In fact I think that probably the correct thing to do is to fix the definition of docs#QuaternionAlgebra so that it follows Bourbaki's notation in Algebra, i.e. instead of having $i^2\in R$, instead have $i^2=ai+b$, and have quaternion algebras paramatrised by $a,b,c$ with $j^2=c$. This would give the correct definition of a quaternion algebra over an arbitrary field. I would imagine that this would meet with some resistance because the current definition is so "nice" and works in the classical case. Here are the formulas, from Bourbaki Algebra Chapter III:

Screenshot-from-2024-05-14-10-35-27.png

[Chris Birkbeck]

I agree, I think that we need to fix the definition of quaternion algebra either this way or by the CSA of dimension 4 definition.

[Kevin Buzzard]

The problem is that the literature is full of the definition in mathlib because it works fine in char not 2, like defining an elliptic curve to be y^2=cubic.

[Chris Birkbeck]

FWIW the wikipedia definition is the CSA one.

[Ross Bowden]

Voight has this approach for general char (including 2)
image.png

[Kevin Buzzard]

Right: the $K[i]/(i^2-ai-b)$ is the quadratic algebra. In fact arguably the $\Z[\sqrt{d}]$ definition docs#Zsqrtd should be generalised to take a commutative (semi?)ring and a,b as above.

[Filippo A. E. Nuccio]

Mitchell Lee said:

Hi, I strongly feel that it would be easier to develop the Hurwitz quaternions as a subtype of the ($\mathbb{Q}$)-quaternions than to develop them as a standalone structure. This gets you the coercions for free, and you don't have to redefine multiplication and star. Rather, you only have to prove that the set is closed under multiplication and star, and you can use docs#StarSubalgebra, which automatically gives it the structure of a star ring.

The problem with this approach is that it might lead to troubles related to "subtypes" as the one adressed in #12386. My suggestion would be

• if you plan to only use $\mathbb{Z}$-valued quaternions, to proceed as you suggest
• if we will eventually need to replace $\mathbb{Q}$ by a number field and work with the corresponding $\mathcal{O}_K$-quaternions, to rather define it as a stand-alone structure.

[Kevin Buzzard]

The only reason we need this integer lattice is because we're doing an example; my guess is that it's not used at all in the proof of FLT (and my guess is that the definition of quat alg in mathlib is fine for FLT).

[Yaël Dillies]

Filippo A. E. Nuccio said:

The problem with this approach is that it might lead to troubles related to "subtypes" as the one adressed in #12386.

People keep bringing up #12386 as an argument against implementing concrete types as subobjects, but this really is not what the PR is saying. What it says is that you should not define concreteType : Subobject := blah but instead concreteType : Type _ := (blah : Subobject).

[Yaël Dillies]

Importantly, the benefits Mitchell is mentioning apply to both versions indiscriminately.

[Filippo A. E. Nuccio]

@Yaël Dillies Good point, I agree.

[Steven Rossi]

Hi has anyone claimed 6.3 before I take a look?

[Ruben Van de Velde]

I don't think so

[Kevin Buzzard]

I've been in marking hell so I've not really been keeping track, but I guess one algorithm is to check this thread and check the PRs and if there's nothing there then go for it :-)

[Kevin Buzzard]

I've got a couple of days in Wales this week and might be able to catch up

[Steven Rossi]

Great, I checked for PRs and messages but just wanted to be sure I didn't miss anything

[Alex Meiburg]

I'm looking and maybe interested in contributing, but my number theory is not great. Is filling in sorries in https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/AutomorphicRepresentation/Example.lean a useful thing to do?

[Kevin Buzzard]

Sure! In fact it's about the only thing available right now. Currently I am involved in making more API for the finite adeles (e.g. #13021 ) which we need to even state the definition of a quaternionic modular form in the general case. In fact right now I'm a bit hung up on topology; this example you link to is going to turn into an example of a space of such forms, but I need to figure out how the topology on $\widehat{\Z}$ turns into a topology on $\mathbb{Q}\otimes\widehat{\Z}$ and it's not true in general that if $R$ and $S$ are topological rings then $R\otimes S$ inherits one natural topology (it might get more than one). So I'm a bit bogged down with that theoretically, and I'm a bit bogged down with work admin as well (term ends in a month) and this is why things are stagnant right now. I'll remark again that things will really get going by October, and actually in practice by July.

[Alex Meiburg]

Makes sense. ... Quick question, is ZHat a flat module over Z? Or just QHat? ... and is ZHat free? I'm getting all tripped up here. (If needing to ask these questions mean that I probably cannot contribute usefully, let me know.)

[Kevin Buzzard]

An abelian group is flat over $\mathbb{Z}$ iff it's torsion-free, and we've already proved that it's torsion-free IIRC. I don't know whether we have this result in mathlib though.

[Kevin Buzzard]

ZHat isn't free though, because ZHat/pZHat = Z/pZ so if it were free it would have to be free on one generator, which can't be right because it's uncountable.

[Filippo A. E. Nuccio]

Kevin Buzzard said:

ZHat isn't free though, because ZHat/pZHat = Z/pZ so if it were free it would have to be free on one generator, which can't be right because it's uncountable.

I agree with your conclusion, but the only way I can see it is a topological Nakayama lemma. Is there a more direct way of proving that if it were free it would be free on one gen?

[Adam Topaz]

I don't think any version of Nakayama is needed. If you have a basis $S$ for $\hat\Z$ then $\hat\Z/p$ must be isomorphic to $\Z^{(S)}/p = (\Z/p)^{(S)}$, but since $\hat\Z/p$ is isomorphic to $\Z/p$ it would follow that $S$ is a singleton.

[Scott Carnahan]

Alternative argument: ZHat has nonzero infinitely 2-divisible elements.

[Filippo A. E. Nuccio]

Adam Topaz said:

I don't think any version of Nakayama is needed. If you have a basis $S$ for $\hat\Z$ then $\hat\Z/p$ must be isomorphic to $\Z^{(S)}/p = (\Z/p)^{(S)}$, but since $\hat\Z/p$ is isomorphic to $\Z/p$ it would follow that $S$ is a singleton.

Oh sure, thanks.

[Filippo A. E. Nuccio]

Scott Carnahan said:

Alternative argument: ZHat has nonzero infinitely 2-divisible elements.

Yes yes, I agree, I was looking for an easy proof of the implication "if free then free on one gen", but I was already OK with the fact that it is not free.

[Johan Commelin]

@Kevin Buzzard Just take the tensor product as condensed abelian groups :grinning:

[Kevin Buzzard]

I don't know what topology to put on $\mathbb{Q}$. As a subring of the finite adeles I think it has some crazy topology

[Kevin Buzzard]

Basically I'm totally confused right now about whether I should just do what the books do ("Z-hat is open with its usual topology and it all works") or do something more conceptual.

[Adam Topaz]

If you identify Q with the colimit of copies of Z w.r.t. the inclusions x -> nx as n varies, is this not the right topology?

[Kevin Buzzard]

Yes probably.

[Kevin Buzzard]

Oh wait, what topology are you putting on Z?

[Kevin Buzzard]

The one coming from Zhat?

[Adam Topaz]

No, what I mean is identify Q \otimes Zhat with the colimit of Zhats

[Adam Topaz]

(I’m identifying Z otimes Zhat with Zhat)

[Kevin Buzzard]

Right, my guess is that this is the correct topology. I then have to prove that multiplication is continuous

[Adam Topaz]

Yeah I think that will be more challenging with this approach

[David Michael Roberts]

Does the product preserve this colimit separately in each slot?

[Kevin Buzzard]

I don't really understand David's question. I'm worried that proving that multiplication is continuous will be a pain whatever method I use.

[David Michael Roberts]

Mapping out of a colimit means you only need to check continuity on the objects of the colimit diagarm. And showing that a binary operation on a colimit is continuous is easier when you know that the product commutes (at least on each side separately) with the colimit. But this is mathematics, not Lean, so I don't know what I'm blithely waving away in the above description.

[Steven Rossi]

Are there any concerns with upgrading the mathlib version and using simp in proofs? Having RingCon.coe_bot is very nice

[Ruben Van de Velde]

As in FLT#82?

[Steven Rossi]

Ah great, missed that. Had the same changes locally

[Kevin Buzzard]

Sorry, I'll try to merge today

[Ruben Van de Velde]

Thanks for the merge, I did another one for good measure at FLT#89 :)

[Kevin Buzzard]

I'm going to spend the afternoon on FLT so hopefully I'll get it merged

[Ruben Van de Velde]

I have a half-finished proof for exists_near that I'll look into some more tomorrow