Jonathan Hanke / Quadratic Forms Formalization

Stream: new members

[Jonathan Hanke]

Hi! I'm a new Lean4 user looking to learn Lean4 and to formalize definitions / examples / theorems about the arithmetic of quadratic forms over QQ and ZZ.

I've started a new project here to formalize the Hasse-Minkowski theorem based on Cassels "Rational Quadratic Forms" book as a way to learn and contribute. Anyone interested in working on this, please feel free to let me know! Thanks and great to meet everyone here! =)

[Kevin Buzzard]

I thought about this at an LFTCM about two years ago. One thing I observed is that the following is true: if K is any number field and V is any vector space over K (doesn't have to be finite-dimensional!) equipped with a quadratic form, then the form has a global zero iff it has local zeros.

In the FLT project we are currently working on a proof of $K\otimes_KK_v=\oplus_{w|v}L_v$ for $L/K$ a finite extension of number fields; it currently has a sorry, the guts of which is that if $N/M$ is finite extension of p-adic fields then the degree is $ef$. Assuming this, you can reduce from $K$ to $\mathbb{Q}$, which may or may not be helpful depending on which route you're taking.

When we worked on the project at LFTCM there was a big problem in that there was no theory of base change for bilinear or quadratic forms. I'm assuming we have this now?

[Eric Wieser]

I believe you examined a thesis which described the process of adding the base change to mathlib :)

[Eric Wieser]

Though I now remember the gap; docs#QuadraticForm.baseChange works in non-free modules in characteristic not 2, whereas a proposed replacement works in any characteristic but only in free modules

[Kevin Buzzard]

@Jonathan Hanke an idle question I have about this area: is local-global for quadratic forms true in the case of global function fields of characteristic 2? I remember Eric and I getting tied up in knots trying to do base change in char 2.

[Junyan Xu]

I found this paper by searching hasse minkowski "characteristic 2":
image.png
The reference given is this:
image.png

[Junyan Xu]

while Gemini hallucinated a counterexample:
image.png

[Junyan Xu]

From the foreword (notes to the reader) of Lam's Introduction to Quadratic Forms over Fields:
image.png
I looked into the three references but didn't see char 2 global fields being treated.

Cassels' book sketches a proof for number fields but not global function fields:
image.png

Gerstein's Basic Quadratic Forms refers to O'Meara's Introduction to Quadratic Forms for a unified proof:
image.png
image.png

[Jonathan Hanke]

@Junyan Xu. Thanks for the characteristic 2 similitude / isometry paper reference and for the other literature research. Following up on O'Meara's book, it seems that while he talks about function fields as global fields, after p82 many of the harder statements are restricted to exclude fields with characteristic 2. He mentions this explicitly on p82:

image.png

image.png

and then again on p112, p158, and p206. On p152 (Section 66) he excludes local fields of characteristic 2:

image.png

so the Hasse-Minkowski statement there will only apply in that context. So the Arxiv reference you mentioned closes this literature gap.

@Kevin Buzzard @Eric Wieser Kevin -- Thanks for the question. I was chatting with Eric in early May about Clifford algebras in characteristic 2 and came up with some additional examples which we partly formalized. I can share the writeup when it's done / formalized in case it's of interest . =)

[Junyan Xu]

Yeah, I think O'Meara's book shows that the proofs for global function fields and number fields can be unified, but the approach still doesn't encompass the char 2 case.