Redundant and indispensable relation coordinates

Proof. We prove the contrapositive equivalence: $r_\alpha$ is redundant if and only if no pair (6.3) exists, i.e. if and only if $r_\alpha$ is constant on every fiber of the joint map $g:=(p,R_{A_{-\alpha}})\colon S\to T\times V_{A_{-\alpha}}$. This is the descent statement of Paper 1 [1] applied to $g$; we give the argument in full.

Redundant $\Rightarrow$ constant on fibers of $g$. Suppose (6.2) holds and suppose $g(s)=g(s')$, i.e. $p(s)=p(s')$ and $r_\beta(s)=r_\beta(s')$ for all $\beta\neq\alpha$. Applying $f_\alpha$ to the equal values $g(s)=g(s')$ gives $r_\alpha(s)=f_\alpha(g(s))=f_\alpha(g(s'))=r_\alpha(s')$. Hence no pair as in (6.3) can exist.

Constant on fibers of $g$ $\Rightarrow$ redundant. Suppose that $g(s)=g(s')$ implies $r_\alpha(s)=r_\alpha(s')$. Define $f_\alpha$ on the image of $g$ by $$f_\alpha\bigl(g(s)\bigr):=r_\alpha(s)\qquad(s\in S),\tag{6.4}$$ The prescription (6.4) is well defined on $\mathop{\mathrm{Im}}(g)$ precisely by the assumed fiber-constancy: if $g(s)=g(s')$ then the two prescribed values $r_\alpha(s)$ and $r_\alpha(s')$ agree. Every point of $\mathop{\mathrm{Im}}(g)$ is of the form $g(s)$, so $f_\alpha$ is defined on all of $\mathop{\mathrm{Im}}(g)$. It remains to extend $f_\alpha$ to the whole of $T\times V_{A_{-\alpha}}$, and we treat the two cases explicitly.

Case $S\neq\varnothing$. Fix any $s_0\in S$ and define $f_\alpha(y):=r_\alpha(s_0)$ for every $y\in\bigl(T\times V_{A_{-\alpha}}\bigr)\setminus\mathop{\mathrm{Im}}(g)$. This is legitimate because $r_\alpha(s_0)$ is an element of $V_\alpha$, so $V_\alpha\neq\varnothing$ and a value is available. The extension changes nothing on $\mathop{\mathrm{Im}}(g)$, where (6.4) already fixes $f_\alpha$.

Case $S=\varnothing$. Then $T=\varnothing$: the readout $p\colon S\to T$ is surjective by standing hypothesis, and the image of the empty map is empty, so $T=p(S)=\varnothing$. Hence the product $T\times V_{A_{-\alpha}}=\varnothing$ as well, and the unique map $\varnothing\to V_\alpha$, the empty map, serves as $f_\alpha$. It satisfies $r_\alpha=f_\alpha\circ g$ vacuously as an identity of maps out of $S=\varnothing$, both sides being the empty map. So $r_\alpha$ is redundant in this case, which is consistent: no witness pair (6.3) can exist in an empty source, so $r_\alpha$ is not indispensable, exactly as the equivalence requires. (The two sides of the criterion agree here; the case is not merely set aside.)

In either case $f_\alpha$ is defined on all of $T\times V_{A_{-\alpha}}$ and satisfies $r_\alpha=f_\alpha\circ g$, which is (6.2).

Finally, “no pair as in (6.3)” is by inspection the same statement as “$g(s)=g(s')$ implies $r_\alpha(s)=r_\alpha(s')$”, since the first two clauses of (6.3) say $g(s)=g(s')$ and the third says $r_\alpha(s)\neq r_\alpha(s')$. Negating both sides of the equivalence just proved yields $\Leftrightarrow$. ◻

Proof. The inclusion $\sim_A\subseteq\sim_{A_{-\alpha}}$ is immediate from (3.5), since the defining condition for $\sim_A$ is the condition for $\sim_{A_{-\alpha}}$ conjoined with the extra clause $r_\alpha(s)=r_\alpha(s')$.

(1) $\Leftrightarrow$ (3). Strictness means: there exist $s,s'$ with $s\sim_{A_{-\alpha}}s'$ but not $s\sim_A s'$. Unwinding (3.5), this says $p(s)=p(s')$ and $r_\beta(s)=r_\beta(s')$ for all $\beta\neq\alpha$, while $r_\alpha(s)\neq r_\alpha(s')$, which is exactly the witness (6.3). By Theorem 6.2 this holds iff $r_\alpha$ is indispensable.

(1) $\Leftrightarrow$ (2). By Proposition 3.4, $E_A\cong S/\!\sim_A$ and $E_{A_{-\alpha}}\cong S/\!\sim_{A_{-\alpha}}$, and under these identifications $\pi$ is the canonical map $S/\!\sim_A\ \to\ S/\!\sim_{A_{-\alpha}}$ sending $[s]_A\mapsto[s]_{A_{-\alpha}}$, which is well defined by the inclusion just proved. This map is injective iff $[s]_{A_{-\alpha}}=[s']_{A_{-\alpha}}$ implies $[s]_A=[s']_A$, i.e. iff $\sim_{A_{-\alpha}}\ \subseteq\ \sim_A$, i.e. (given the reverse inclusion) iff the two relations are equal. Its failure is precisely strictness. ◻