Prop. 1 analogue: without gauge arrows A ↦ δA forgets structure

Proved

WeatherallGauge.prop1_analogue

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$ . If $\delta^0\lambda\ne0$ for some $\lambda$ , the functor Pot0 $\to$ Fld is faithful, not full, and essentially surjective iff every 2-cochain is a coboundary ( $H^2=0$ ).

Preamble

import Mathlib
import Definitions.Def_WeatherallGauge_defs

open CategoryTheory

Formal statement

namespace WeatherallGauge

/-- Analogue of Weatherall (2016), Prop. 1: without gauge arrows, `A ↦ δA` is faithful, is not
full as soon as the coboundary `δ⁰` is not the zero map, and is essentially surjective iff
`H² = 0`. -/
theorem prop1_analogue (X : CellComplex2) (K : Type) [AddCommGroup K]
    (h : ∃ lam : C0 X K, delta0 lam ≠ 0) :
    (fieldStrength0 (X := X) (K := K)).Faithful ∧ ¬ (fieldStrength0 (X := X) (K := K)).Full ∧
    ((fieldStrength0 (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. 8, Proposition 1

Read-back

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

For every cell complex $X$ and abelian group $K$ , under the hypothesis that there exists $\lambda\in C^0(X;K)$ with $\delta^0\lambda\ne0$ , the functor $G\colon\mathrm{Pot0}\to\mathrm{Fld}$ , $A\mapsto\delta^1A$ , satisfies all of: (i) $G$ is faithful; (ii) $G$ is not full; (iii) $G$ is essentially surjective if and only if for every $F\in C^2$ there is $A\in C^1$ 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