Formalizing multi-graded Brenner-Schröer Proj schemes and dilatations of rings in Lean4

Resumen Técnico: Formalización de Esquemas Proj de Brenner–Schröer Multigradados y Dilataciones de Anillos en Lean4

Planteamiento del Problema
El artículo aborda la formalización de construcciones avanzadas en la geometría algebraica multigraduada dentro del probador de teoremas Lean4. Mientras que la geometría algebraica clásica suele apoyarse en anillos graduados por los números naturales ($\mathbb{N}$) o los enteros ($\mathbb{Z}$), los desarrollos modernos —como los de la teoría de Lie, la teoría de representaciones geométricas y el programa del modelo mínimo— requieren anillos graduados por monoide o grupos más generales. Específicamente, los autores se centran en la construcción Proj de Brenner–Schröer, que generaliza la construcción Proj clásica al entorno multigraduado, y en la teoría de dilataciones de anillos, una operación relacionada con la localización y los sopletes (blowups). El desafío radica en implementar estas estructuras en un marco de teoría de tipos (Lean4) donde la distinción entre un anillo $A$ y su descomposición de suma directa $\bigoplus_{i \in \iota} A_i$ debe gestionarse rigurosamente sin sacrificar la usabilidad ergonómica.

Metodología
Los autores adoptan un enfoque algebraico consistente con la literatura existente (específicamente siguiendo el tratamiento en [9]) para formalizar estos conceptos en Lean4. La metodología implica:

1. Configuración General para Estructuras Graduadas: La formalización define anillos y módulos graduados donde el monoide de graduación $\iota$ es un grupo abeliano arbitrario. Para manejar las restricciones de la teoría de tipos, los autores distinguen entre el anillo $A$ y sus componentes graduados $A_i$, utilizando estructuras SetLike para tratar los componentes como subgrupos manteniendo la capacidad de alternar entre el anillo y su descomposición de suma directa.
2. Localización Homogénea y "Potions" (Pociones): Una innovación técnica central es la definición de "potions" ($\vartheta(S)$), definidas como la parte de grado cero de una localización homogénea $A(S)$. A diferencia de la localización estándar, las potions no se definen como subanillos del anillo localizado, sino como cocientes de triples $(i, a, b)$ donde $a, b$ son elementos homogéneos del mismo grado y $b \in S$. Esta estructura facilita la inducción y el acceso a numeradores y denominadores.
3. Relevancia e Ingredientes de Pociones Buenos: Los autores formalizan el concepto de submonoides homogéneos "relevantes", donde el subgrupo generado por los grados de los elementos en el submonoide tiene índice finito (o cociente de torsión) en el grupo de graduación. Definen "ingredientes de pociones buenos" como submonoides que son tanto relevantes como finitos generadores.
4. Pegado y Construcción Proj: El esquema Proj se construye pegando esquemas afines $\text{Spec}(\vartheta(S_i))$ asociados a una familia de ingredientes de pociones buenos. Los datos de pegado dependen de isomorfismos entre productos tensoriales de potions (por ejemplo, $\vartheta(ST) \otimes_{\vartheta(S)} \vartheta(SR) \cong \vartheta(RST)$), los cuales se establecen mediante "generadores de pociones".
5. Dilataciones: El artículo formaliza las dilataciones de anillos con respecto a un multicentro (una colección de ideales y elementos). Esto implica definir clases de equivalencia de fracciones simbólicas $m/a^\nu$ y probar la propiedad universal que caracteriza a las dilataciones.

Contribuciones Clave y Resultados
El artículo presenta una biblioteca completa de definiciones, lemas y teoremas en Lean4:

• Formalización de Proj Multigraduado: Los autores proporcionan una implementación completa de la construcción Proj de Brenner–Schröer. Esto incluye la definición de localización homogénea, la teoría de potions y el pegado de esquemas afines para formar el esquema Proj.
• Generadores de Pociones e Isomorfismos: Una contribución significativa es la formalización de los "generadores de pociones", que permiten a los autores probar que para un $S$ relevante y un $T$ finitamente generado, el morfismo $\text{Spec}(\vartheta(ST)) \to \text{Spec}(\vartheta(S))$ es una inmersión abierta. También establecen las condiciones de cociclo requeridas para la construcción de pegado.
• Funtorialidad: Se muestra que la construcción Proj es un funtor contravariante de la categoría de anillos graduados a la categoría de esquemas. Los autores abordan cuidadosamente las sutilezas de la teoría de tipos donde la imagen de una familia bajo un homomorfismo de anillos no es definiciónmente igual a la familia objetivo, requiriendo el uso de morfismos específicos (projHomOfLE) para establecer la funtoriedad.
• Dilataciones: El artículo formaliza la definición de dilataciones de anillos y prueba su propiedad universal: para cualquier homomorfismo de anillos $\chi: A \to B$ donde las imágenes de los elementos del centro son no-divisores de cero y generan las imágenes de los ideales correspondientes, existe un único morfismo desde la dilatación hacia $B$.
• Isomorfismo de Familias Ampliadas: Los autores prueban que ampliar una familia de ingredientes de pociones buenos (incluyendo productos de ingredientes existentes) resulta en un esquema Proj isomórfico, asegurando la robustez de la construcción frente a la elección de la familia generadora.

Significancia
El artículo reclama su significancia principalmente como un paso fundacional en la formalización de la geometría algebraica avanzada. Sirve como:

1. Documentación: Un relato detallado de las definiciones, decisiones de diseño y principales resultados subyacentes a la formalización, destinado a guiar a futuros desarrolladores.
2. Fundación: Una biblioteca reutilizable para futuras extensiones en la geometría algebraica formalizada, particularmente para proyectos que requieren estructuras multigraduadas o dilataciones.
3. Verificación: Una implementación formal completa que verifica la corrección de la construcción de Brenner–Schröer y la teoría de dilataciones dentro de un asistente de pruebas, asegurando la adherencia rigurosa a las definiciones algebraicas encontradas en la literatura.

Los autores declaran explícitamente que el código correspondiente está disponible públicamente para apoyar desarrollos posteriores en la formalización de estructuras geométricas avanzadas. No pretenden haber resuelto problemas abiertos en geometría algebraica, sino que han logrado traducir teorías complejas existentes a un formato verificado por máquina.