Why would a spinor transform under Lorentz transformations?

From my understanding of spinors, they arise as projective representations of $SO_0(1,3)$ that do not correspond to representations of $SO_0(1,3)$.
But still one says here – and virtually everywhere – that the Dirac equation is Lorentz invariant and even gives an explicit “representation” for the Lorentz group acting on it.
In my head, I am telling myself, that I should read the action as being one of $Spin(1,3)$ instead. Then, fixing a covering map $rho : Spin(1,3) to SO_0(1,3)$, I can push any $s in Spin(1,3)$ down to a $Lambda simeq rho(s) in SO_0(1,3)$ telling me how to transform the derivatives appearing in the Dirac equation. But then, in the parlance of the linked question, $U(Lambda)$ would have to be multi-valued – or one would have to choose one of many possible values for $U(Lambda)$.
Of course different choices of $U(Lambda)$ can only differ by a complex phase $exp(i phi)$ for some $phi in mathbb{R}$, which is why I have the feeling that this is intimately connected with the $U(1)$ gauge invariance of QED:
Because we can at least locally around a point $x$ choose a $phi(y)$ for every $y$ in some neighbourhood of $x$, the Dirac equation can only ever become Lorentz i.e $SO_0(1,3)$-invariant if we promote it to an equation that is also locally $U(1)$ invariant which leads to QED in the familiar way.

From these thoughts, I conclude that the Dirac equation is not Lorentz invariant but rather it is $Spin(1,3)$-invariant. It becomes Lorentz invariant only when it is extended to something making it locally $U(1)$ invariant e.g QED.

Am I off track or on the spot here? I have failed to find anything written on this topic :/