Gauge theory and the geometry of physics

Lens

MotivationH

Forces as curvature

In 1959 Yakir Aharonov and David Bohm proposed an experiment. Send electrons around both sides of a long, thin, perfectly shielded solenoid and let the two beams interfere. Outside the solenoid the magnetic field is zero; classically the electrons feel no force. Yet the interference pattern shifts by an amount proportional to the magnetic flux trapped inside — a flux the electrons never touch. The effect was confirmed decisively by Akira Tonomura and collaborators at Hitachi in 1986, with the solenoid's field sealed inside a superconductor.

What the electrons feel is not the field but the holonomy of a connection: the phase acquired by parallel transport around a loop. The magnetic field is the curvature of that connection, and curvature is holonomy around infinitesimal loops; where the curvature vanishes, holonomy around a large loop can still be non-trivial if the loop encircles a hole. This is the geometry of gauge theory, in which every fundamental force of the Standard Model is described by a connection on a principal bundle and its field strength by curvature.

The same mathematics turned out to be a powerful tool in pure mathematics. In 1983 Simon Donaldson used the moduli spaces of solutions of the Yang–Mills equations — instantons — to prove that many topological 4-manifolds admit no smooth structure, and, combined with Michael Freedman's work, that $\R^4$ carries exotic smooth structures, a phenomenon that occurs in no other dimension. And the quantum version of the theory contains one of the Millennium Problems: to construct quantum Yang–Mills theory rigorously and prove that it has a mass gap.

IntuitionH

Comparing phases at different points

A quantum particle carries an internal phase, a point of $U(1)$ , or for the weak and strong forces an internal frame acted on by $SU(2)$ or $SU(3)$ . There is no canonical way to compare internal frames at different points: one needs a rule of parallel transport. That rule is a connection.

The lattice picture of Kenneth Wilson (1974) makes this concrete. Place the particle on a grid. On each oriented edge from $x$ to $y$ put a group element $U_{xy} \in G$ — the transporter — with $U_{yx} = U_{xy}^{-1}$ . Transport along a path is the product of the transporters on its edges. A gauge transformation is an independent change of frame $g(x) \in G$ at every vertex, under which $U_{xy} \mapsto g(x) U_{xy} g(y)^{-1}$ . Physical quantities must not depend on the arbitrary choice of frames, so they must be gauge invariant.

What is invariant? Transport around a closed loop based at $x$ changes only by conjugation, $g(x) \cdot \mathrm{hol} \cdot g(x)^{-1}$ , so its trace — the Wilson loop — is invariant, and for the abelian group $U(1)$ the holonomy itself is. Around the smallest loop, one square (a plaquette), the holonomy measures the field strength through that square: it is the lattice curvature.

Wilson's lattice gauge field. Each edge carries a transporter U in the gauge group; transport around a square (the plaquette, in gold) is the lattice curvature. A gauge transformation g at each vertex changes every U, but the trace of the transport around any closed loop is unchanged.

The continuum theory is the limit in which the transporter along a short edge $v$ is $U \approx 1 - A(v)$ for a Lie-algebra-valued $1$ -form $A$ , the gauge potential, and the plaquette around the square spanned by $\varepsilon v, \varepsilon w$ is $1 - \varepsilon^2 F(v, w) + O(\varepsilon^3)$ (with suitable sign conventions), where $F = dA + A \wedge A$ is the curvature or field strength.

Analogy, not a formal construction

Carry a compass needle around a triangle on the Earth's surface, always keeping it "parallel" to itself: it comes back rotated by an angle equal to the enclosed curvature (the spherical excess). Gauge fields do the same to internal phases instead of tangent vectors. The analogy is close — the Levi-Civita connection is a connection on the frame bundle — but it is still an analogy: in gauge theory the bundle is an independent, internal one, and the connection is a dynamical field rather than determined by a metric.

DefinitionsH

Definitions

We assume vector bundles and characteristic classes, Lie groups, differential forms and, for the physics, quantum mechanics. Let $G$ be a compact Lie group (think $U(1)$ , $SU(2)$ , $SU(3)$ ), realised as a matrix group with Lie algebra $\mathfrak{g}$ .

Definition— principal bundle

A principal $G$ -bundle is a smooth map $\pi : P \to M$ with a smooth right action of $G$ on $P$ that is free and preserves fibres, which is locally trivial: every point of $M$ has a neighbourhood $U$ with a diffeomorphism $\pi^{-1}(U) \cong U \times G$ commuting with the projections and turning the action into right multiplication on $G$ . So $G$ acts simply transitively on each fibre. Local sections $s_\alpha : U_\alpha \to P$ give trivialisations, related by transition functions $g_{\alpha\beta} : U_\alpha \cap U_\beta \to G$ with $s_\beta = s_\alpha g_{\alpha\beta}$ . A representation $G \to GL(V)$ gives an associated vector bundle $P \times_G V$ , whose sections are the matter fields.

Definition— connection, gauge potential and gauge transformation

A connection on $P$ is a $\mathfrak{g}$ -valued $1$ -form $\omega$ on $P$ that restricts to the Maurer–Cartan form on each fibre and is equivariant, $R_g^*\omega = \operatorname{Ad}(g^{-1})\omega$ ; equivalently, a $G$ -invariant choice of horizontal subspaces $\ker\omega$ complementary to the fibres. In a local section $s$ it is described by the gauge potential $A = s^*\omega$ , a $\mathfrak{g}$ -valued $1$ -form on $U$ , and the covariant derivative of a matter field is $\nabla \psi = d\psi + A\psi$ . A change of section $s' = s g$ , with $g : U \to G$ , is a gauge transformation:

A' = g^{-1} A g + g^{-1} dg, \qquad \psi' = g^{-1}\psi .

Definition— curvature and holonomy

The curvature of $\omega$ is $\Omega = d\omega + \frac12[\omega \wedge \omega]$ ; locally it is the $\mathfrak{g}$ -valued $2$ -form

F_A = dA + A \wedge A .

The connection is flat if $F_A = 0$ . Parallel transport along a loop $\gamma$ based at $x$ gives the holonomy $\operatorname{hol}_\gamma(A) \in G$ , well defined up to conjugation (the choice of frame at $x$ ).

Definition— Yang–Mills functional and equations

On a compact oriented Riemannian manifold $M$ , with the $\operatorname{Ad}$ -invariant inner product $\langle X, Y \rangle = -\operatorname{tr}(XY)$ on $\mathfrak{g}$ and the Hodge star $\star$ , the Yang–Mills functional is

\mathrm{YM}(A) = \int_M |F_A|^2 \, d\mathrm{vol} = -\int_M \operatorname{tr}(F_A \wedge \star F_A).

Its Euler–Lagrange equations are the Yang–Mills equations $d_A {\star} F_A = 0$ , where $d_A \beta = d\beta + A \wedge \beta - (-1)^k \beta \wedge A$ on $\mathfrak{g}$ -valued $k$ -forms.

Definition— instanton and topological charge

On an oriented Riemannian $4$ -manifold, $\star$ maps $2$ -forms to $2$ -forms with $\star^2 = 1$ , so $\Lambda^2 = \Lambda^+ \oplus \Lambda^-$ splits into self-dual and anti-self-dual forms. A connection is an instanton (anti-self-dual, ASD) if $F_A = -\star F_A$ . For an $SU(2)$ -bundle $E$ over a closed oriented $4$ -manifold, the topological charge is the characteristic number

k = c_2(E)[M] = \frac{1}{8\pi^2} \int_M \operatorname{tr}(F_A \wedge F_A),

which by Chern–Weil theory is an integer independent of $A$ .

Worked examplesH

Examples

Example— Electromagnetism is a U(1) gauge theory

For $G = U(1)$ , $\mathfrak{g} = i\R$ and $A = -i\,\frac{q}{\hbar}\,a$ for a real $1$ -form $a$ , the electromagnetic potential, so that $\nabla = d - i\frac{q}{\hbar} a$ for a particle of charge $q$ . Gauge transformations $g = e^{-iq\lambda/\hbar}$ act by $a \mapsto a + d\lambda$ (and $\psi \mapsto e^{iq\lambda/\hbar}\psi$ ), and the curvature is the real $2$ -form $F = da$ (times $-iq/\hbar$ ). In space-time with coordinates $(t, x, y, z)$ and units $c = 1$ , write

a = a_x\, dx + a_y\, dy + a_z\, dz - \varphi\, dt, \qquad F = da = B_x\, dy\wedge dz + B_y\, dz \wedge dx + B_z\, dx \wedge dy + (E_x\, dx + E_y\, dy + E_z\, dz) \wedge dt .

Comparing coefficients gives $B = \operatorname{curl}\vec a$ and $E = -\nabla\varphi - \partial_t \vec a$ , where $\vec a = (a_x, a_y, a_z)$ is the vector potential and $\varphi$ the electric potential. The identity $dF = 0$ has two kinds of components: the coefficient of $dx \wedge dy \wedge dz$ is $\operatorname{div} B$ , and the coefficient of $dy \wedge dz \wedge dt$ is $\partial_t B_x + (\operatorname{curl} E)_x$ (and cyclically). So $dF = 0$ is exactly the pair of homogeneous Maxwell equations

\operatorname{div} B = 0, \qquad \partial_t B + \operatorname{curl} E = 0 .

The other pair needs the Minkowski metric: with the Lorentzian Hodge star and the current $3$ -form $J$ (charge density $\rho$ and current $j$ ), $d{\star}F = J$ encodes Gauss's law $\operatorname{div} E = \rho$ and the Ampère–Maxwell law $\operatorname{curl} B - \partial_t E = j$ (up to sign conventions for $\star$ ). Applying $d$ to it gives $dJ = 0$ : charge conservation is a consequence of the field equations. Maxwell's four equations become two.

Example— The Dirac monopole and charge quantisation

Cover $S^2$ by the two hemispheres $U_N$ , $U_S$ , overlapping near the equator, and glue trivial $U(1)$ -bundles by the transition function $e^{in\phi}$ , $n \in \Z$ . A connection is a pair of real potentials $a_N$ , $a_S$ with $a_N - a_S = n\, d\phi$ on the overlap, and the curvature $F = da_N = da_S$ is a global $2$ -form. By Stokes,

\int_{S^2} F = \oint_{\text{equator}} a_N - \oint_{\text{equator}} a_S = \oint n\, d\phi = 2\pi n ,

so $\frac{1}{2\pi}\int_{S^2} F = n$ is the first Chern number of the bundle, an integer that no choice of connection can change. Physically, a magnetic monopole of total flux $\Phi_m$ can coexist with a particle of charge $q$ only if $q\Phi_m \in 2\pi\hbar\,\Z$ (Dirac, 1931): if a single monopole exists anywhere, electric charge is quantised. The case $n = 1$ is the Hopf bundle $S^3 \to S^2$ .

Example— The Aharonov–Bohm solenoid: a flat connection with holonomy

Outside an infinitely long solenoid of flux $\Phi$ along the $z$ -axis, the potential can be taken to be $a = \frac{\Phi}{2\pi}\, d\theta$ on $\R^2 \setminus \{0\}$ (times the $z$ -direction). Then $F = da = 0$ there: no magnetic field. But for a loop $\gamma$ winding $w$ times around the solenoid,

\operatorname{hol}_\gamma = \exp\Big(\frac{iq}{\hbar}\oint_\gamma a\Big) = \exp\Big(\frac{iq}{\hbar}\, w\,\Phi\Big).

Two electron paths on either side of the solenoid differ by a loop of winding number one, so their phases differ by $q\Phi/\hbar$ , which shifts the interference fringes. The shift is invisible exactly when $q\Phi/\hbar \in 2\pi\Z$ — whence the flux quantum $h/q$ for a charge $q$ . Theorem 5 below shows that the holonomy is the only gauge-invariant information in a flat connection on the punctured plane.

Example— The BPST instanton

Identify $\R^4$ with the quaternions $\mathbb{H}$ and $\mathfrak{su}(2)$ with the imaginary quaternions. Belavin, Polyakov, Schwarz and Tyupkin (1975) found the $SU(2)$ connection

A = \operatorname{Im}\Big( \frac{\bar x\, dx}{1 + |x|^2} \Big), \qquad F_A = \frac{d\bar x \wedge dx}{(1 + |x|^2)^2},

whose curvature is (anti-)self-dual, depending on the orientation convention, with $\frac{1}{8\pi^2}\int |F_A|^2 = 1$ . Its energy density is concentrated in a ball of radius $1$ ; rescaling $x \mapsto x/\lambda$ and translating give a $5$ -parameter family of charge-one instantons, which extends to $S^4 = \R^4 \cup \{\infty\}$ . The Atiyah–Drinfeld–Hitchin–Manin construction (1978) describes all instantons on $S^4$ by linear algebra.

Example— Lattice gauge fields

On the lattice $\Z^2$ a $U(1)$ gauge field is a phase $e^{i a_e}$ on each edge; its curvature is the plaquette angle $\theta_p = a_1 + a_2 - a_3 - a_4$ around each square (reduced to $(-\pi, \pi]$ ). On a periodic $N \times N$ lattice — a discrete torus — the reduced angles add up to $2\pi Q$ with $Q \in \Z$ , a lattice version of the first Chern number; the first experiment computes it. In Wilson's lattice formulation of quantum chromodynamics the link variables are $SU(3)$ matrices and the action is a sum over plaquettes of $1 - \frac13\operatorname{Re}\operatorname{tr} U_p$ .

ProofH

Curvature, the Yang–Mills equations and the instanton bound

Theorem— Proposition 1 — curvature transforms by conjugation

If $A' = g^{-1}Ag + g^{-1}dg$ , then $F_{A'} = g^{-1} F_A\, g$ . Consequently $\operatorname{tr}(F_A \wedge F_A)$ , $\operatorname{tr}(F_A \wedge \star F_A)$ and $|F_A|^2$ are gauge invariant; for $G = U(1)$ , $F_A$ itself is.

Proof

Use $d(g^{-1}) = -g^{-1}\, dg\, g^{-1}$ and the graded Leibniz rule $d(\alpha\beta) = d\alpha\, \beta - \alpha\, d\beta$ for a matrix of $1$ -forms $\alpha$ :

dA' = -g^{-1}dg\, g^{-1} \wedge A g + g^{-1}\, dA\, g - g^{-1}A \wedge dg - g^{-1}dg\, g^{-1} \wedge dg ,

A' \wedge A' = g^{-1}A\wedge A\, g + g^{-1}A \wedge dg + g^{-1}dg\, g^{-1} \wedge A g + g^{-1}dg\, g^{-1} \wedge dg .

Adding, every term containing $dg$ cancels against one in the other line (first with third, third with second, fourth with fourth), leaving $F_{A'} = g^{-1}(dA + A \wedge A)g$ . The invariance statements follow from $\operatorname{tr}(g^{-1}Xg\, g^{-1}Yg) = \operatorname{tr}(XY)$ .

∎

Theorem— Proposition 2 — the Bianchi identity

$d_A F_A = dF_A + A \wedge F_A - F_A \wedge A = 0$ . For $G = U(1)$ this is $dF = 0$ .

Proof

$dF_A = d(dA) + d(A \wedge A) = dA \wedge A - A \wedge dA$ . On the other hand $A \wedge F_A - F_A \wedge A = A \wedge dA + A\wedge A\wedge A - dA \wedge A - A\wedge A\wedge A = A \wedge dA - dA \wedge A$ . The two cancel.

∎

Theorem— Theorem 3 — the Yang–Mills equations

$A$ is a critical point of $\mathrm{YM}$ (for compactly supported variations) if and only if $d_A^* F_A = 0$ , equivalently $d_A{\star}F_A = 0$ . Every instanton solves the Yang–Mills equations.

Proof

For a $\mathfrak{g}$ -valued $1$ -form $\alpha$ , $F_{A + t\alpha} = F_A + t\, d_A\alpha + t^2\, \alpha \wedge \alpha$ . Hence

\frac{d}{dt}\Big|_{t=0} \mathrm{YM}(A + t\alpha) = 2\int_M \langle d_A\alpha, F_A\rangle\, d\mathrm{vol} = 2\int_M \langle \alpha, d_A^* F_A\rangle\, d\mathrm{vol},

which vanishes for all $\alpha$ iff $d_A^* F_A = 0$ . On $2$ -forms $d_A^* = \pm\star d_A \star$ , so this is $d_A{\star}F_A = 0$ . If $F_A = -\star F_A$ , then $d_A{\star}F_A = -d_A F_A = 0$ by the Bianchi identity.

∎

Theorem— Theorem 4 — the instanton bound

Let $A$ be a connection on an $SU(2)$ -bundle $E$ over a closed oriented Riemannian $4$ -manifold, with $k = c_2(E)[M]$ . Then

\mathrm{YM}(A) \ \ge\ 8\pi^2 |k|,

with equality if and only if $A$ is anti-self-dual (when $k \gt 0$ ) or self-dual (when $k \lt 0$ ); for $k = 0$ , equality means $A$ is flat. Instantons minimise the Yang–Mills energy in their topological class.

Proof

Split $F = F^+ + F^-$ with $\star F^\pm = \pm F^\pm$ . The spaces $\Lambda^+$ and $\Lambda^-$ are orthogonal, so $|F|^2 = |F^+|^2 + |F^-|^2$ , and $\alpha \wedge \beta = \langle \alpha, \star\beta \rangle\,d\mathrm{vol}$ shows $\Lambda^+ \wedge \Lambda^- = 0$ . With $|X|^2 d\mathrm{vol} = -\operatorname{tr}(X \wedge \star X)$ ,

\operatorname{tr}(F \wedge F) = \operatorname{tr}(F^+\wedge F^+) + \operatorname{tr}(F^- \wedge F^-) = \big(-|F^+|^2 + |F^-|^2\big)\, d\mathrm{vol}.

By Chern–Weil, $8\pi^2 k = \int (|F^-|^2 - |F^+|^2)$ , while $\mathrm{YM}(A) = \int (|F^+|^2 + |F^-|^2)$ . Hence $\mathrm{YM}(A) \ge |8\pi^2 k|$ , with equality iff $F^+ = 0$ or $F^- = 0$ everywhere, matching the sign of $k$ .

∎

The pointwise inequality $|F \wedge F| \le |F|^2$ with its equality cases is formalised below; Chern–Weil theory, which turns the integral into the integer $k$ , is not.

Theorem— Theorem 5 — flat U(1) connections on the punctured plane

Let $M = \R^2 \setminus \{0\}$ and consider $U(1)$ connections $\nabla = d - i\frac{q}{\hbar}a$ on the trivial bundle. Gauge-equivalence classes of flat connections are in bijection with $U(1)$ , via the holonomy $e^{iq\Phi/\hbar}$ around the unit circle, $\Phi = \oint_{S^1} a$ . More generally, on a connected manifold $M$ , flat connections on principal $G$ -bundles, up to isomorphism, correspond to $\operatorname{Hom}(\pi_1(M), G)/G$ (homomorphisms up to conjugation), via holonomy.

Proof

Flatness means $da = 0$ . By de Rham's theorem for the punctured plane, $H^1_{dR}(M) \cong \R$ via $[a] \mapsto \oint_{S^1} a$ , so $a = \frac{\Phi}{2\pi}d\theta + df$ for a smooth function $f$ (see differential forms). The gauge transformation $g = e^{iqf/\hbar}$ changes $a$ by $-df$ and so removes it. A general gauge transformation $g : M \to U(1)$ changes $a$ by $-\frac{\hbar}{q}\cdot\frac{1}{i}g^{-1}dg$ , and $\frac{1}{i}g^{-1}dg$ is a closed real $1$ -form with period $2\pi n$ around the circle, $n$ the winding number of $g$ ; conversely $g = e^{-in\theta}$ shifts $a$ by $\frac{\hbar}{q}\, n\, d\theta$ . So $\frac{\Phi}{2\pi}d\theta$ and $\frac{\Phi'}{2\pi}d\theta$ are gauge equivalent iff $\frac{q}{\hbar}(\Phi - \Phi') \in 2\pi\Z$ , i.e. iff $e^{iq\Phi/\hbar} = e^{iq\Phi'/\hbar}$ . The holonomy is gauge invariant (the group is abelian) and equals $e^{iq\Phi/\hbar}$ .

∎

ExplanationH

Gauge theory and the topology of four-manifolds

Every closed oriented $4$ -manifold $M$ has an intersection form $Q_M$ on $H_2(M; \Z)/\text{torsion}$ , a unimodular symmetric bilinear form. Freedman (1982) showed that simply connected closed topological $4$ -manifolds are classified by $Q_M$ together with one $\Z/2$ -invariant, and that every unimodular form occurs. In particular there is a topological $4$ -manifold with intersection form $-E_8 \oplus -E_8$ , negative definite and not diagonalisable.

Donaldson's theorem (1983). If a smooth closed simply connected oriented $4$ -manifold has negative definite intersection form, then the form is diagonalisable over $\Z$ , i.e. isomorphic to $\langle -1 \rangle \oplus \cdots \oplus \langle -1 \rangle$ . (In 1987 Donaldson removed the hypothesis of simple connectivity.) So the topological manifold with form $-E_8 \oplus -E_8$ has no smooth structure.

The idea of the proof is a cobordism made of instantons. Take the $SU(2)$ -bundle with $c_2 = 1$ and a generic metric. The index theorem gives the dimension of the moduli space $\mathcal{M}$ of ASD connections modulo gauge as $8k - 3(1 - b_1 + b^+) = 8 - 3 = 5$ . Uhlenbeck's compactness theorem and Taubes' gluing show that one end of $\mathcal{M}$ is a collar on $M$ itself (instantons concentrating at a point of $M$ ), and $\mathcal{M}$ is a smooth $5$ -manifold except at finitely many reducible connections, one for each pair $\pm e$ of classes with $e \cdot e = -1$ , where it is a cone on $\mathbb{CP}^2$ . Cutting out the cones, $\mathcal{M}$ is an oriented cobordism between $M$ and a disjoint union of copies of $\pm\mathbb{CP}^2$ , so the signatures agree, and a lattice-theoretic argument shows the form must be diagonal.

Consequences and descendants, all theorems:

Exotic $\R^4$ . Combining Freedman's and Donaldson's results gives smooth manifolds homeomorphic but not diffeomorphic to $\R^4$ ; Taubes showed there are uncountably many. In every other dimension $\R^n$ has a unique smooth structure.
Donaldson invariants (polynomial invariants from counts of instantons) distinguish homeomorphic, non-diffeomorphic simply connected $4$ -manifolds.
Seiberg–Witten theory (1994), an abelian gauge theory with a spinor field, reproduces and extends much of Donaldson theory with far simpler analysis; Kronheimer and Mrowka used it to prove the Thom conjecture (1994).
Furuta's 10/8 theorem (2001): a smooth closed spin $4$ -manifold with indefinite intersection form satisfies $b_2 \ge \frac{10}{8}|\sigma| + 2$ ; Hopkins, Lin, Shi and Xu improved the additive constant (2018).
Low dimensions. Floer's instanton homology (1988) for $3$ -manifolds; Witten's interpretation of the Jones polynomial through Chern–Simons gauge theory (1989; see knot theory); Kronheimer and Mrowka's proofs of Property P (2004) and that Khovanov homology detects the unknot (2011). See low-dimensional topology.

ExplanationH

Physics, and what is open

The Standard Model is a quantum gauge theory with gauge group $SU(3) \times SU(2) \times U(1)$ (up to a finite quotient): $SU(3)$ for the strong force (quantum chromodynamics), $SU(2) \times U(1)$ for the electroweak force, broken to the $U(1)$ of electromagnetism by the Higgs mechanism. Its mathematical consistency at the level of perturbation theory rests on 't Hooft and Veltman's proof of renormalisability (1971–72), and the weakness of the strong force at short distances on the asymptotic freedom of Gross and Wilczek and of Politzer (1973). Lattice gauge theory makes the theory computable: Wilson (1974) showed that at strong coupling Wilson loops obey an area law $\langle W(C)\rangle \approx e^{-\sigma\,\mathrm{Area}(C)}$ , a signature of confinement, and large-scale Monte Carlo simulations now compute hadron masses from first principles — numerical evidence of great precision, not proof.

Open problems (as of the references; check recent surveys):

Yang–Mills existence and mass gap (Clay Millennium Problem, 2000): prove that for every compact simple gauge group $G$ a non-trivial quantum Yang–Mills theory exists on $\R^4$ , satisfying axioms at least as strong as those of constructive quantum field theory, and that it has a mass gap $\Delta \gt 0$ . No four-dimensional interacting quantum gauge theory has been constructed rigorously.
The smooth $4$ -dimensional Poincaré conjecture: is every smooth homotopy $4$ -sphere diffeomorphic to $S^4$ ? (Freedman proved the topological version in 1982.)
The 11/8 conjecture (Matsumoto, 1982): a smooth closed spin $4$ -manifold satisfies $b_2 \ge \frac{11}{8}|\sigma|$ . Furuta's 10/8 theorem and its improvements are the best results.

Formal mathematicsF

Gauge invariance in Lean and Mathlib

Mathlib has Lie groups and Lie algebras, smooth vector bundles and differential forms on normed spaces, but not yet principal bundles or connections. Formalised here: Wilson's lattice gauge theory, with gauge covariance proved by induction on paths and for any structure group; the gauge invariance of the electromagnetic field strength and the Bianchi identity in the continuum, using Mathlib's exterior derivative; and the pointwise algebra of Theorem 4.

The lattice: links, paths, transport and gauge transformations.

LatticeConnectionLean 4Formally verified

/-- A lattice gauge field (connection) on the square lattice `ℤ²` with structure group `G`:
`ux x` transports from `x + (1, 0)` back to `x` along the edge in the `x`-direction, and `uy x`
likewise in the `y`-direction. (Wilson, 1974.) -/
structure LatticeConnection (G : Type*) where
  /-- The link variable on the edge from `x` to `x + (1, 0)`. -/
  ux : ℤ × ℤ → G
  /-- The link variable on the edge from `x` to `x + (0, 1)`. -/
  uy : ℤ × ℤ → G

Axioms used: No axiomsformal/Lumenary/GaugeTheory.leanTry it in the Lean web editor

StepLean 4Formally verified

/-- A step of a lattice path: one unit east (`xp`), west (`xm`), north (`yp`) or south (`ym`). -/
inductive Step
  | xp
  | xm
  | yp
  | ym

Axioms used: No axiomsformal/Lumenary/GaugeTheory.leanTry it in the Lean web editor

shiftLean 4Formally verified

/-- The displacement of a step. -/
def Step.shift : Step → ℤ × ℤ
  | .xp => (1, 0)
  | .xm => (-1, 0)
  | .yp => (0, 1)
  | .ym => (0, -1)

Axioms used: No axiomsformal/Lumenary/GaugeTheory.leanTry it in the Lean web editor

transportLean 4Formally verified

/-- Parallel transport along one step from `x`: the link variable, inverted when the edge is
traversed backwards. -/
def transport (A : LatticeConnection G) (x : ℤ × ℤ) : Step → G
  | .xp => A.ux x
  | .xm => (A.ux (x + (-1, 0)))⁻¹
  | .yp => A.uy x
  | .ym => (A.uy (x + (0, -1)))⁻¹

Axioms used: propextformal/Lumenary/GaugeTheory.leanTry it in the Lean web editor

endpointLean 4Formally verified

/-- The endpoint of the path that starts at `x` and takes the given steps. -/
def endpoint (x : ℤ × ℤ) : List Step → ℤ × ℤ
  | [] => x
  | s :: ss => endpoint (x + s.shift) ss

Axioms used: No axiomsformal/Lumenary/GaugeTheory.leanTry it in the Lean web editor

holonomyLean 4Formally verified

/-- Parallel transport (holonomy) along a path: the ordered product of the step transports. For a
closed path this is the holonomy of the loop; for the boundary of one square it is the discrete
curvature (the plaquette variable). -/
def holonomy (A : LatticeConnection G) (x : ℤ × ℤ) : List Step → G
  | [] => 1
  | s :: ss => transport A x s * holonomy A (x + s.shift) ss

Axioms used: propextformal/Lumenary/GaugeTheory.leanTry it in the Lean web editor

gaugeLean 4Formally verified

/-- A gauge transformation `g : ℤ² → G` (a change of frame at every vertex) acts on link variables
by `U(x → y) ↦ g(x) U(x → y) g(y)⁻¹`. -/
def gauge (g : ℤ × ℤ → G) (A : LatticeConnection G) : LatticeConnection G where
  ux x := g x * A.ux x * (g (x + (1, 0)))⁻¹
  uy x := g x * A.uy x * (g (x + (0, 1)))⁻¹

Axioms used: propextformal/Lumenary/GaugeTheory.leanTry it in the Lean web editor

gauge_mulLean 4Proved here from basic factsFormally verified

/-- Gauge transformations form a group acting on connections: doing `h` and then `g` is the same as
doing the pointwise product `g * h`. -/
theorem gauge_mul (g h : ℤ × ℤ → G) (A : LatticeConnection G) :
    gauge g (gauge h A) = gauge (g * h) A := by
  simp only [gauge, Pi.mul_apply, mul_inv_rev]
  congr 1 <;> funext x <;> group

Axioms used: propext, Quot.soundformal/Lumenary/GaugeTheory.leanTry it in the Lean web editor

Gauge covariance of transport along one step and then along any path, and its consequences for loops:

transport_gaugeLean 4Proved here from basic factsFormally verified

/-- One step transforms covariantly: `transport (g • A) x s = g(x) · transport A x s · g(x + s)⁻¹`.
For backward steps this uses `(x - e) + e = x`. -/
theorem transport_gauge (g : ℤ × ℤ → G) (A : LatticeConnection G) (x : ℤ × ℤ) (s : Step) :
    transport (gauge g A) x s = g x * transport A x s * (g (x + s.shift))⁻¹ := by
  cases s
  · rfl
  · simp only [transport, gauge, Step.shift]
    have : x + (-1, 0) + (1, 0) = x := by ext <;> simp
    rw [this]; group
  · rfl
  · simp only [transport, gauge, Step.shift]
    have : x + (0, -1) + (0, 1) = x := by ext <;> simp
    rw [this]; group

Axioms used: propextformal/Lumenary/GaugeTheory.leanTry it in the Lean web editor

holonomy_gaugeLean 4Proved here from basic factsFormally verified

/-- **Gauge covariance of parallel transport.** Along any path from `x` to `y`, the holonomy of the
transformed connection is `g(x) · hol · g(y)⁻¹`: the gauge transformations at intermediate
vertices cancel in pairs. Proof by induction on the path. -/
theorem holonomy_gauge (g : ℤ × ℤ → G) (A : LatticeConnection G) (p : List Step) :
    ∀ x, holonomy (gauge g A) x p = g x * holonomy A x p * (g (endpoint x p))⁻¹ := by
  induction p with
  | nil => intro x; simp [holonomy, endpoint]
  | cons s ss ih =>
    intro x
    simp only [holonomy, endpoint, transport_gauge, ih]
    group

Axioms used: propextformal/Lumenary/GaugeTheory.leanTry it in the Lean web editor

holonomy_loop_conjLean 4Proved here from basic factsFormally verified

/-- The holonomy of a closed loop based at `x` changes by conjugation by `g(x)`. So only its
conjugacy class — not the group element itself — is physical in a non-abelian theory. -/
theorem holonomy_loop_conj (g : ℤ × ℤ → G) (A : LatticeConnection G) (x : ℤ × ℤ)
    (p : List Step) (hp : endpoint x p = x) :
    holonomy (gauge g A) x p = g x * holonomy A x p * (g x)⁻¹ := by
  rw [holonomy_gauge, hp]

Axioms used: propextformal/Lumenary/GaugeTheory.leanTry it in the Lean web editor

holonomy_loop_abelianLean 4Proved here from basic factsFormally verified

/-- **Abelian gauge theory (electromagnetism on a lattice).** For a commutative structure group such
as `U(1)`, the holonomy of every closed loop is gauge invariant. Around a single square it is the
lattice field strength `exp(i · flux)`; around a large loop, `exp(i · enclosed flux)`. -/
theorem holonomy_loop_abelian {G : Type*} [CommGroup G] (g : ℤ × ℤ → G)
    (A : LatticeConnection G) (x : ℤ × ℤ) (p : List Step) (hp : endpoint x p = x) :
    holonomy (gauge g A) x p = holonomy A x p := by
  rw [holonomy_gauge, hp, mul_comm (g x), mul_assoc, mul_inv_cancel, mul_one]

Axioms used: propextformal/Lumenary/GaugeTheory.leanTry it in the Lean web editor

plaquetteLean 4Proved here from basic factsFormally verified

/-- The holonomy around the unit square with corner `x` (the plaquette variable, Wilson's lattice
curvature): `U_x(x) U_y(x + e₁) U_x(x + e₂)⁻¹ U_y(x)⁻¹`. -/
theorem plaquette (A : LatticeConnection G) (x : ℤ × ℤ) :
    holonomy A x [.xp, .yp, .xm, .ym] =
      A.ux x * A.uy (x + (1, 0)) * (A.ux (x + (0, 1)))⁻¹ * (A.uy x)⁻¹ := by
  simp only [holonomy, transport, Step.shift]
  have h1 : x + (1, 0) + (0, 1) + (-1, 0) = x + (0, 1) := by ext <;> simp
  rw [h1]
  have h3 : x + (0, 1) + (0, -1) = x := by ext <;> simp
  rw [h3]
  group

Axioms used: propextformal/Lumenary/GaugeTheory.leanTry it in the Lean web editor

For matrix groups, the trace kills the conjugation, so Wilson loops are gauge invariant:

trace_conjLean 4Applies a library theoremFormally verified

/-- The trace of a matrix is invariant under conjugation by an invertible matrix,
`tr(g h g⁻¹) = tr(h)`. This applies Mathlib's `Matrix.trace_mul_cycle` (`tr(ABC) = tr(CAB)`). -/
theorem trace_conj {n : Type*} [Fintype n] [DecidableEq n] (g h : (Matrix n n ℂ)ˣ) :
    trace (↑(g * h * g⁻¹) : Matrix n n ℂ) = trace (↑h : Matrix n n ℂ) := by
  rw [Units.val_mul, Units.val_mul, Matrix.trace_mul_cycle, ← Units.val_mul, inv_mul_cancel,
    Units.val_one, Matrix.one_mul]