Aharonov–Bohm: on a circle A ↦ δA is not full

Proved

WeatherallGauge.aharonov_bohm

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

aharonov-bohmcategory-theorycochainsgauge-theoryphilosophy-of-physics

On circle3 (three vertices, edges $e:e\to e+1$ mod 3, no faces) with $\mathbb Z$ coefficients, the potential $A=\mathbf 1_{e=0}$ satisfies $\delta^1A=\delta^1 0$ (trivially: no faces), there is no gauge arrow $A\to0$ in PotG, and the field-strength functor PotG $\to$ Fld is not full.

Preamble

import Mathlib
import Definitions.Def_WeatherallGauge_defs

open CategoryTheory

Formal statement

namespace WeatherallGauge

/-- Aharonov–Bohm on the circle `circle3` with `ℤ` coefficients: the potential that is `1` on
edge `0` has the same field strength as the zero potential (trivially, as `circle3`
has no faces), yet no gauge transformation relates
them; hence the field-strength functor is not full. -/
theorem aharonov_bohm :
    delta1 (Pi.single 0 1 : C1 circle3 ℤ) = delta1 0 ∧
    IsEmpty ((⟨Pi.single 0 1⟩ : PotG circle3 ℤ) ⟶ ⟨0⟩) ∧
    ¬ (fieldStrength (X := circle3) (K := ℤ)).Full := 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), fn. 9 (topology set aside), discrete counterexample

Read-back

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

Take $X=\mathrm{circle3}$ , $K=\mathbb Z$ , and $a\in C^1=\mathbb Z^3$ the cochain equal to $1$ at edge $0$ and $0$ at the other edges. Three things are asserted: (1) $\delta^1a=\delta^1 0$ in $C^2$ ; (2) there is no morphism in $\mathrm{PotG}$ from $a$ to $0$ , i.e. no $\lambda\in\mathbb Z^3$ with $a+\delta^0\lambda=0$ ; (3) the functor $\mathrm{fieldStrength}\colon\mathrm{PotG}(\mathrm{circle3},\mathbb Z)\to\mathrm{Fld}$ is not full.

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