Filled triangle: A ↦ δA forgets only stuff

Proved

WeatherallGauge.filledTriangle_forgets_only_stuff

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

aharonov-bohmcategory-theorycochainsgauge-theoryphilosophy-of-physics

On filledTriangle (circle3 plus one face bounded by all three edges) with $\mathbb Z$ coefficients, the functor PotG $\to$ Fld is full and essentially surjective but not faithful.

Preamble

import Mathlib
import Definitions.Def_WeatherallGauge_defs

open CategoryTheory

Formal statement

namespace WeatherallGauge

/-- On the filled triangle with `ℤ` coefficients the field-strength functor is full and
essentially surjective but not faithful: constant gauge transformations are non-trivial arrows
sent to identities (it "forgets only stuff"). -/
theorem filledTriangle_forgets_only_stuff :
    (fieldStrength (X := filledTriangle) (K := ℤ)).Full ∧
    (fieldStrength (X := filledTriangle) (K := ℤ)).EssSurj ∧
    ¬ (fieldStrength (X := filledTriangle) (K := ℤ)).Faithful := 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 (stuff/structure/property) and §4, p. 11, fn. 15, discrete example

Read-back

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

Take $X=\mathrm{filledTriangle}$ , $K=\mathbb Z$ . The functor $\mathrm{fieldStrength}\colon\mathrm{PotG}\to\mathrm{Fld}$ , $A\mapsto\delta^1A$ , is full, is essentially surjective, and is not faithful.

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