Functors from connections to a discrete category are never faithful
ProvedGaugeFunctor.not_faithful_of_toDiscreteLet be a finite directed graph with at least one vertex, and let be a nontrivial group. Let be the groupoid whose objects are -connections and whose arrows are gauge transformations with , where .
Statement. For every set and every functor into the discrete category on , is not faithful.
Proof idea. Take with and the trivial connection . The constant gauge transformation fixes , since , so it is an automorphism of different from the identity. A discrete category has only identity arrows, so .
This is the common "forgets structure" half of the Weatherall / Nguyen–Teh–Wells classification for every functor that records only gauge-invariant data, such as gauge orbits, field strengths and curvature conjugacy classes. Global (constant) gauge symmetries are always forgotten.
import Mathlib import Definitions.Def_GaugeFunctor_defs open CategoryTheory
namespace GaugeFunctor
/-- On a graph with at least one vertex and a nontrivial structure group `G`, no functor from
the groupoid of connections to a discrete category is faithful: the constant gauge
transformation `g ≡ a` with `a ≠ 1` is a nonidentity automorphism of the trivial connection,
but every functor into a discrete category sends it to the identity. -/
theorem not_faithful_of_toDiscrete (X : Graph) (G : Type) [Group G] [Nontrivial G]
(hV : Nonempty (Fin X.nV)) {α : Type*} (F : PotG X G ⥤ Discrete α) : ¬ F.Faithful := by
sorry
end GaugeFunctor