María Inés de Frutos-Fernández

midff@math.uni-bonn.de

I am María Inés, a postdoctoral researcher at the University of Bonn, working in the workgroup on Formal Mathematics led by Floris van Doorn. Previously, I worked as a Margarita Salas Postdoctoral Researcher at Universidad Autónoma de Madrid (with Daniel Macias Castillo) and as a Research Associate at Imperial College London, in Kevin Buzzard’s’s research group. Before joining Imperial College, I worked as an Assistant Professor (Profesor Ayudante Doctor) at Universidad Nebrija. I earned my PhD in Mathematics from Boston University in 2020, under the supervision of Jared Weinstein.

My main research interests are mathematical formalization and number theory.

Here is my CV.

Last updated: 4 November 2024.

Selected Publications

CPP
A Formalization of Complete Discrete Valuation Rings and Local Fields

María Inés de Frutos-Fernández, and Filippo A. E. Nuccio Mortarino Majno di Capriglio

In Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs 2024

Abs Bib HTML PDF

Local fields, and fields complete with respect to a discrete valuation, are essential objects in commutative algebra, with applications to number theory and algebraic geometry. We formalize in Lean the basic theory of discretely valued fields. In particular, we prove that the unit ball with respect to a discrete valuation on a field is a discrete valuation ring and, conversely, that the adic valuation on the field of fractions of a discrete valuation ring is discrete. We define finite extensions of valuations and of discrete valuation rings, and prove some global-to-local results. Building on this general theory, we formalize the abstract definition and some fundamental properties of local fields. As an application, we show that finite extensions of the field Q_p of p-adic numbers and of the field F_p((X)) of Laurent series over F_p are local fields.
@inproceedings{dFN23, author = {{de Frutos-Fernández}, María Inés and {Nuccio Mortarino Majno di Capriglio}, Filippo A. E.}, title = {A Formalization of Complete Discrete Valuation Rings and Local Fields}, year = {2024}, isbn = {9798400704888}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, url = {https://doi.org/10.1145/3636501.3636942}, doi = {10.1145/3636501.3636942}, booktitle = {Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs}, pages = {190–204}, numpages = {15}, keywords = {Lean, algebraic number theory, discrete valuation rings, formal mathematics, local fields, mathlib}, location = {, London, UK, }, series = {CPP 2024} }
LIPIcs
Formalizing Norm Extensions and Applications to Number Theory

María Inés de Frutos-Fernández

In 14th International Conference on Interactive Theorem Proving (ITP 2023) 2023

Abs Bib HTML PDF

The field R of real numbers is obtained from the rational numbers Q by taking the completion with respect to the usual absolute value. We then define the complex numbers C as an algebraic closure of R. The p-adic analogue of the real numbers is the field Q_p of p-adic numbers, obtained by completing Q with respect to the p-adic norm. In this paper, we formalize in Lean 3 the definition of the p-adic analogue of the complex numbers, which is the field C_p of p-adic complex numbers, a field extension of Q_p which is both algebraically closed and complete with respect to the extension of the p-adic norm. More generally, given a field K complete with respect to a nonarchimedean real-valued norm, and an algebraic field extension L/K, we show that there is a unique norm on L extending the given norm on K, with an explicit description. Building on the definition of C_p, we formalize the definition of the Fontaine period ring B_HT and discuss some applications to the theory of Galois representations and to p-adic Hodge theory. The results formalized in this paper are a prerequisite to formalize Local Class Field Theory, which is a fundamental ingredient of the proof of Fermat’s Last Theorem.
@inproceedings{defrutosfernandez:LIPIcs.ITP.2023.13, author = {{de Frutos-Fernández}, María Inés}, title = {{Formalizing Norm Extensions and Applications to Number Theory}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {13:1--13:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, isbn = {978-3-95977-284-6}, issn = {1868-8969}, year = {2023}, volume = {268}, editor = {Naumowicz, Adam and Thiemann, Ren\'{e}}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, url = {https://drops.dagstuhl.de/opus/volltexte/2023/18388}, urn = {urn:nbn:de:0030-drops-183880}, doi = {10.4230/LIPIcs.ITP.2023.13}, annote = {Keywords: formal mathematics, Lean, mathlib, algebraic number theory, p-adic analysis, Galois representations, p-adic Hodge theory} }
arXiv
The refined class number formula for Drinfeld modules

María Inés de Frutos-Fernández, Daniel Macías Castillo, and Daniel Martínez Marqués

2023

Abs Bib HTML PDF

Let K/k be a finite Galois extension of global function fields. Let E be a Drinfeld module over k. We state and prove an equivariant refinement of Taelman’s analogue of the analytic class number formula for (E, K/k), and derive explicit consequences for the Galois structure of the Taelman class group of E over K.
@unpublished{RCNF, title = {The refined class number formula for Drinfeld modules}, author = {{de Frutos-Fernández}, María Inés and {Macías Castillo}, Daniel and {Martínez Marqués}, Daniel}, note = {Preprint}, year = {2023}, }
JTNB
Moduli Spaces of Shtukas over the Projective Line

María Inés de Frutos-Fernández

Journal de théorie des nombres de Bordeaux 2022

Abs Bib HTML PDF

We provide explicit equations for moduli spaces of Drinfeld shtukas over the projective line P^1 with Γ(N), Γ_1(N) and Γ_0(N) level structures, where N is an effective divisor on P^1. If the degree of N is high enough, these moduli spaces are relative surfaces. We study some invariants of the moduli space of shtukas with Γ_0(N) level structure for several degree 4 divisors on P^1.
@article{JTNB22, title = {Moduli Spaces of Shtukas over the Projective Line}, author = {{de Frutos-Fernández}, María Inés}, journal = {Journal de théorie des nombres de Bordeaux}, volume = {34}, number = {2}, pages = {393--418}, year = {2022}, doi = {10.5802/jtnb.1207}, url = {https://jtnb.centre-mersenne.org/articles/10.5802/jtnb.1207/}, }

LIPIcs

Formalizing the Ring of Adèles of a Global Field

María Inés de Frutos-Fernández

In 13th International Conference on Interactive Theorem Proving (ITP 2022) 2022

Abs Bib HTML PDF

The ring of adèles of a global field and its group of units, the group of idèles, are fundamental objects in modern number theory. We discuss a formalization of their definitions in the Lean 3 theorem prover. As a prerequisite, we formalize adic valuations on Dedekind domains. We present some applications, including the statement of the main theorem of global class field theory and a proof that the ideal class group of a number field is isomorphic to an explicit quotient of its idèle class group.

@inproceedings{defrutosfernandez:LIPIcs.ITP.2022.14,
  author = {{de Frutos-Fernández}, María Inés},
  title = {{Formalizing the Ring of Ad\`{e}les of a Global Field}},
  booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages = {14:1--14:18},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  isbn = {978-3-95977-252-5},
  issn = {1868-8969},
  year = {2022},
  volume = {237},
  editor = {Andronick, June and de Moura, Leonardo},
  publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address = {Dagstuhl, Germany},
  url = {https://drops.dagstuhl.de/opus/volltexte/2022/16723},
  urn = {urn:nbn:de:0030-drops-167232},
  doi = {10.4230/LIPIcs.ITP.2022.14},
  annote = {Keywords: formal math, algebraic number theory, class field theory, Lean, mathlib}
}