5 papers
A Prime-Generated Formalization of Nagata's Factoriality Theorem in Lean 4
Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira
We present a Lean 4 Mathlib formalization of Nagata's factoriality theorem: if R is a noetherian domain and S <= R is a prime-generated submonoid such that S^{-1}R is a UFD, then R…
The Seifert-van Kampen Theorem via Computational Paths: A Formalized Approach to Computing Fundamental Groups
Arthur F. Ramos, Tiago M. L. de Veras, Ruy J. G. B. de Queiroz +1
The Seifert-van Kampen theorem computes the fundamental group of a space from the fundamental groups of its constituents. We develop a modular SVK framework within the setting of c…
Computational Paths Form a Weak Ï-Groupoid
Arthur F. Ramos, Tiago M. L. de Veras, Ruy J. G. B. de Queiroz +1
Lumsdaine (2010) and van den Berg-Garner (2011) proved that types in Martin-Löf type theory carry the structure of weak Ï-groupoids. Their proofs, while foundational, rely on abs…
Formalizing Computational Paths and Fundamental Groups in Lean
Arthur F. Ramos, Anjolina G. de Oliveira, Ruy J. G. B. de Queiroz +1
Computational paths treat propositional equality as explicit paths built from labelled deduction steps and rewrite rules. This view originates in work by de Queiroz and collaborato…
Solving Homotopy Domain Equations
Daniel O. MartÃnez-Rivillas, Ruy J. G. B. de Queiroz
In order to get -models with a rich structure of -groupoid, which we call "homotopy -models", a general technique is described for solving domain equations on any c…