2 citations · 4 across the 14 of their papers we have counts for
4 papers · 1 filter
Retro-synthetic Riemannian geometry in Rocq I : Taylor series of a metric
Gabriella Clemente, Hugo Herbelin, Carlos Simpson
We introduce a synthetic framework for doing local Riemannian geometry that is influenced by a reverse-engineering method for formalizing in Rocq. These new perspectives and techni…
Differential Homology
Fabio Ferrari Ruffino, Gabriel Longatto Clemente
We first construct the differential refinement of singular homology, verifying that it satisfies the axioms dual to their cohomological counterparts. Then, we define the differenti…
Kähler thresholds
Gabriella Clemente, Carlos Simpson
The topology of Kähler manifolds is largely determined by the geometry due to its rigidity. In particular, the cohomology and Hodge theory of compact Kähler manifolds is quite rest…
Synthetic Differential Geometry in Lean
Riccardo Brasca, Gabriella Clemente
This article is about the formalization of synthetic differential geometry with the Lean proof assistant and the mathematical library mathlib. The main result we prove and formaliz…