Derivation of the quantum electrodynamics Lagrangian Updated +Created
Like the rest of the Standard Model Lagrangian, this can be split into two parts:
Video 1.
Deriving the qED Lagrangian by Dietterich Labs (2018)
Source.
As mentioned at the start of the video, he starts with the Dirac equation Lagrangian derived in a previous video. It has nothing to do with electromagnetism specifically.
He notes that that Dirac Lagrangian, besides being globally Lorentz invariant, it also also has a global invariance.
However, it does not have a local invariance if the transformation depends on the point in spacetime.
He doesn't mention it, but I think this is highly desirable, because in general local symmetries of the Lagrangian imply conserved currents, and in this case we want conservation of charges.
To fix that, he adds an extra gauge field (a field of matrices) to the regular derivative, and the resulting derivative has a fancy name: the covariant derivative.
Then finally he notes that this gauge field he had to add has to transform exactly like the electromagnetic four-potential!
So he uses that as the gauge, and also adds in the Maxwell Lagrangian in the same go. It is kind of a guess, but it is a natural guess, and it turns out to be correct.
Lorentz gauge condition Updated +Created
There are several choices of electromagnetic four-potential that lead to the same physics.
E.g. thinking about the electric potential alone, you could set the zero anywhere, and everything would remain be the same.
The Lorentz gauge is just one such choice. It is however a very popular one, because it is also manifestly Lorentz invariant.