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

Resumo Técnico: Formalização de Esquemas Proj de Brenner-Schröer Multigradados e Dilatações de Anéis em Lean4

Enunciado do Problema
O artigo aborda a formalização de construções avançadas de geometria algébrica multigraduada no provador de teoremas Lean4. Enquanto a geometria algébrica clássica frequentemente se baseia em anéis graduados pelos números naturais ($\mathbb{N}$) ou inteiros ($\mathbb{Z}$), desenvolvimentos modernos — como na teoria de Lie, teoria de representação geométrica e o programa do modelo mínimo — exigem anéis graduados por monoides ou grupos mais gerais. Especificamente, os autores focam na construção Proj de Brenner–Schröer, que generaliza a construção Proj clássica para contextos multigradados, e na teoria de dilatações de anéis, uma operação relacionada à localização e blowups. O desafio reside em implementar essas estruturas em um framework de teoria de tipos (Lean4) onde a distinção entre um anel graduado $A$ e sua decomposição de soma direta $\bigoplus_{i \in \iota} A_i$ deve ser gerenciada rigorosamente sem sacrificar a usabilidade ergonômica.

Metodologia
Os autores adotam uma abordagem algébrica consistente com a literatura existente (especificamente seguindo o tratamento em [9]) para formalizar esses conceitos em Lean4. A metodologia envolve:

1. Configuração Geral para Estruturas Graduadas: A formalização define anéis e módulos graduados onde o monoide de graduação $\iota$ é um grupo abeliano arbitrário. Para lidar com restrições de teoria de tipos, os autores distinguem entre o anel $A$ e seus componentes graduados $A_i$, utilizando estruturas SetLike para tratar os componentes como subgrupos enquanto mantêm a capacidade de alternar entre o anel e sua decomposição de soma direta.
2. Localização Homogênea e "Poções": Uma inovação técnica central é a definição de "poções" ($\vartheta(S)$), definidas como a parte de grau zero de uma localização homogênea $A(S)$. Diferente da localização padrão, as poções não são definidas como subanéis do anel localizado, mas como quocientes de triplas $(i, a, b)$ onde $a, b$ são elementos homogêneos do mesmo grau e $b \in S$. Esta estrutura facilita a indução e o acesso a numeradores e denominadores.
3. Relevância e Ingredientes de Boas Poções: Os autores formalizam o conceito de submonioides homogêneos "relevantes", onde o subgrupo gerado pelos graus dos elementos no submonoide possui índice finito (ou quociente de torção) no grupo de graduação. Eles definem "ingredientes de boas poções" como submonioides que são tanto relevantes quanto finitamente gerados.
4. Colagem e Construção Proj: O esquema Proj é construído colando esquemas afins $\text{Spec}(\vartheta(S_i))$ associados a uma família de bons ingredientes de poções. Os dados de colagem dependem de isomorfismos entre produtos tensoriais de poções (por exemplo, $\vartheta(ST) \otimes_{\vartheta(S)} \vartheta(SR) \cong \vartheta(RST)$), que são estabelecidos via "geradores de poção".
5. Dilatações: O artigo formaliza as dilatações de anéis em relação a um multicentro (uma coleção de ideais e elementos). Isso envolve definir classes de equivalência de frações simbólicas $m/a^\nu$ e provar a propriedade universal que caracteriza as dilatações.

Principais Contribuições e Resultados
O artigo apresenta uma biblioteca abrangente de definições, lemas e teoremas em Lean4:

• Formalização de Proj Multigradado: Os autores fornecem uma implementação completa da construção Proj de Brenner–Schröer. Isso inclui a definição de localização homogênea, a teoria das poções e a colagem de esquemas afins para formar o esquema Proj.
• Geradores de Poção e Isomorfismos: Uma contribuição significativa é a formalização de "geradores de poção", que permitem aos autores provar que, para $S$ relevante e $T$ finitamente gerado, o morfismo $\text{Spec}(\vartheta(ST)) \to \text{Spec}(\vartheta(S))$ é uma imersão aberta. Eles também estabelecem as condições de cociclo necessárias para a construção de colagem.
• Functorialidade: A construção Proj é mostrada como um funtor contravariante do categoria de anéis graduados para a categoria de esquemas. Os autores abordam cuidadosamente as sutilezas de teoria de tipos onde a imagem de uma família sob um homomorfismo de anel não é definiçãomente igual à família alvo, exigindo o uso de morfismos específicos (projHomOfLE) para estabelecer a functorialidade.
• Dilatações: O artigo formaliza a definição de dilatações de anéis e prova sua propriedade universal: para qualquer homomorfismo de anel $\chi: A \to B$ onde as imagens dos elementos do centro são não-divisores de zero e geram as imagens dos ideais correspondentes, existe um único morfismo da dilatação para $B$.
• Isomorfismo de Famílias Ampliadas: Os autores provam que ampliar uma família de bons ingredientes de poções (incluindo produtos de ingredientes existentes) resulta em um esquema Proj isomórfico, garantindo a robustez da construção contra a escolha da família geradora.

Significância
O artigo reivindica significância primariamente como um passo fundamental na formalização da geometria algébrica avançada. Ele serve como:

1. Documentação: Um relato detalhado das definições, escolhas de design e principais resultados subjacentes à formalização, destinado a guiar futuros desenvolvedores.
2. Fundação: Uma biblioteca reutilizável para extensões futuras na geometria algébrica formalizada, particularmente para projetos que requerem estruturas multigradadas ou dilatações.
3. Verificação: Uma implementação totalmente formal que verifica a correção da construção de Brenner–Schröer e da teoria de dilatações dentro de um assistente de prova, garantindo a adesão rigorosa às definições algébricas encontradas na literatura.

Os autores declaram explicitamente que o código correspondente está disponível publicamente para apoiar desenvolvimentos futuros na formalização de estruturas geométricas avançadas. Eles não alegam ter resolvido problemas abertos na geometria algébrica, mas sim que conseguiram traduzir teorias complexas existentes para um formato verificado por máquina.