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