Formalizing local fields in Lean - María Inés de Frutos F...

Stream: Lean Together 2024

[María Inés de Frutos Fernández]

Local Fields slides :
local_fields.pdf

[Johan Commelin]

Are you connecting your mixed characteristic local fields to Mathlib/Algebra/CharP/MixedCharZero.lean? That connection is listed as a todo in the module docstring of that file.

[David Ang]

Are there any plans to replace the existing mathlib p-adic numbers definition with the one in your project?

[María Inés de Frutos Fernández]

There were some discussions at the Machine-Checked Mathematics workshop about adding some sort of IsPadic definition, so that both versions can be used and the user does not need to worry about the concrete implementation.

[Filippo A. E. Nuccio]

There have been some discussions about this in Leiden this summer. We agreed that we certainly also need the previous/old version, as it is more "down-to-earth". @Mario Carneiro was suggesting to define a specific class of "$p$-adically complete field" and to ignore the particular implementation.

[Filippo A. E. Nuccio]

(ops, sorry...)

[David Ang]

I see. On another note: we can also define Q_p as the fraction field of Z_p defined using inverse limits - was this useful anywhere in your project?

[Mario Carneiro]

more specifically, IIRC I was suggesting that the universal property of Q_p or the definitions in it are lifted to a class so that you can use \Q_[p] in its place and still use all the theorems

[Mario Carneiro]

(as opposed to generalizing all results about \Q_[p] to a class so that both Q_p and \Q_[p] exist and all the theorems apply to both)

[María Inés de Frutos Fernández]

David Ang said:

I see. On another note: we can also define Q_p as the fraction field of Z_p defined using inverse limits - was this useful anywhere in your project?

We did not need that version of the definition.