Faithful iff H⁰ = 0 (constant gauge transformations are stuff)

Proved

WeatherallGauge.faithful_iff

by Alien60 · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

aharonov-bohmcategory-theorycochainsgauge-theoryphilosophy-of-physics

Throughout, $X$ is a finite oriented 2-complex (cells indexed by Fin, integer incidence numbers with $\partial\partial=0$ ), $K$ an additive commutative group, $\delta^0:C^0\to C^1$ , $\delta^1:C^1\to C^2$ the coboundaries; PotG has potentials as objects and gauge parameters $\lambda$ with $A+\delta^0\lambda=A'$ as arrows $A\to A'$ ; Pot0 and Fld are discrete; the functors send $A\mapsto\delta^1A$ . The functor PotG $\to$ Fld is faithful iff $\delta^0\lambda=0$ implies $\lambda=0$ .

Preamble

import Mathlib
import Definitions.Def_WeatherallGauge_defs

open CategoryTheory

Formal statement

namespace WeatherallGauge

/-- The functor `A ↦ δA` on potentials with gauge arrows is faithful iff `H⁰(X;K) = 0`. -/
theorem faithful_iff (X : CellComplex2) (K : Type) [AddCommGroup K] :
    fieldStrength (X := X) (K := K).Faithful ↔ H0Vanishes X K := by sorry

end WeatherallGauge

Source

J. O. Weatherall, Understanding Gauge, Philos. Sci. 83 (2016) 1039-1049, https://arxiv.org/abs/1505.02229 (page numbers refer to arXiv v2), §4, p. 11, fn. 15 (EM2 with gauge arrows); matches Proposition 2 as corrected by the erratum (arXiv v2, p. 15)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

For every cell complex $X$ and abelian group $K$ , the functor $\mathrm{fieldStrength}\colon\mathrm{PotG}(X,K)\to\mathrm{Fld}(X,K)$ , $A\mapsto\delta^1A$ , is faithful if and only if for every $\lambda\in C^0(X;K)$ , $\delta^0\lambda=0$ implies $\lambda=0$ .

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Alien60 · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph