Quaternion algebras are wrong

Stream: mathlib4

[Kevin Buzzard]

Mathlib has a naive definition of quaternion algebras:

/-- Quaternion algebra over a type with fixed coefficients $a=i^2$ and $b=j^2$.
Implemented as a structure with four fields: `re`, `imI`, `imJ`, and `imK`. -/
@[ext]
structure QuaternionAlgebra (R : Type*) (a b : R) where
  /-- Real part of a quaternion. -/
  re : R
  /-- First imaginary part (i) of a quaternion. -/
  imI : R
  /-- Second imaginary part (j) of a quaternion. -/
  imJ : R
  /-- Third imaginary part (k) of a quaternion. -/
  imK : R

This definition is analogous to defining an elliptic curve over a field to be a pair $(A,B)$ representing the equation $y^2=x^3+Ax+B$ -- that equation can be singular, and it doesn't cover all cases in small characteristic. The same is true here. There is a standard definition of a quaternion algebra over a field in the literature, and mathlib's definition is wrong in "both directions": there are actual quaternion algebras in characteristic 2 which cannot be represented as mathlib-quaternion-algebras (because there are degree 2 extensions of fields in char 2 which aren't of the form "adjoin a square root"), and conversely there are mathlib-quaternion-algebras over fields which are not quaternion algebras according to the standard definition (e.g. you can set $a=b=0$ and the corresponding algebra is not a central simple algebra).

As well as these issues, there is also the moral objection that we don't define a $k$-vector space to be $k^n$, we define it to be something which satisfies the vector space axioms, and yet (unlike in the literature) our quaternion algebras all come equipped with a canonical basis. One can apply this same moral objection to our definition of elliptic curves, which don't come with a preferred realisation as a smooth plane cubic, but here there are some good counter-arguments for preferring our plane cubic definition: firstly, many elliptic curves in arithmetic really do come presented as a plane cubic (for example the Frey curve, key to FLT, or curves which show up when solving Diophantine equations). And secondly the morally correct alternative (a smooth proper connected group scheme of genus 1 equipped with a marked point) was completely inaccessible when we made the definition of an elliptic curve, and indeed the definition still cannot be formalized in mathlib because we still don't have the concept of genus of a curve and haven't really made up our minds about how to talk about group schemes in the non-affine case. In stark contrast to this, it's easy to write down the correct definition of a quaternion algebra in mathlib, and has been for years; furthermore some students at Imperial have developed a huge theory of central simple algebras and now need to think about PRing to mathlib.

I need quaternion algebras for FLT but only in characteristic 0 so I am not desperate to change the definition, but I do find it a bit weird that we've diverged from the literature. Bourbaki define quaternion algebras "explicitly" like we do, but use three parameters $a,b,c$ and have equations $i^2=ai+b$ and $j^2=c$. This is at least valid in characteristic 2, but allows rings which are not quaternion algebras according to Wikipedia (which is the definition I think we should aspire to). Does anyone have any comments about what we should do here? I remember talking about this to @Antoine Chambert-Loir at some point...

[Mario Carneiro]

Could you maybe be a bit more explicit about what the proposed alternative is here?

[Mario Carneiro]

as a newbie to this kind of mathematics that definition looks perfectly reasonable

[Mario Carneiro]

I suspect the issue is that "quaternion algebra" here is the wrong word. This looks like what you get if you take hamilton's quaternions and just generalize the ring without doing anything else. In particular, it's a construction not a typeclass

[Kevin Buzzard]

There are at least two other definitions which deserve the name QuaternionAlgebra: the definition according to Wikipedia (which could be IsQuaternionAlgebra, a class predicate on algebras) and a better variant of our definition which takes in three inputs not two and allows i^2=ai+b. An additional issue is that there is a nonzeroness condition which is missing in our definition. In the elliptic curve case we have docs#WeierstrassCurve which is the equation and then docs#EllipticCurve which has the nonsingularity condition. Similarly here we should have a nonvanishing condition which actually makes our definition into a quaternion algebra.

In short I'm uncomfortable about the fact that our definition is mathematically wrong for two reasons and morally wrong because it's not a class.

[Scott Carnahan]

I am certainly in favor of a refactor changing to the rank 4 central simple algebra definition. Bourbaki's definition looks like it should be named something like QuaternionAlgebra.mk' or QuaternionAlgebra.ofBasis

[Antoine Chambert-Loir]

These are cases where I don't really know what to do. Over a field, all legit quaternion algebras should be there, and having some explicitly presented algebras is important. Of course, the simple central algebra point of view is ultimately vital. Over a ring, the situation is complicated because orders of quaternion algebras are important objects, but they are usually not Azumaya algebras — bad reduction happens.

[Edison Xie]

So if I get this right, we should only define quaternion algebra over fields as rank 4 central simple algebras?

[Edison Xie]

What about over rings though

[Kevin Buzzard]

Over (commutative) rings the correct object is an Azumaya algebra

[Kevin Buzzard]

But like several objects in algebraic geometry it's sometimes best to develop the theory over fields first and then generalise to rings/schemes later (because a bunch of the scheme proofs use devissage to reduce to fields)

[Edison Xie]

Hmmm do we have azumaya algebra in Mathlib yet?

[Antoine Chambert-Loir]

I don't think so, but we could easily define them. It just requires the definition of a separable (possibly noncommutative) algebra.

[Edison Xie]

variable (F : Type*) [Field F]

class IsQuaternionAlgebra (Q : Type*) [Ring Q] [Algebra F Q] extends
  Algebra.IsCentral F Q, IsSimpleRing Q where
  rank_four : Module.finrank F Q = 4

Does this definition looks right?

[Riccardo Brasca]

No, that's the point: this works if Q is a field, but is "wrong" otherwise. Instead of IsSimpleRing we want something like IsSeparable, but currently Algebra.IsSeparable works well only over a field.

[Riccardo Brasca]

But I think it is better to stay over a field, at least at the beginning

[Eric Wieser]

extends IsSimpleRing is not legal there, as it doesn't capture F

[Edison Xie]

wait but I thought over a field quaternion is dim 4 central simple algebra?

[Edison Xie]

also why does Q have to be field

[Edison Xie]

didn't quite follow

[Riccardo Brasca]

Sorry, I swapped F and Q. Yes, over a field the definition is mathematically OK

[Kevin Buzzard]

For FLT we only need the theory over fields and my instinct is to develop that first (in such a way that it works for all fields).

[Edison Xie]

Eric Wieser said:

extends IsSimpleRing is not legal there, as it doesn't capture F

Why is it not legal? I’m still a bit confused :anguish::anguish:

[Johan Commelin]

@Edison Xie I agree it is confusing. Let me try to explain. (We should document this somewhere, maybe on a blogpost?)

By writing extends, there will automatically be an instance: [IsQuaternionAlgebra F Q] -> [IsSimpleRing Q].
Now suppose that 3 files later, you are working on a proof, and you need to know [IsSimpleRing Q]. Lean will remember "Aaah, I know that quaternion algebras are simple!" And it will start hunting for [IsQuaternionAlgebra ?F Q]. Where the ?F is unknown, because it isn't determined by [IsSimpleRing Q]. And so Lean goes on a wild goose chase. Conclusion: it shouldn't do that, so we shouldn't create the automatic instance.

[Johan Commelin]

Now you can fairly ask the question: can't extends recognise this on its own, and just do a "structure extends" without making it an instance. And I think it should be able to do that. Maybe @Kyle Miller can say more about this?

[Daniel Weber]

Would it make sense for F to be an outParam?

[Kyle Miller]

@Johan Commelin It should already give an error in this case, and I think it would be surprising if extends silently omitted instances. I wonder if there's room for "non-instance parents" as an additional feature.

[Johan Commelin]

In this case, an outParam might actually make sense. Because an algebra Q can only be a quaternion algebra over 1 field (up to isom), namely its center.
This is in contrast with Module R M, where R used to be an outParam long ago, but that caused many headaches because $\mathbb{C}$ is naturally a module over $\mathbb{C}$, $\R$, $\mathbb{Q}$, $\Z$, and $\N$.

[Johan Commelin]

Of course the "(up to isom)" is still hinting at potential sources of trouble. outParam only works if the field is in practice unique up to defeq. But I'm claiming that this might actually be the case in 99%.

[Kevin Buzzard]

Unfortunately whilst it might be the case that you're a quaternion algebra over one field, you might be an algebra over several fields. Is this a problem?

[Edward van de Meent]

Johan Commelin said:

In this case, an outParam might actually make sense. Because an algebra Q can only be a quaternion algebra over 1 field (up to isom), namely its center.

still, then in order to not get defeq issues, do we only want the IsQuaternionAlgebra (center Q) Q instance? i doubt that...

[Junyan Xu]

Antoine Chambert-Loir said:

I don't think so, but we could easily define them. It just requires the definition of a separable (possibly noncommutative) algebra.

I think Definition 4 on Wikipedia is the most accessible, without requiring defining IsSeparable first.
image.png

[Edison Xie]

That’s right and Jujian Zhang already formalised morita equivalence so theoretically it could be easily done

[Edison Xie]

Opened #20489 but still a work in progress if anyone interested could go take a look

[Edison Xie]

opened #20657 about the definition of quaternion on Bourbaki's book

[Andrew Yang]

Shouldn't we just replace the old one?

[Eric Wieser]

Is the old one just a specialization of the new one?

[Edison Xie]

Eric Wieser said:

Is the old one just a specialization of the new one?

Yes it is but I'm thinking maybe do that in the next PR?

[Edison Xie]

I could do it in this one but I thought one PR should only be doing one thing?

[Eric Wieser]

I think generalizing the existing one in place would be a smaller diff

[Eric Wieser]

If it's really just adding an extra c parameter, which you could possible even give a default value to preserve the old behavior

[Edison Xie]

hmmm okay

[Edison Xie]

I'll just wait for more people to respond on this for now :))

[Edison Xie]

If that's what we all think then I'll jus replace the old one

[Edison Xie]

how should we name them?

[Edison Xie]

Maybe QuaternionAlgebra and Quaternion?

[Kevin Buzzard]

I like the idea of replacing what we have already. My mental model was that this would be a huge PR because you'd have to redo the quaternion algebra file and also patch all the applications, but probably the quaternion algebra diff wouldn't be so bad and if you give the new variable a default value of 0 perhaps the patches won't be so bad either.

[Kevin Buzzard]

If we do this then the only remaining objection I have to the name is that it would be then like defining an elliptic curve over a field to be [a1,a2,a3,a4,a6] rather than "this + disc != 0". Nowadaysin mathlib we have docs#WeierstrassCurve k defined to be k^5 and then docs#WeierstrassCurve.IsElliptic to be "this + disc != 0". With Edison's new definition we can still set everything to be 0 and get a rank 4 algebra which is not a quaternion algebra in the sense of the usual definition, because it is degenerate. I must be honest: I don't know the conditions on the coefficients which ensure that that the algebra is a quaternion algebra in the usual sense.

[Eric Wieser]

I'm not sure having parametrizations which aren't actually quaternion algebras is that different to defining MonoidAlgebra which accepts non -monoids and produces non-algebras

[Eric Wieser]

(and I think both are sensible)

[Edison Xie]

done changing the files in Mathlib I could be ignoring some of the docstring errors but in general this should be what we want

[Kevin Buzzard]

Eric Wieser said:

I'm not sure having parametrizations which aren't actually quaternion algebras is that different to defining MonoidAlgebra which accepts non -monoids and produces non-algebras

There is something of a difference here: if you give MonoidAlgebra a monoid, it will produce an algebra, i.e. it's not possible to construct something which a mathematician would say was mathematically wrong, just something which a mathematician would say was missing some structure. But right now QuaternionAlgebra ℝ 0 0 produces something which is an ℝ-algebra but is genuniely not a quaternion algebra: it can't be the quaternions because they don't have any nonzero solutions to $x^2=0$, and it can't be $M_2(\R)$ because if this ring acted faithfully on $\R^2$ then $i^2=0$ means that one can choose a basis such that $i$ is represented by $(0,1;0,0)$ and then an explicit matrix calculation shows that there are no nonzero $j$ with $ij=-ji$ and $j^2=0$, as $ij=-ji$ forces $j$ to be diagonal. Maybe the condition over fields is just that $c_1$ and $c_2$ are nonzero?

[Antoine Chambert-Loir]

I just checked Bourbaki (Algebra, chap 3), and they don't impose any condition on their quaternion algebras.

[Antoine Chambert-Loir]

By the way, their presentation, starting from quadratic algebras and Cailey algebra also furnished octonions.

[Antoine Chambert-Loir]

In Algebra, chap 8, §19, they go back to quaternion algebras and study their center, simplicity, and explain when they are fields.

[Kevin Buzzard]

Do they explain when they are quaternion algebras? :-) Thanks for the reference! I think that if it's good enough for Bourbaki it's probably good enough for us.

[Antoine Chambert-Loir]

They are quaternion algebras, by definition, and, over a field, are central simple when $(4a+b^2)c\neq 0$. This is proposition 3 of chapter 8, §19.

[Antoine Chambert-Loir]

I think it's the correct way to do, because you don't want to have to carry conditions whenever you wish to talk about those algebras.

[Kevin Buzzard]

My experience with elliptic curves was similar; I defined them with the disc!=0 condition and then David Ang started using them and found that a whole bunch of results were true for Weierstrass curves more generally. The only difference was that that there were distinctions Weierstrass curve for the plane cubic and IsElliptic for disc!=0. Here you are claiming that Mathlib's quaternion algebras are quaternion algebras by definition but I dispute this claim; it might be what Bourbaki says but it's not what Wikipedia says or what the internet in general says or what I was taught. But this is not really relevant; after this discussion I'm pretty convinced that the current state of #20657 is the way to go and I suspect you are too.

[Antoine Chambert-Loir]

i love internet and Wikipedia, but don't trust them too much.

[Antoine Chambert-Loir]

and we were taught and teach simplified versions of what ought to be done in a Great Mathematical Library.

[Damiano Testa]

I personally find that having QuaternionAlgebras being the ones where you just add square roots of any two elements, with no extra consideration, and then central simple algebras, with all the rest of the conditions is very clear.

Whenever I taught them, I restrained from using the words quaternion algebras in a situation where they were not central simple algebras and felt that I was lacking a term. I think that sometimes I called them "quadratic algebras" and felt the need to add lots of disclaimers about the name.

[Damiano Testa]

And with elliptic curves, the whole "elliptic curve factorisation method" actually relies on having "elliptic curves" that are not elliptic curves!

[William Coram]

I had an old project I was working on where I was generalising quaternon algebras to Bourbaki's definition and giving lemmas for when they are split (in both cases of char 2 and general char fields) via defining explicit isomorphisms.
If people are interested I could work on updating my code for the second part and create a PR for them. That being said, I am not sure if Mathlib is the place for these explicit isomorphisms, especially when it can be proved directly using other methods (e.g. Thm 5.4.4 in Voights QA book).

[Kevin Buzzard]

You might want to liaise with @Edison Xie who has also been thinking about this.

[Edison Xie]

William Coram said:

I had an old project I was working on where I was generalising quaternon algebras to Bourbaki's definition and giving lemmas for when they are split (in both cases of char 2 and general char fields) via defining explicit isomorphisms.
If people are interested I could work on updating my code for the second part and create a PR for them. That being said, I am not sure if Mathlib is the place for these explicit isomorphisms, especially when it can be proved directly using other methods (e.g. Thm 5.4.4 in Voights QA book).

I have the some results about quaternions and dimension four central simple algebra but you are welcome to PR more stuff about it if later I found your results are corollaries of my theorem then I’ll make another PR to change that! :))