Below is my attempt to understand gauge redundancy:
Let's consider some starshaped region $S$ of a smooth 4-dimensional manifold $M$. The space of 1-forms I will denote $\Lambda^1(S)$. Then the equations of motion for (say) electrodynamics, are in fact nothing but a linear differential operator
$$ \Lambda^1(S)\xrightarrow{ \ D \ } \Lambda^1(S). $$
Now the interesting part is this: It seems that the physical degrees of freedom are not the 1-forms in $\Lambda^1(S)$ but rather the 1-forms in $\Lambda^1(S)/\text{Im}d_0$
$$ \Lambda^0(S)\xrightarrow{ \ d_0 \ }\Lambda^1(S)\xrightarrow{\ D \ }\Lambda^1(S). $$ Why? Because gauge redundancy means $A^\prime = A + \text{Im}d_0$, namely we identify forms up to an exact 1-form $d\phi$, for $\phi\in\Lambda^0(S)$. My first queston pops up here:
Why do we insist that these be our degrees of freedom? Is it for mathematical reasons, or experimental ones, i.e. we know that the photon carries two polarizations and somehow we want to cut down the 4 degrees of freedom of $A$?
So it seems that the equations of motion are effectively given by
$$ \Lambda^1(S)/\mathcal{E}(S) \xrightarrow{ \ \tilde{D} \ } \Lambda^1(S) $$ where $\text{Im}d_0 \equiv \mathcal{E}(S)$, the space of exact forms. The space of solutions now, it seems to me, should be
$$ \text{ker}\tilde{D}=\{A\in \Lambda^1(S)/\mathcal{E}(S) \ | \ DA=0 \}. $$ So what one usually does is pick a gauge, namely a coset in the domain, solve the equation, and then make sure that the solution is gauge invariant, which is related to the fact that a function with domain a coset space ought to be well-define (i.e. independent of the representative).
The next question I must admit I haven't thought about deeply, it has to do with the index of $D$ defined as
$$\text{ind}D=\text{dim} \ \text{ker}D - \text{dim} \left( \ \Lambda^1(S)/\text{Im} \ D\right)$$ and if the operator is to have a well defined index, it ought to be Fredholm, namely: $\text{dim} \ \text{ker}D<\infty$ and $\text{dim} \left( \ \Lambda^1(S)/\text{Im} \ D\right)<\infty$, being Fredholm means that the linear map $D$ is "almost" isomorphism, hence we can invert it and get a Green's function. The question is the following:
Could it be that we choose our degrees of freedom to be elements of $\Lambda^1(S)/\mathcal{E}(S)$ so that the operator becomes Fredholm?
(As far as I understand it is important for an operator to be Fredholm, as we can extract topological information regarding our manifold via the Atiyah-Singer type theorems, purely from information of a linear operator.)