Seminar of Algebra

Back to main page.

Formalización de cuerpos locales en Lean

Speaker:
María Inés de Frutos Fernández (Universidad Autónoma de Madrid)
Email:
maria.defrutos@uam.es
Location:
Departamento de Álgebra
Date:
Fri, 1 dec 2023 10:00
Soy investigadora postdoctoral Margarita Salas. Mi investigación se centra en la formalización matemática y la teoría algebraica de números

El objetivo de esta charla es presentar una formalización en el asistente interactivo de demostración Lean de la teoría básica de los cuerpos discretamente valorados. En particular, demostramos que la bola unidad con respecto a una valoración discreta en un cuerpo es un anillo de valoración discreta y, recíprocamente, que la valoración ádica en el cuerpo de fracciones de un anillo de valoración discreta es discreta. Definimos extensiones finitas de valoraciones y de anillos de valoración discreta, y probamos algunos resultados de tipo global a local. Partiendo de esta teoría general, formalizamos la definición abstracta y algunas propiedades fundamentales de los cuerpos locales, y demostramos que las extensiones finitas del cuerpo $\mathbb{Q}_p$ de números $p$-ádicos y el cuerpo $\mathbb{F}_p(!(X)!)$ de series de Laurent sobre $\mathbb{F}_p$ son cuerpos locales. Este proyecto es un trabajo conjunto con Filippo Nuccio.