The holonomy functor is full
ProvedGaugeFunctor.holF_fullSetting: 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 full: whenever satisfies for every loop at , there is a gauge transformation with and .
import Mathlib import Definitions.Def_GaugeFunctor_defs open CategoryTheory
namespace GaugeFunctor
/-- On a graph connected from `x`, if `h : G` conjugates the holonomies at `x` of `A` into
those of `B`, some gauge transformation `g` with `g x = h` carries `A` to `B`: the holonomy
functor is full. -/
theorem holF_full (X : Graph) (G : Type) [Group G] (x : Fin X.nV)
(hX : X.Connected x) : (holF X G x).Full := 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 is full: for any connections and any with
there exists a gauge transformation with and .
Notes: plausibly true (apply a gauge transformation with value at , then the representation theorem). Docstring matches. Connectivity is needed (on an edge outside the component of , and could be non-conjugate, blocking existence).
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.