Examples of "gauging a global symmetry" I am looking for someone to exemplify the actual process of "gauging a global symmetry." I am familiar with gauge bosons, gauge theories (QED), and the definition of "gauging a symmetry" etc., but I haven't seen an actual example of someone literally doing this and calling the process as such, which I think would be valuable given how often the phrase is employed.
Preferably an answer to this would not be a fully general exposition on the notion of gauge symmetries, but instead just a short sketch of gauging a particular global symmetry. It might be helpful to gauge a symmetry both in a classical and in a quantum field theory. Gauging a higher-form symmetry would also be very helpful. Thank you!
 A: Here is a simple example, one of the first you should try to understand. The theory has a free $U(1)$ scalar field $\phi$ in $d+1$ spacetime dimensions, discussed in the modern notation of differential forms. The Lagrangian density
$$L_0 = d\phi \wedge\star d\phi.$$
This has a manifest global symmetry $\phi \mapsto \phi + \theta$. If we perform a local variation where $\theta$ has a small first derivative, then the Lagrangian is not invariant, instead, up to boundary terms
$$\delta L_0 = 2 \theta d\star d\phi + \mathcal{O}(\theta^2) = \theta\ dj + \mathcal{O}(\theta^2),$$
where we identify the Noether current $d$-form $j = \star d \phi$. The conservation law
$$dj = 2 d\star d\phi = 0$$
is equivalent to the equations of motion. To gauge this symmetry, we couple to a $U(1)$ gauge field $A$. Minimal coupling is
$$L_0 - A \wedge j = L_0 - 2 A \star d\phi.$$
This action is not yet gauge invariant, but we're allowed to add local terms possibly depending on $\phi$ and at least secord order in $A$. We're missing a term like $A \wedge \star A$. If we put it all together we get
$$(d\phi - A) \wedge \star (d\phi - A).$$
You can check that this is a trivial theory (!). Note that this step we have only coupled to a background gauge field. If we want to integrate over $A$ also, we need to choose some measure. This last step, which is what is usually called gauging, is not canonical, but typically we use a Gaussian (Maxwell) measure for $A$ and it's alright. We still get a trivial theory: $\phi$ acts as the phase of a Higgs field for $A$.
However, if instead the symmetry was $\phi \mapsto \phi + 2\theta$, we would end up with $j = 4 \star d\phi$ and a gauged Lagrangian
$$(d\phi - 2A) \wedge \star (d\phi - 2A),$$
which you can check is a nontrivial TQFT. It's the $\mathbb{Z}_2$ gauge theory. You can see this theory has a $\mathbb{Z}_2$ 1-form symmetry which if you gauge takes you back to the trivial theory above.
PS. Very happy to see the interest in higher symmetries :)
