Essentially surjective iff H² = 0

Proved

WeatherallGauge.essSurj_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 essentially surjective iff every 2-cochain is $\delta^1A$ for some $A$ .

Preamble

import Mathlib
import Definitions.Def_WeatherallGauge_defs

open CategoryTheory

Formal statement

namespace WeatherallGauge

/-- The functor `A ↦ δA` on potentials with gauge arrows is essentially surjective iff
`H²(X;K) = 0`. -/
theorem essSurj_iff (X : CellComplex2) (K : Type) [AddCommGroup 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), §4, p. 11, fn. 15 (EM2 with gauge arrows), 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$ , the functor $\mathrm{fieldStrength}$ is essentially surjective (every object of Fld is isomorphic, i.e. equal, to some $\delta^1A$ ) if and only if for every $F\in C^2(X;K)$ there exists $A\in C^1(X;K)$ with $\delta^1A=F$ .

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