Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2609.20127

Retro-synthetic Riemannian geometry in Rocq I : Taylor series of a metric

Gabriella Clemente·Hugo Herbelin·Carlos Simpson
View original source ↗Read source document ↗Export metadata ↓

Abstract

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 techniques lead to a synthetic Taylor formula for a Riemannian metric in normal coordinates, which is the main contribution of this work.

Explore related subjects

math.DGcs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Gabriella Clemente, Hugo Herbelin, Carlos Simpson. 2026-09-17. Retro-synthetic Riemannian geometry in Rocq I : Taylor series of a metric. https://arxiv.org/abs/2609.20127

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Futaki invariant on Hopf manifolds

The Futaki invariant is a fundamental tool in Kähler geometry representing an obstruction to the existence of Kähler-Einstein metrics. Recently, it was generalized to compact complex manifolds. In this paper, we prove that it vanishes on Hopf manifolds.

math.DG↗
arXiv2026

Remarks on potential functions of noncompact quasi-Einstein manifolds

In this article, we study the set of potential functions on noncompact quasi-Einstein manifolds. We show that the space of all positive potential functions on a three-dimensional noncompact quasi-Einstein manifold has dimension at most two, and that equality holds if and only if the manifold is isometric to a product $B\times\mathbb{R}$, where $B$ is a $λ$-Einstein surface or one of the examples obtained by L. Berard Bergery and described in Besse's book. Moreover, we prove that any asymptotically flat $n$-dimensional quasi-Einstein manifold with $λ=0$ is necessarily Ricci-flat.

math.DG↗
arXiv2026

Adjusted connections on non-abelian bundle gerbes

Higher gauge theory for non-abelian structure 2-groups faces significant challenges when extending beyond the fake-flat sector, which suffers from limited applicability in physical models. A promising resolution involves equipping 2-groups with additional structure, known as adjustments. We present a comprehensive theory of adjusted connections on non-abelian bundle gerbes, classified by Saemann's adjusted version of non-abelian differential cohomology. This theory enables, in particular, a new coordinate-independent formulation of Tellez-Dominguez' lifting theorem, establishing a correspondence between adjusted connections on non-abelian bundle gerbes and connections on abelian bundle 2-gerbes.

math.DG↗