Full iff H¹ = 0

Proved

WeatherallGauge.full_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 full iff every 1-cochain $A$ with $\delta^1A=0$ is $\delta^0\lambda$ for some $\lambda$ .

Preamble

import Mathlib
import Definitions.Def_WeatherallGauge_defs

open CategoryTheory

Formal statement

namespace WeatherallGauge

/-- The functor `A ↦ δA` on potentials with gauge arrows is full iff `H¹(X;K) = 0`. -/
theorem full_iff (X : CellComplex2) (K : Type) [AddCommGroup K] :
    fieldStrength (X := X) (K := K).Full ↔ H1Vanishes 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) and p. 4, fn. 9 (topology set aside), 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 full if and only if for every $A\in C^1(X;K)$ with $\delta^1A=0$ there exists $\lambda\in C^0(X;K)$ with $\delta^0\lambda=A$ .

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