Aharonov-Bohm: curvature forgets structure on a circle
ProvedGaugeFunctor.aharonov_bohm_nonabelianSetting: 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 .
For a 2-complex (a graph with faces, each with a base vertex and a boundary loop there), the curvature functor sends a connection to the family of conjugacy classes of its holonomies around the faces, into the discrete category on such families. Let be the triangle with no faces (a circle) and the same triangle with one face bounded by the loop .
Statement. For every nontrivial group : is not full, while is full and essentially surjective but not faithful.
import Mathlib import Definitions.Def_GaugeFunctor_defs open CategoryTheory
namespace GaugeFunctor
/-- Aharonov–Bohm on a triangle, for any nontrivial group `G` (abelian or not). On the circle
(no faces) the curvature functor is not full: flat connections with different holonomy are
not gauge-equivalent. On the filled triangle it is full and essentially surjective but not
faithful, so it forgets only stuff. -/
theorem aharonov_bohm_nonabelian (G : Type) [Group G] [Nontrivial G] :
¬ (curvF G circleC).Full ∧
(curvF G filledC).Full ∧ (curvF G filledC).EssSurj ∧ ¬ (curvF G filledC).Faithful := by sorry
end GaugeFunctorRead-back
What the Lean code literally says, in plain math · claude-opus-5-5
For every group with at least two elements, all four of the following hold:
- on is not full. Since circleC has no faces, the target category has exactly one object and one arrow, so fullness would mean that every two connections on the triangle graph are gauge-equivalent. The claim is that some pair of connections on the triangle admits no with .
- on is full: whenever and are conjugate in , there is a gauge transformation with .
- on is essentially surjective: every conjugacy class of is the class of for some connection .
- on is not faithful: there exist connections and two distinct gauge transformations with .
Notes: plausibly true. (1) holds because and with have non-conjugate loop holonomies. (4) is witnessed by constant gauge transformations , , stabilising ; so the non-faithfulness part is cheap and uses no non-abelian structure. Nontriviality of is needed for (1) and (4). Despite the name, nothing requires to be non-abelian. The docstring wording ("flat connections with different holonomy") matches, since with no faces every connection is trivially flat.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.