Theorem. Inverse components and retained compression [fdip-001V]
✍️source

  • October 23, 2026

Over a commutative unital ring \(R\), let \(M=X\oplus Y\) be a chosen splitting, with ordinary linear endomorphism \(Q(x,y)=(Ax+By,Ex+Cy)\). Assume that the eliminated component \(C\) is an isomorphism, and put \(S=A-BC^{-1}E\). Then \(Q\) is an isomorphism if and only if \(S\) is an isomorphism. When these conditions hold, all 4 components of the inverse are \[\begin {aligned} \pi _XQ^{-1}\iota _X&=S^{-1}:X\to X,\\ \pi _XQ^{-1}\iota _Y&=-S^{-1}BC^{-1}:Y\to X,\\ \pi _YQ^{-1}\iota _X&=-C^{-1}ES^{-1}:X\to Y,\\ \pi _YQ^{-1}\iota _Y&=C^{-1}+C^{-1}ES^{-1}BC^{-1}:Y\to Y. \end {aligned}\] In particular, the retained compression of \(Q^{-1}\) is \(S^{-1}\); it is not in general \(A^{-1}\).

Proof. 

  • October 23, 2026

Use \(Q=UDV\) and the explicit inverses of \(U,V\) from triangular factorization, where \(D(x,y)=(Sx,Cy)\). If \(S\) is invertible, then \(D^{-1}(u,v)=(S^{-1}u,C^{-1}v)\). Thus \(Q^{-1}=V^{-1}D^{-1}U^{-1}\) is a two-sided inverse.

Conversely, suppose \(Q\) is invertible. Then \(D=U^{-1}QV^{-1}\) is invertible; write \(J=D^{-1}\) and set \(J_X=\pi _XJ\iota _X:X\to X\). The identities \(\pi _XD=S\pi _X\) and \(D\iota _X=\iota _XS\) imply \[\begin {aligned} SJ_X&=\pi _XDJ\iota _X=\pi _X\iota _X=I_X,\\ J_XS&=\pi _XJD\iota _X=\pi _X\iota _X=I_X. \end {aligned}\] Hence \(J_X\) is a two-sided inverse of \(S\). This implication still uses the assumed invertibility of \(C\).

Applying the three inverse factors to \((u,v)\) gives \[\begin {aligned} x&=S^{-1}u-S^{-1}BC^{-1}v,\\ y&=-C^{-1}ES^{-1}u +(C^{-1}+C^{-1}ES^{-1}BC^{-1})v. \end {aligned}\] Setting one input component to zero and projecting the other gives the 4 stated map identities.

The real symmetric inverse formula is [boyd2004convex, Appendix A.5.5, p. 650]; its first-pivot convention is exchanged here. The direct proof uses arbitrary unital \(R\)-modules and needs no pairing or symmetry. Mathlib's CategoryTheory.Biprod.isoElim' constructs the residual isomorphism when both the first component and the whole biproduct map are isomorphisms. With summands \((Y,X)\) and component arguments \((C,B,E,A)\), it supports the whole-to-residual direction; it does not by itself assert the 4 inverse formulas above.

For a self-adjoint precision with a chosen perfect pairing, inverse response supplies its separate response interpretation. The cycle calculation exhibits a retained inverse entry \(2/15\) where \(A^{-1}\) has entry zero. No probability law is needed for the map comparison.