I'm currently doing Introductory QFT and was confused about the origin of the additional terms in the covariant derivate. My understanding is as follows:
If we begin with the Dirac Lagrangian describing a free fermion:
\begin{equation} \require{cancel} L = \bar{\psi}(i\cancel{\partial}-m)\psi, \end{equation}
where $\bar{\psi} = \psi^{\dagger}\gamma^0$ is the anti-fermion spinor and m is their mass. I believe that we want to describe a world with massless vector bosons so we require local symmetry, meaning I want the spinors to transform as:
$$\psi (x) \rightarrow e^{i\alpha (x)} \psi (x)$$
where $e^{i\alpha (x)}$ is a representation of a unitary transformation as they describe quantum transformations. If $\alpha$ didn't depend on x, then applying the unitary transformations would allow the exponential to pass through the derivative and thus give a global symmetry, however now it does act on the exponential so we want to promote the partial derivate to another kind of derivative which leaves it invariant under unitary transformations:
$$U^{\dagger}D_{\mu}U = D_{\mu}.$$
The only form of the covariant derivative which has this property is:
$$\partial_{\mu} \rightarrow D_{\mu} = \partial_{\mu} + ieA_{\mu} (x)$$
My question is where does this particular form of $D_{\mu}$ come from and how to we derive it?