The holonomy functor is faithful
ProvedGaugeFunctor.holF_faithfulSetting: is a finite directed graph with vertex set , edge set and maps ; a walk may use edges in either direction, and is connected from if every vertex is reached by a walk from . is any group. A connection is ; its holonomy along a walk is the ordered product of on forward steps and on backward steps. A gauge transformation acts by . is the category whose objects are connections and whose arrows are gauge transformations with . is the category of holonomy maps at (assignments of group elements to walks, multiplicative on loops at and unchanged by inserting a backtrack into a loop at ), with arrows the elements such that for every loop at . The holonomy functor sends and .
Statement. If is connected from , then is faithful: two gauge arrows with are equal.
import Mathlib import Definitions.Def_GaugeFunctor_defs open CategoryTheory
namespace GaugeFunctor
/-- On a graph connected from `x`, a gauge transformation relating two connections is
determined by its value at `x`: the holonomy functor is faithful. -/
theorem holF_faithful (X : Graph) (G : Type) [Group G] (x : Fin X.nV)
(hX : X.Connected x) : (holF X G x).Faithful := by sorry
end GaugeFunctorRead-back
What the Lean code literally says, in plain math · claude-opus-5-5
Let be a graph, a group, a vertex with connected from . Then the holonomy functor is faithful: for any connections and gauge transformations with , if then (as functions on all vertices).
Notes: plausibly true via along a walk . Connectivity is needed (false for an isolated vertex and nontrivial ). Docstring matches.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.