The gauge-orbit functor forgets only stuff
ProvedGaugeFunctor.orbitF_forgets_only_stuffSetting: 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 .
Let send each connection to its gauge orbit, where is the discrete category (identity arrows only) on the set of gauge orbits.
Statement. For every finite graph (connected or not) and every group , is full and essentially surjective, and it is faithful if and only if has no vertices or is trivial.
import Mathlib import Definitions.Def_GaugeFunctor_defs open CategoryTheory
namespace GaugeFunctor
/-- The functor from connections-with-gauge-arrows to gauge orbits is full and essentially
surjective, and it is faithful exactly when the graph has no vertices or the gauge group is
trivial; otherwise it forgets only stuff (the global gauge transformations). -/
theorem orbitF_forgets_only_stuff (X : Graph) (G : Type) [Group G] :
(orbitF X G).Full ∧ (orbitF X G).EssSurj ∧
((orbitF X G).Faithful ↔ (IsEmpty (Fin X.nV) ∨ Subsingleton G)) := by sorry
end GaugeFunctorRead-back
What the Lean code literally says, in plain math · claude-opus-5-5
For every graph and group (no connectivity and no nontriviality assumed):
- is full: whenever there is a gauge arrow .
- is essentially surjective: every gauge class is for some .
- is faithful iff ( has no vertices, or has at most one element). Faithfulness here means: for all there is at most one with .
Notes: plausibly true. If and in , the constant gauge transformation and both fix , so faithfulness fails; conversely, with or trivial there is only one gauge transformation. Parts 1 and 2 are essentially definitional (low difficulty). Docstring matches.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.