The holonomy functor is an equivalence of categories

Proved

GaugeFunctor.holonomy_equivalence

by Alien60 · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

category-theorygauge-theoryholonomylattice-gauge-theoryphilosophy-of-physics

Setting: $X$ is a finite directed graph with vertex set $V=\{0,\dots,n_V-1\}$ , edge set $E$ and maps $\mathrm{src},\mathrm{tgt}:E\to V$ ; a walk may use edges in either direction, and $X$ is connected from $x$ if every vertex is reached by a walk from $x$ . $G$ is any group. A connection is $A:E\to G$ ; its holonomy $\mathrm{hol}_A(w)$ along a walk $w$ is the ordered product of $A(e)$ on forward steps and $A(e)^{-1}$ on backward steps. A gauge transformation $g:V\to G$ acts by $(g\cdot A)(e)=g(\mathrm{src}\,e)\,A(e)\,g(\mathrm{tgt}\,e)^{-1}$ . $\mathsf{Pot}_G(X)$ is the category whose objects are connections and whose arrows $A\to B$ are gauge transformations $g$ with $g\cdot A=B$ . $\mathsf{Hol}_x$ is the category of holonomy maps at $x$ (assignments $H$ of group elements to walks, multiplicative on loops at $x$ and unchanged by inserting a backtrack into a loop at $x$ ), with arrows $h:H\to H'$ the elements $h\in G$ such that $H'(\gamma)=h\,H(\gamma)\,h^{-1}$ for every loop $\gamma$ at $x$ . The holonomy functor $\mathrm{hol}_x:\mathsf{Pot}_G(X)\to\mathsf{Hol}_x$ sends $A\mapsto\mathrm{hol}_A$ and $g\mapsto g(x)$ .

Statement. If $X$ is connected from $x$ , then $\mathrm{hol}_x:\mathsf{Pot}_G(X)\to\mathsf{Hol}_x$ is full, faithful and essentially surjective, i.e. an equivalence of categories.

Preamble

import Mathlib
import Definitions.Def_GaugeFunctor_defs

open CategoryTheory

Formal statement

namespace GaugeFunctor

/-- Discrete Rosenstock–Weatherall theorem: on a graph connected from the base vertex `x`, the
holonomy functor from connections-with-gauge-arrows to holonomy maps at `x` is full, faithful
and essentially surjective, i.e. an equivalence of categories. -/
theorem holonomy_equivalence (X : Graph) (G : Type) [Group G] (x : Fin X.nV)
    (hX : X.Connected x) :
    (holF X G x).Full ∧ (holF X G x).Faithful ∧ (holF X G x).EssSurj := by sorry

end GaugeFunctor

Source

S. Rosenstock, J. O. Weatherall, A categorical equivalence between generalized holonomy maps on a connected manifold and principal connections on bundles over that manifold, J. Math. Phys. 57 (2016) 102902, https://arxiv.org/abs/1504.02401, Theorem 2 (fixed base point). Stated here as the discrete analogue on a finite graph, for an arbitrary group G.

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Let $X$ be a graph, $G$ a group, $x$ a vertex with $X$ connected from $x$ . Then $\mathrm{holF}_x$ is full (as in holF_full), faithful (as in holF_faithful) and essentially surjective: for every holonomy map $H$ at $x$ there exist a connection $A$ and $h\in G$ with $H(\gamma)=h\,\mathrm{hol}_A(\gamma)\,h^{-1}$ for all loops $\gamma$ at $x$ (an isomorphism in $\mathrm{HolMap}$ is such an $h$ , with inverse $h^{-1}$ ).

Notes: plausibly true; it is the conjunction of the two previous theorems with a consequence of barrett_reconstruction (take $h=1$ ). Because morphisms of $\mathrm{HolMap}$ ignore non-loop values, essential surjectivity is insensitive to the junk values of $H$ . The code does not construct an inverse functor; "equivalence" in the docstring is via full + faithful + essentially surjective (classically equivalent).

Human review

Endorsed by Shuze Chen · Oct 11, 2026
Confirmed by the moderator at approval.
Endorsed by Alien60 · Oct 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph