Cohomological classification of the field-strength functor

Proved

WeatherallGauge.classification

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$ . For every $X$ and $K$ : PotG $\to$ Fld is faithful iff $H^0=0$ , full iff $H^1=0$ , and essentially surjective iff $H^2=0$ , with $H^i=0$ in the elementary forms of the definitions.

Preamble

import Mathlib
import Definitions.Def_WeatherallGauge_defs

open CategoryTheory

Formal statement

namespace WeatherallGauge

/-- Main goal. For the field-strength functor `A ↦ δA` from potentials with gauge arrows to
field strengths on a finite 2-complex `X` with coefficients `K`: it is faithful iff `H⁰ = 0`,
full iff `H¹ = 0`, and essentially surjective iff `H² = 0`. -/
theorem classification (X : CellComplex2) (K : Type) [AddCommGroup K] :
    (fieldStrength (X := X) (K := K).Faithful ↔ H0Vanishes X K) ∧ (fieldStrength (X := X) (K := K).Full ↔ H1Vanishes X K) ∧
    (fieldStrength (X := X) (K := K).EssSurj ↔ H2Vanishes 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), §3 p. 7 and §4 pp. 8–11 (Proposition 1, fn. 9, fn. 15; Proposition 2 as corrected by the erratum, p. 15), discrete analogue

Read-back

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

For every cell complex $X$ and abelian group $K$ , all three hold: (1) $\mathrm{fieldStrength}$ is faithful iff $\delta^0\lambda=0\Rightarrow\lambda=0$ for all $\lambda\in C^0$ ; (2) it is full iff every $A\in C^1$ with $\delta^1A=0$ equals $\delta^0\lambda$ for some $\lambda\in C^0$ ; (3) it is essentially surjective iff every $F\in C^2$ equals $\delta^1A$ for some $A\in C^1$ . There are no further hypotheses; $n_V,n_E,n_P=0$ and $K=0$ are included.

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