Book a Demo!
CoCalc Logo Icon
StoreFeaturesDocsShareSupportNewsAboutPoliciesSign UpSign In
Download
324 views
ubuntu2004
Kernel: SageMath 9.8

NOTE: The notebook cannot be run online in the cloud because CoCalc does not allow to install or load custom packages in publicly shared files.

The outputs, however, are still visible, giving an indication of the computations.

To edit the file and run the code, please follow the following steps:

  • Download this file to your local machine (or a private CoCalc project).

  • Install the package operator_gb as desribed on its webpage (https://github.com/ClemensHofstadler/operator_gb).

  • Open the notebook, for example by running the following command in your terminal: $ sage -n jupyter /path/to/Case-Study.ipynb where "/path/to/" is the path to the directory in which the file Case-Study.ipynb is. 

from operator_gb import *

The Moore-Penrose inverse

Recall that the Moore-Penrose inverse of a complex matrix AA (or more generally of a linear operator AA) is the complex matrix (resp. the linear operator) BB satisfying ABA=A,BAB=B,AB=B∗A∗,BA=A∗B∗, ABA = A, \qquad BAB = B, \qquad AB = B^\ast A^\ast, \qquad BA = A^\ast B^\ast, where P∗P^\ast denotes the Hermitian adjoint of a complex matrix (resp. a linear operator) PP.

Handbook of Linear Algebra

Uniqueness of Moore-Penrose Inverse (Fact 1 in [Hog13, Sec. I.5.7])

If BB and CC both satisfy the Moore-Penrose identities for AA, then B=CB = C.

Required property: Enconding the Hermitian transpose ∗^{}\ast

Strategy: Add for every assumed identitiy P=QP = Q also the corresponding adjoint identity P∗=Q∗P^\ast = Q^\ast and simplify all operator expressions using the following identities before translating them into polynomials.

(P+Q)∗=P∗+Q∗,(PQ)∗=Q∗P∗,(P∗)∗=P(P+Q)^\ast = P^* + Q^*, \qquad\qquad (PQ)^\ast = Q^\ast P^\ast, \qquad\qquad (P^\ast)^\ast = P
# first create FreeAlgebra
F.<a, b, c, a_adj, b_adj, c_adj> = FreeAlgebra(QQ)

# create assumptions and claim as usual SageMath noncommutative polynomials
# the command pinv generates polynomials for the Moore-Penrose identities
Pinv_B = pinv(a, b, a_adj, b_adj)
Pinv_C = pinv(a, c, a_adj, c_adj)
# the command add_adj adds the corresponding adjoint statements
assumptions = add_adj(Pinv_B + Pinv_C)
claim = b - c

print("The assumptions are %s.\n" % str(assumptions))
print("The claim is %s.\n" % str(claim))

# make quiver - a quiver is a list of triples (source, target, label)
Q = Quiver([(1,2,a), (2,1,b), (2,1,c), (2,1,a_adj), (1,2,b_adj), (1,2,c_adj)])

# call certify
proof = certify(assumptions,claim,Q)

print("The proof is:")
pretty_print_proof(proof,assumptions)
The assumptions are [-a + a*b*a, -b + b*a*b, -a*b + b_adj*a_adj, -b*a + a_adj*b_adj, -a + a*c*a, -c + c*a*c, -a*c + c_adj*a_adj, -c*a + a_adj*c_adj, a_adj - a_adj*b_adj*a_adj, b_adj - b_adj*a_adj*b_adj, a_adj - a_adj*c_adj*a_adj, c_adj - c_adj*a_adj*c_adj]. The claim is b - c. Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! The proof is:
'b - c = (-c + c*a*c) - b*c_adj*(a_adj - a_adj*b_adj*a_adj) - b*a*c*(-a*b + b_adj*a_adj) - b*(-a + a*c*a)*b + b*(-a*c + c_adj*a_adj) - b*(-a*c + c_adj*a_adj)*b_adj*a_adj - (-b + b*a*b) + (-c*a + a_adj*c_adj)*b*a*c + (a_adj - a_adj*c_adj*a_adj)*b_adj*c + c*(-a + a*b*a)*c - (-b*a + a_adj*b_adj)*c + a_adj*c_adj*(-b*a + a_adj*b_adj)*c'

Existence of Moore-Penrose Inverse (Fact 1 in [Hog13, Sec. I.5.7])

Every complex matrix has a Moore-Penrose Inverse.

Required property: Proving an existential statements

Strategy: Construct explicit expression for the existentially quantified variable.

To do this, the package provides dedicated methods, such as the command find_equivalent_expression.

F.<a,b,c,a_adj,b_adj,c_adj,x,x_adj> = FreeAlgebra(QQ)

# in this example, we first to find an expression for the Moore-Penrose inverse
# we do this using our heuristics
# to this end, we introduce a dummy variable x satisfying the Moore-Penrose equations
# and then search for an expression equivalent to x but in terms of a,b,c and their adjoints
assumptions =  add_adj([a - b*a_adj*a, a - a*a_adj*c])
Pinv_x = add_adj(pinv(a, x, a_adj, x_adj))
I = NCIdeal(Pinv_x + assumptions)
candidates = I.find_equivalent_expression(x)
# one of the candidates shows that X = A^* C B^*
print("Found candidates for the Moore-Penrose inverse: %s\n"% str(candidates))

# we show that the candidate a_adj*c*b_adj is indeed the Moore-Penrose inverse of a
# by showing that it satisfies the four Moore-Penrose equations
MP_candidate = a_adj * c * b_adj
MP_candidate_adj = b * c_adj * a
claim = pinv(a, MP_candidate, a_adj, MP_candidate_adj)
print("The assumptions are %s\n" % str(assumptions))
print("The claim is %s\n" % str(claim))

# call certify
proof = certify(assumptions,claim)

print("The proofs consist of %s steps, respectively.\n" % str(list(map(len,proof))))
print("The following assumptions were used %s" % str({assumptions[cofactor.i()] for p in proof for cofactor in p}))
Found candidates for the Moore-Penrose inverse: [- x + a_adj*c*b_adj, - x + a_adj*x_adj*x, - x + a_adj*c*x, - x + a_adj*b*x] The assumptions are [a - b*a_adj*a, a - a*a_adj*c, a_adj - a_adj*a*b_adj, a_adj - c_adj*a*a_adj] The claim is [-a + a*a_adj*c*b_adj*a, -a_adj*c*b_adj + a_adj*c*b_adj*a*a_adj*c*b_adj, -a*a_adj*c*b_adj + b*c_adj*a*a_adj, a_adj*b*c_adj*a - a_adj*c*b_adj*a] Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! The proofs consist of [4, 8, 4, 12] steps, respectively. The following assumptions were used {a_adj - a_adj*a*b_adj, a - b*a_adj*a, a_adj - c_adj*a*a_adj, a - a*a_adj*c}

Moore-Penrose inverse of real matrix is real (Fact 2 in [Hog13, Sec. I.5.7])

If AA is a real matrix, then A†A^\dagger is real as well.

Required property: Enconding real matrices

Strategy: Decompose Hermitian adjoint into complex conjugation and transposition, i.e., A∗=(AC)TA^* = (A^C)^T, and express AA being real as A=ACA = A^C.

In terms of polynomials, this means introducing new variables aCa^C and aTa^T and adding the polynomial a−aCa - a^C .

Additionally, for every assumption P=QP = Q, the corresponding adjoint identity P∗=Q∗P^* = Q^*, the transposed identity PT=QTP^T = Q^T, and the conjugated identitiy PC=QCP^C = Q^C have to be translated into polynomials as well. These additional identities first have to be simplified using the following rules that relate the different function symbols to each other (P+Q)α=Pα+Qα,(Pα)β={P if α=βPγ if α≠β,(PQ)C=PCQC,(PQ)δ=QδPδ,\begin{align*} (P+Q)^\alpha &= P^\alpha + Q^\alpha, \qquad\quad& (P^\alpha)^\beta &= \begin{cases} P & \text{ if } \alpha = \beta \\ P^\gamma & \text{ if } \alpha \neq \beta \end{cases},\\ (PQ)^C &= P^C Q^C, & (PQ)^\delta &= Q^\delta P^\delta, \end{align*} with α,β,γ,δ∈{∗,C,T}\alpha,\beta,\gamma,\delta \in \{\ast, C, T\} such that γ≠α,β\gamma \neq \alpha, \beta and δ≠C\delta \neq C.

F.<a, a_tr, a_c, a_adj, b, b_tr, b_c, b_adj> = FreeAlgebra(QQ)

# the classical Moore-Penrose identities + their adjoint statements
Pinv_b = add_adj(pinv(a, b, a_adj, b_adj))
# the transposed identities
Pinv_b_tr = [a_tr*b_tr*a_tr - a_tr, b_tr*a_tr*b_tr - b_tr, a_tr*b_tr - b_c*a_c, b_tr*a_tr - a_c*b_c]
# the conjugated identities
Pinv_b_c = [a_c*b_c*a_c - a_c, b_c*a_c*b_c - b_c]
# assumption that a is real
a_real = [a - a_c, a_tr - a_adj]

assumptions = Pinv_b + Pinv_b_tr + Pinv_b_c + a_real
claim = b - b_c

print("The assumptions are %s\n" % str(assumptions))
print("The claim is %s\n" % str(claim))

Q = Quiver([(1, 2, u) for u in [a, a_c, b_tr, b_adj]] + [(2, 1, u) for u in [a_tr, a_adj, b, b_c]])

proof = certify(assumptions, claim, Q)

print("The proof is:")
pretty_print_proof(proof, assumptions)
The assumptions are [-a + a*b*a, -b + b*a*b, -a*b + b_adj*a_adj, a_adj*b_adj - b*a, a_adj - a_adj*b_adj*a_adj, b_adj - b_adj*a_adj*b_adj, -a_tr + a_tr*b_tr*a_tr, -b_tr + b_tr*a_tr*b_tr, a_tr*b_tr - b_c*a_c, -a_c*b_c + b_tr*a_tr, -a_c + a_c*b_c*a_c, -b_c + b_c*a_c*b_c, a - a_c, a_tr - a_adj] The claim is b - b_c Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! The proof is:
'b - b_c = (a_tr*b_tr - b_c*a_c)*b - (-b + b*a*b) + (-b_c + b_c*a_c*b_c) - b_c*b_tr*(a_adj - a_adj*b_adj*a_adj) - b_c*b_tr*(a_tr - a_adj) + b_c*b_tr*(a_tr - a_adj)*b_adj*a_adj - b_c*b_tr*a_tr*(-a*b + b_adj*a_adj) - b_c*a*b_c*(a - a_c)*b - b_c*(-a_c + a_c*b_c*a_c)*b - b_c*(a - a_c)*b_c*a_c*b + b_c*(-a_c*b_c + b_tr*a_tr) - b_c*(-a_c*b_c + b_tr*a_tr)*a*b + b_c*(a - a_c)*b_c*a*b - (a_adj*b_adj - b*a)*a_tr*b_tr*b - (a_tr - a_adj)*b_adj*a_tr*b_tr*b + a_tr*b_adj*(a_tr - a_adj)*b_tr*b - (a_adj - a_adj*b_adj*a_adj)*b_tr*b - (a_tr - a_adj)*b_tr*b + (a_tr - a_adj)*b_adj*a_adj*b_tr*b - b*(-a_c + a_c*b_c*a_c)*b + b*(a - a_c)*b - b*(a - a_c)*b_c*a_c*b - b*a*(a_tr*b_tr - b_c*a_c)*b'

Full Rank Decomposition (Fact 3 in [Hog13, Sec. I.5.7])

If A=BCA = BC is a full rank decomposition, i.e., BB has full column rank and CC has full row rank, then A†=C∗(B∗AC∗)−1B∗A^\dagger = C^*(B^*AC^*)^{-1}B^*.

Required property: Enconding full rank of matrices

Strategy: Use the fact that full row (resp. column) rank correspond to the existence of a right (resp. left) inverse.

Thus, AA having full row rank can be encoded via the identity AU=IUAU = I_U, where UU is a new symbol that does not satisfy any additional hypotheses and IUI_U is the identity matrix. Analogously, full column rank of AA corresponds to the identity VA=IVVA = I_V.

To encode the identity matrices, a new indeterminate iui_u has to be introduced for every identity matrix IUI_U and the identities satisfied by IUI_U have to be added explicitly to the assumptions. In particular, these are the idempotency of IUI_U, the fact that IUI_U is self-adjoint, and the identities AIU=AA I_U = A and IUB=BI_U B = B for all basic operators A,BA,B for which these expressions are well-defined.

Remark: More generally, using one-sided inverses also injectivity and surjectivity of operators can be encoded.

Remark: Note that B∗AC∗=B∗BCC∗B^\ast A C^\ast = B^\ast B C C^\ast is invertible because B∗BB^\ast B and CC∗CC^\ast are.

# inverse of full rank dec

F.<a, b, c, i, u, v, x, a_adj, b_adj, c_adj, i_adj, u_adj, v_adj, x_adj, inv, inv_adj> = FreeAlgebra(QQ)

Pinv_x = pinv(a, x, a_adj, x_adj)
a_decomposition = [a - b*c]
full_rank = [u*b - i, c*v - i]
inverse = [b_adj*a*c_adj*inv - i, inv*b_adj*a*c_adj - i]
identity_matrix = [i*i - i, i - i_adj, b*i - b, i*c - c, i*u - u, v*i - v, inv*i-inv, i*inv-inv]

assumptions = add_adj(Pinv_x + a_decomposition + full_rank + inverse + identity_matrix)
claim = x - c_adj * inv * b_adj

Q = Quiver([(1, 2, u) for u in [a, x_adj]] + 
           [(2, 1, u) for u in [a_adj, x]] + 
           [(1, 3, u) for u in [c, v_adj]] + 
           [(3, 1, u) for u in [c_adj, v]] + 
           [(2, 3, u) for u in [b_adj, u]] + 
           [(3, 2, u) for u in [b, u_adj]] + 
           [(3, 3, u) for u in [i, i_adj, inv, inv_adj]])

proof = certify(assumptions, claim, Q)

print("The proof consists of %d steps\n" % len(proof))
Computing a (partial) Groebner basis and reducing the claims... Starting iteration 5... Done! Ideal membership of all claims could be verified! The proof consists of 17 steps

Moore-Penrose Inverse via Singular Value Decomposition (Fact 4,17 in [Hog13, Sec. I.5.7])

If A=UΣV∗A = U \Sigma V^* with U,VU, V unitary, then A†=VΣ†U∗A^\dagger = V \Sigma^\dagger U^* 

#inverse of SVD

F.<a, a_adj, x, x_adj, s, s_adj, y, y_adj, u, u_adj, v, v_adj, id1, id1_adj, id2, id2_adj> = FreeAlgebra(QQ)

Pinv_x = pinv(a, x, a_adj, x_adj)
Pinv_s = pinv(s, y, s_adj, y_adj)
identity_matrices = [exp for o in [x, a_adj, y, s_adj] for exp in (id1*o - o, o*id2 - o)] + [exp for o in [x_adj, a, y_adj, s] for exp in (o*id1 - o, id2*o - o)] + [id2*u - u, u*id2 - u, id2*u_adj - id2, u_adj*id2 - u_adj, id1*v - v, v*id1 - v, v_adj*id1 - v_adj, id1*v_adj - v_adj]
uv_normal = [u*u_adj - id2, u_adj*u - id2, v*v_adj - id1, v_adj*v - id1]
a_decomposition = [a - u*s*v_adj, a_adj - v*s_adj*u_adj]

assumptions = add_adj(Pinv_x + Pinv_s + a_decomposition + uv_normal + identity_matrices)
claim = x - v*y*u_adj

print("The assumptions are %s\n" % str(assumptions))
print("The claim is %s\n" % str(claim))

Q = Quiver([(1, 2, u) for u in [a, x_adj, s, y_adj]] + 
            [(2, 1, u) for u in [a_adj, x, s_adj, y]] + 
           [(1, 1, u) for u in [id1, id1_adj, v, v_adj]] +
           [(2, 2, u) for u in [id2, id2_adj, u, u_adj]])

proof = certify(assumptions,claim,Q)

print("The proof consists of %d steps\n" % len(proof))
print("The following assumptions were used %s" % str({assumptions[cofactor.i()] for cofactor in proof}))
The assumptions are [-a + a*x*a, -x + x*a*x, -a*x + x_adj*a_adj, a_adj*x_adj - x*a, -s + s*y*s, -y + y*s*y, -s*y + y_adj*s_adj, s_adj*y_adj - y*s, a - u*s*v_adj, a_adj - v*s_adj*u_adj, -id2 + u*u_adj, -id2 + u_adj*u, -id1 + v*v_adj, -id1 + v_adj*v, -x + id1*x, -x + x*id2, -a_adj + id1*a_adj, -a_adj + a_adj*id2, -y + id1*y, -y + y*id2, -s_adj + id1*s_adj, -s_adj + s_adj*id2, -x_adj + x_adj*id1, -x_adj + id2*x_adj, -a + a*id1, -a + id2*a, -y_adj + y_adj*id1, -y_adj + id2*y_adj, -s + s*id1, -s + id2*s, -u + id2*u, -u + u*id2, -id2 + id2*u_adj, -u_adj + u_adj*id2, -v + id1*v, -v + v*id1, -v_adj + v_adj*id1, -v_adj + id1*v_adj, a_adj - a_adj*x_adj*a_adj, x_adj - x_adj*a_adj*x_adj, s_adj - s_adj*y_adj*s_adj, y_adj - y_adj*s_adj*y_adj, id2_adj - u*u_adj, id2_adj - u_adj*u, id1_adj - v*v_adj, id1_adj - v_adj*v, x_adj - x_adj*id1_adj, x_adj - id2_adj*x_adj, a - a*id1_adj, a - id2_adj*a, y_adj - y_adj*id1_adj, y_adj - id2_adj*y_adj, s - s*id1_adj, s - id2_adj*s, x - id1_adj*x, x - x*id2_adj, a_adj - id1_adj*a_adj, a_adj - a_adj*id2_adj, y - id1_adj*y, y - y*id2_adj, s_adj - id1_adj*s_adj, s_adj - s_adj*id2_adj, u_adj - u_adj*id2_adj, u_adj - id2_adj*u_adj, id2_adj - u*id2_adj, u - id2_adj*u, v_adj - v_adj*id1_adj, v_adj - id1_adj*v_adj, v - id1_adj*v, v - v*id1_adj] The claim is x - v*y*u_adj Computing a (partial) Groebner basis and reducing the claims... Starting iteration 5... Done! Ideal membership of all claims could be verified! The proof consists of 123 steps The following assumptions were used {-u + u*id2, -s*y + y_adj*s_adj, a_adj - a_adj*x_adj*a_adj, id2_adj - u*id2_adj, -y + y*s*y, -s + id2*s, s_adj*y_adj - y*s, a - u*s*v_adj, y_adj - y_adj*s_adj*y_adj, u_adj - id2_adj*u_adj, -s_adj + s_adj*id2, id2_adj - u*u_adj, -s + s*y*s, id1_adj - v_adj*v, -id1 + v*v_adj, -y + y*id2, s_adj - s_adj*y_adj*s_adj, a_adj - v*s_adj*u_adj, -id2 + u*u_adj, -x + x*a*x, -a + a*x*a, -a*x + x_adj*a_adj, a_adj*x_adj - x*a, -s_adj + id1*s_adj, -id2 + id2*u_adj, id1_adj - v*v_adj}

Moore-Penrose inverse is Involution (Fact 10 in [Hog13, Sec. I.5.7])

(A†)†=A(A^\dagger)^\dagger = A

#inverse involution

F.<a, x, y, a_adj, x_adj, y_adj> = FreeAlgebra(QQ)

Pinv_x = pinv(a, x, a_adj, x_adj)
Pinv_y = pinv(x, y, x_adj, y_adj)

assumptions = add_adj(Pinv_x + Pinv_y)
claim = a - y

print("The assumptions are %s\n" % str(assumptions))
print("The claim is %s\n" % str(claim))

Q = Quiver([(1, 2, u) for u in [a, x_adj, y]] + [(2, 1, u) for u in [a_adj, x, y_adj]])

proof = certify(assumptions,claim,Q)

print("The proof consists of %d steps\n" % len(proof))
print("The following assumptions were used %s" % str({assumptions[cofactor.i()] for cofactor in proof}))
The assumptions are [-a + a*x*a, -x + x*a*x, -a*x + x_adj*a_adj, -x*a + a_adj*x_adj, -x + x*y*x, -y + y*x*y, -x*y + y_adj*x_adj, -y*x + x_adj*y_adj, a_adj - a_adj*x_adj*a_adj, x_adj - x_adj*a_adj*x_adj, x_adj - x_adj*y_adj*x_adj, y_adj - y_adj*x_adj*y_adj] The claim is a - y Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! The proof consists of 12 steps The following assumptions were used {-x + x*a*x, -x + x*y*x, -y + y*x*y, -x*y + y_adj*x_adj, x_adj - x_adj*y_adj*x_adj, -a + a*x*a, -a*x + x_adj*a_adj, -y*x + x_adj*y_adj, x_adj - x_adj*a_adj*x_adj, -x*a + a_adj*x_adj}

Moore-Penrose Inverse of Adjoint (Fact 10 in [Hog13, Sec. I.5.7])

(A∗)†=(A†)∗(A^*)^\dagger = (A^\dagger)^* 

#inverse of adjoint is adjoint inverse

F.<a, a_dag, a_adj_dag, a_adj, a_dag_adj, a_adj_dag_adj> = FreeAlgebra(QQ)

Pinv_a = pinv(a, a_dag, a_adj, a_dag_adj)
Pinv_a_adj = pinv(a_adj, a_adj_dag, a, a_adj_dag_adj)

assumptions = add_adj(Pinv_a + Pinv_a_adj)
claim = a_dag_adj - a_adj_dag

print("The assumptions are %s\n" % str(assumptions))
print("The claim is %s\n" % str(claim))

Q = Quiver([(1, 2, u) for u in [a, a_dag_adj, a_adj_dag]] + [(2, 1, u) for u in [a_adj, a_dag, a_adj_dag_adj]])

proof = certify(assumptions,claim,Q)

print("The proof consists of %d steps\n" % len(proof))
print("The following assumptions were used %s" % str({assumptions[cofactor.i()] for cofactor in proof}))
The assumptions are [-a + a*a_dag*a, -a_dag + a_dag*a*a_dag, -a*a_dag + a_dag_adj*a_adj, -a_dag*a + a_adj*a_dag_adj, -a_adj + a_adj*a_adj_dag*a_adj, -a_adj_dag + a_adj_dag*a_adj*a_adj_dag, -a_adj*a_adj_dag + a_adj_dag_adj*a, a*a_adj_dag_adj - a_adj_dag*a_adj, a_adj - a_adj*a_dag_adj*a_adj, a_dag_adj - a_dag_adj*a_adj*a_dag_adj, a - a*a_adj_dag_adj*a, a_adj_dag_adj - a_adj_dag_adj*a*a_adj_dag_adj] The claim is -a_adj_dag + a_dag_adj Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! The proof consists of 12 steps The following assumptions were used {a - a*a_adj_dag_adj*a, a*a_adj_dag_adj - a_adj_dag*a_adj, -a_adj*a_adj_dag + a_adj_dag_adj*a, -a*a_dag + a_dag_adj*a_adj, a_adj - a_adj*a_dag_adj*a_adj, a_dag_adj - a_dag_adj*a_adj*a_dag_adj, -a_dag*a + a_adj*a_dag_adj, -a_adj_dag + a_adj_dag*a_adj*a_adj_dag}

Moore-Penrose inverse of non-singular square matrix (Fact 11 in [Hog13, Sec. I.5.7])

If AA is a non-singular square matrix, then A†=A−1A^\dagger = A^{-1}.

#inverse of bijective operator

F.<a, a_dag, a_adj, a_dag_adj, a_inv, a_inv_adj, id1, id2, id1_adj, id2_adj> = FreeAlgebra(QQ)

Pinv_a = pinv(a, a_dag, a_adj, a_dag_adj)
identity_matrices = [id2*a - a, a*id1 - a, a_dag*id2 - a_dag, id1*a_dag - a_dag, a_inv*id2 - a_inv, id1*a_inv - a_inv, a_adj*id2 - a_adj, id1*a_adj - a_adj, id2*a_dag_adj - a_dag_adj, a_dag_adj*id1 - a_dag_adj, id2*a_inv_adj - a_inv_adj, a_inv_adj*id1 - a_inv_adj]
a_inverse = [a*a_inv - id2, a_inv*a - id1]

assumptions = add_adj(Pinv_a + a_inverse + identity_matrices)
claim = a_dag - a_inv

print("The assumptions are %s\n" % str(assumptions))
print("The claim is %s\n" % str(claim))

Q = Quiver([(1, 2, u) for u in [a, a_dag_adj, a_inv_adj]] + 
           [(2, 1, u) for u in [a_adj, a_dag, a_inv]] + 
           [(1, 1, id1), (1, 1, id1_adj), (2, 2, id2), (2, 2, id2_adj)])

proof = certify(assumptions,claim,Q)

print("The proof consists of %d steps\n" % len(proof))
print("The following assumptions were used %s" % str({assumptions[cofactor.i()] for cofactor in proof}))
The assumptions are [-a + a*a_dag*a, -a_dag + a_dag*a*a_dag, -a*a_dag + a_dag_adj*a_adj, -a_dag*a + a_adj*a_dag_adj, -id2 + a*a_inv, -id1 + a_inv*a, -a + id2*a, -a + a*id1, -a_dag + a_dag*id2, -a_dag + id1*a_dag, -a_inv + a_inv*id2, -a_inv + id1*a_inv, -a_adj + a_adj*id2, -a_adj + id1*a_adj, -a_dag_adj + id2*a_dag_adj, -a_dag_adj + a_dag_adj*id1, -a_inv_adj + id2*a_inv_adj, -a_inv_adj + a_inv_adj*id1, a_adj - a_adj*a_dag_adj*a_adj, a_dag_adj - a_dag_adj*a_adj*a_dag_adj, id2_adj - a_inv_adj*a_adj, id1_adj - a_adj*a_inv_adj, a_adj - a_adj*id2_adj, a_adj - id1_adj*a_adj, a_dag_adj - id2_adj*a_dag_adj, a_dag_adj - a_dag_adj*id1_adj, a_inv_adj - id2_adj*a_inv_adj, a_inv_adj - a_inv_adj*id1_adj, a - id2_adj*a, a - a*id1_adj, a_dag - a_dag*id2_adj, a_dag - id1_adj*a_dag, a_inv - a_inv*id2_adj, a_inv - id1_adj*a_inv] The claim is a_dag - a_inv Computing a (partial) Groebner basis and reducing the claims... Starting iteration 5... Done! Ideal membership of all claims could be verified! The proof consists of 12 steps The following assumptions were used {a_inv - id1_adj*a_inv, a_adj - a_adj*a_dag_adj*a_adj, id1_adj - a_adj*a_inv_adj, -a_inv + id1*a_inv, a - a*id1_adj, -a_dag*a + a_adj*a_dag_adj, -id1 + a_inv*a, -a_inv_adj + a_inv_adj*id1, -id2 + a*a_inv, -a_dag + a_dag*id2}

Orthonormal columns or rows (Fact 12 in [Hog13, Sec. I.5.7])

If AA has orthonormal columns or orthonormal rows, then A†=A∗A^\dagger = A^* 

# inverse is conjugate
F.<a, a_dag, a_adj, a_dag_adj, id1, id2, id1_adj, id2_adj> = FreeAlgebra(QQ)

Pinv_a = pinv(a, a_dag, a_adj, a_dag_adj)
a_orthonormal_cols = [a_adj*a - id1]
a_orthonormal_rows = [a*a_adj - id2]
identity_matrix = [a*id1 - a, id2*a - a, id1*a_dag - a_dag, a_dag*id2 - a_dag]

Q = Quiver([(1, 2, u) for u in [a, a_dag_adj]] + 
           [(2, 1, u) for u in [a_adj, a_dag]] + 
           [(1, 1, id1), (1, 1, id1_adj), (2, 2, id2), (2, 2, id2_adj)])

basic_assumptions = Pinv_a + identity_matrix
claim = a_dag - a_adj

# case 1
assumptions_1 = add_adj(basic_assumptions + a_orthonormal_cols)

print("The claim is %s.\n" % str(claim))

proof = certify(assumptions_1, claim, Q)

print("The proof consists of %d steps.\n" % len(proof))
print("The following assumptions were used %s.\n" % str({assumptions_1[cofactor.i()] for cofactor in proof}))


# case 2
assumptions_2 = add_adj(basic_assumptions + a_orthonormal_rows)

print("The claim is %s.\n" % str(claim))

proof = certify(assumptions_2, claim, Q)

print("The proof consists of %d steps.\n" % len(proof))
print("The following assumptions were used %s." % str({assumptions_2[cofactor.i()] for cofactor in proof}))
The claim is a_dag - a_adj. Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! The proof consists of 4 steps. The following assumptions were used {-id1 + a_adj*a, a_adj - a_adj*a_dag_adj*a_adj, -a_dag + id1*a_dag, -a*a_dag + a_dag_adj*a_adj}. The claim is a_dag - a_adj. Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! The proof consists of 4 steps. The following assumptions were used {-a_dag*a + a_adj*a_dag_adj, a_adj - a_adj*a_dag_adj*a_adj, -id2 + a*a_adj, -a_dag + a_dag*id2}.

Self-Inverse (Fact 13 in [Hog13, Sec. I.5.7])

If A=A∗A = A^* and A=A2A = A^2, then A†=AA^\dagger = A.

# self-inverse

F.<a, a_dag, a_adj, a_dag_adj> = FreeAlgebra(QQ)

Pinv_a = pinv(a, a_dag, a_adj, a_dag_adj)

assumptions = add_adj(Pinv_a + [a - a_adj, a*a - a])
claim = a_dag - a
Q = Quiver([(1, 1, u) for u in [a, a_dag_adj, a_adj, a_dag]])

proof = certify(assumptions, claim, Q)

print("The proof consists of %d steps." % len(proof))
Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! The proof consists of 21 steps.

Characterization of Inverse is Adjoint (Fact 14 in [Hog13, Sec. I.5.7])

A†=A∗A^\dagger = A^* if and only if A∗AA^*A is idempotent.

# inverse is conjugate, ==>

F.<a, a_dag, a_adj, a_dag_adj> = FreeAlgebra(QQ)

Pinv_a = pinv(a, a_dag, a_adj, a_dag_adj)

assumptions = add_adj(Pinv_a + [a_adj - a_dag])
claim = a_adj*a - a_adj*a*a_adj*a
Q = Quiver([(1, 2, u) for u in [a, a_dag_adj]] + [(2, 1, u) for u in [a_adj, a_dag]])

proof = certify(assumptions, claim, Q)

print("The proof consists of %d steps." % len(proof))
Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! The proof consists of 4 steps. 
# inverse is conjugate, <==

F.<a, a_dag, a_adj, a_dag_adj> = FreeAlgebra(QQ)

Pinv_a = pinv(a, a_dag, a_adj, a_dag_adj)

assumptions = add_adj(Pinv_a + [a_adj*a - a_adj*a*a_adj*a])
claim = a_adj - a_dag
Q = Quiver([(1, 2, u) for u in [a, a_dag_adj]] + [(2, 1, u) for u in [a_adj, a_dag]])

proof = certify(assumptions, claim, Q)

print("The proof consists of %d steps." % len(proof))
Computing a (partial) Groebner basis and reducing the claims... Starting iteration 5... Done! Ideal membership of all claims could be verified! The proof consists of 11 steps.

Normal matrices commute with Moore-Penrose inverse (Fact 15 in [Hog13, Sec. I.5.7])

If AA is normal, i.e., AA∗=A∗AAA^* = A^*A, then AA†=A†AAA^\dagger = A^\dagger A.

# normality of inverse

F.<a, a_dag, a_adj, a_dag_adj> = FreeAlgebra(QQ)

Pinv_a = pinv(a, a_dag, a_adj, a_dag_adj)

assumptions = add_adj(Pinv_a + [a*a_adj - a_adj*a])
claim = a*a_dag - a_dag*a

Q = Quiver([(1, 1, u) for u in [a, a_adj, a_dag, a_dag_adj]])

proof = certify(assumptions, claim, Q)

print("The proof consists of %d steps." % len(proof))
Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! The proof consists of 18 steps.

Sufficient condition for orthonormal columns (Fact 16 in [Hog13, Sec. I.5.7])

If AA has full column rank and satisfies A†=A∗A^\dagger = A^*, then AA has orthonormal columns.

#If inverse is conjugate

F.<a, a_dag, a_adj, a_dag_adj, i, i_adj, j, j_adj, u, u_adj> = FreeAlgebra(QQ)

Pinv_a = pinv(a, a_dag, a_adj, a_dag_adj)
full_col_rank = [u*a - i]
identity_matrix = [i*i-i, i-i_adj, a*i - a, i*a_dag - a_dag, i*u - u]

assumptions = add_adj(Pinv_a + full_col_rank + identity_matrix + [a_dag - a_adj])
claim = a_adj * a - i

Q = Quiver([(1, 2, x) for x in [a, a_dag_adj, u_adj]] + 
           [(2, 1, x) for x in [a_adj, a_dag, u]] + 
           [(1, 1, x) for x in [i, i_adj]])

proof = certify(assumptions,claim,Q)

print("The proof consists of %d steps." % len(proof))
Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! The proof consists of 9 steps.

Moore-Penrose Inverse in terms of Gram Matrix (Fact 18 in [Hog13, Sec. I.5.7])

It holds that A†=(A∗A)†A∗A^{\dagger} = (A^*A)^{\dagger}A^*.

# formula for inverse

F.<a, a_adj, a_dag, a_dag_adj, b, b_adj, b_dag, b_dag_adj> = FreeAlgebra(QQ)

Pinv_a = pinv(a, a_dag, a_adj, a_dag_adj)
# b = a_adj * a
Pinv_b = pinv(b, b_dag, b, b_dag_adj)

assumptions = add_adj(Pinv_a + Pinv_b + [b - a_adj*a])
claim = a_dag - b_dag*a_adj
Q = Quiver([(1, 2, u) for u in [a, a_dag_adj]] + 
           [(2, 1, u) for u in [a_adj, a_dag]] + 
           [(1, 1, u) for u in [b, b_adj, b_dag, b_dag_adj]])

proof = certify(assumptions, claim, Q)

print("The proof consists of %d steps." % len(proof))
Computing a (partial) Groebner basis and reducing the claims... Starting iteration 5... Done! Ideal membership of all claims could be verified! The proof consists of 88 steps.

Orthogonal projections (Fact 19a in [Hog13, Sec. I.5.7])

A†AA^\dag A, AA†AA^\dag, I1−A†AI_1 - A^\dag A, I2−AA†I_2 - A A^\dag are orthogonal projections.

F.<a, a_adj, a_dag, a_dag_adj, i, i_adj, j, j_adj> = FreeAlgebra(QQ)

Pinv_a = pinv(a, a_dag, a_adj, a_dag_adj)
id = [i*i - i, i - i_adj, j*j - j, j - j_adj,
      a*i - a, a_dag_adj*i - a_dag_adj, i*a_adj - a_adj, i*a_dag - a_dag,
      j*a - a, j*a_dag_adj - a_dag_adj, a_adj*j - a_adj, a_dag*j - a_dag]

assumptions = add_adj(Pinv_a + id)
p = a_dag * a
p_adj = a_adj * a_dag_adj
q = a * a_dag
q_adj = a_dag_adj * a_adj
r = i - p
r_adj = i_adj - p_adj
s = j - q
s_adj = j_adj - q_adj
claims = [p*p - p, q*q - q, r*r - r, s*s - s,
          p - p_adj, q - q_adj, r - r_adj, s - s_adj]
Q = Quiver([(1, 2, u) for u in [a, a_dag_adj]] + 
           [(2, 1, u) for u in [a_adj, a_dag]] + 
           [(1, 1, u) for u in [i, i_adj]] + 
           [(2, 2, u) for u in [j, j_adj]])

proofs = certify(assumptions, claims, Q)
print("\nThe proofs consist of %s steps respectively." % str(list(map(len,proofs))))
Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! The proofs consist of [1, 1, 7, 4, 1, 1, 2, 2] steps respectively.

Projections onto ranges (Fact 20 in [Hog13, Sec. I.5.7])

AA†=Projrange(A)AA^\dag = \text{Proj}_{\text{range}(A)}; A†A=Projrange(A†)A^\dag A = \text{Proj}_{\text{range}(A^\dag)}.

F.<a, a_adj, a_dag, a_dag_adj> = FreeAlgebra(QQ)

Pinv_a = pinv(a, a_dag, a_adj, a_dag_adj)

assumptions = add_adj(Pinv_a)
p = a_dag * a
p_adj = a_adj * a_dag_adj
q = a * a_dag
q_adj = a_dag_adj * a_adj
# first, show that p and q are projections
claims = [p*p - p, q*q - q]
Q = Quiver([(1, 2, u) for u in [a, a_dag_adj]] + 
           [(2, 1, u) for u in [a_adj, a_dag]] + 
           [(1, 1, u) for u in [i, i_adj]] + 
           [(2, 2, u) for u in [j, j_adj]])

proofs = certify(assumptions, claims, Q)
print("\nThe proofs consist of %s steps respectively.\n" % str(list(map(len,proofs))))

# next, show that they are projections onto ranges
# i.e. that R(AA^\dag) = R(A) and and R(A^\dag A) = R(A^\dag)
# by finding suitable factorisations
I = NCIdeal(assumptions)

print("Factorisations to show range(AA^\\dag) = range(A)")
# range(AA^\dag) \subseteq range(A)
print(I.find_equivalent_expression(a*a_dag,prefix=a,heuristic='naive')[0])
# range(A) \subseteq range(AA^\dag)
print(I.find_equivalent_expression(a,prefix=a*a_dag,heuristic='naive')[0])

print("\nFactorisations to show range(A^\\dag A) = range(A^\\dag)")
# range(A^\dag A) \subseteq range(A^\dag)
print(I.find_equivalent_expression(a_dag*a,prefix=a_dag,heuristic='naive')[0])
# range(A^\dag) \subseteq range(A^\dag A)
print(I.find_equivalent_expression(a_dag,prefix=a_dag*a,heuristic='naive')[0])
Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! The proofs consist of [1, 1] steps respectively. Factorisations to show range(AA^\dag) = range(A) a*a_dag - a*a_dag*a_dag_adj*a_adj a - a*a_dag*a Factorisations to show range(A^\dag A) = range(A^\dag) a_dag*a - a_dag*a_dag_adj*a_adj*a a_dag - a_dag*a*a_dag

Properties of Ranges and Kernels (Fact 21a-d in [Hog13, Sec. I.5.7])

(a) range(A)=range(AA∗)=range(AA†)\text{range}(A) = \text{range}(AA^*) = \text{range}(AA^\dag).

(b) range(A†)=range(A∗)=range(A∗A)=range(A†A)\text{range}(A^\dag) = \text{range}(A^*) = \text{range}(A^*A) = \text{range}(A^\dag A).

(c) ker(A)=ker(A∗A)=ker(A†A)\text{ker}(A) = \text{ker}(A^*A) = \text{ker}(A^\dag A).

(d) ker(A†)=ker(A∗)=ker(AA∗)=ker(AA†)\text{ker}(A^\dag) = \text{ker}(A^*) = \text{ker}(AA^*) = \text{ker}(A A^\dag).

F.<a, a_adj, a_dag, a_dag_adj, x, x_adj> = FreeAlgebra(QQ)
Pinv_a = add_adj(pinv(a, a_dag, a_adj, a_dag_adj))
I = NCIdeal(Pinv_a)

# (a)
print("Proof of (a):")
print("Factorisations to show range(A) = range(AA^*)")
# range(A) \subseteq range(AA^*)
print(I.find_equivalent_expression(a,prefix=a*a_adj,heuristic='naive')[0])
# range(AA^*) \subseteq range(A)
print(I.find_equivalent_expression(a*a_adj,prefix=a,heuristic='naive')[0])

print("\nFactorisations to show range(AA^*) = range(AA^\\dag)")
# range(AA^*) \subseteq range(AA^\dag)
print(I.find_equivalent_expression(a*a_adj,prefix=a*a_dag,heuristic='naive')[0])
# range(AA^\dag) \subseteq range(AA^*)
print(I.find_equivalent_expression(a*a_dag,prefix=a*a_adj,heuristic='naive')[0])

# (b)
print("\nProof of (b):")
print("Factorisations to show range(A^\\dag) = range(A^*)")
# range(A^\dag) \subseteq range(A^*)
print(I.find_equivalent_expression(a_dag,prefix=a_adj,heuristic='naive')[0])
# range(A^*) \subseteq range(A^\dag)
print(I.find_equivalent_expression(a_adj,prefix=a_dag,heuristic='naive')[0])

print("\nFactorisations to show range(A^*) = range(A^*A)")
# range(A^*) \subseteq range(A^*A)
print(I.find_equivalent_expression(a_adj,prefix=a_adj*a,heuristic='naive')[0])
# range(A^*A) \subseteq range(A^*)
print(I.find_equivalent_expression(a_adj*a,prefix=a_adj,heuristic='naive')[0])

print("\nFactorisations to show range(A^*A) = range(A^\\dag A)")
# range(A^*A) \subseteq range(A^\dag A)
print(I.find_equivalent_expression(a_adj*a,prefix=a_dag*a,heuristic='naive')[0])
# range(A^\dag A) \subseteq range(A^*A)
print(I.find_equivalent_expression(a_dag*a,prefix=a_adj*a,heuristic='naive')[0])

# (c)
print("\nProof of (c):")
# ker(A) \subseteq ker(A^*A)
assumptions = add_adj(Pinv_a + [a*x])
proof_c1 = certify(assumptions, a_adj * a * x)
# ker(A^*A) \subseteq ker(A)
assumptions = add_adj(Pinv_a + [a_adj*a*x])
proof_c2 = certify(assumptions, a * x)
# ker(A^*A) \subseteq ker(A^\dag A)
assumptions = add_adj(Pinv_a + [a_adj*a*x])
proof_c3 = certify(assumptions, a_dag * a * x)
# ker(A^\dag A) \subseteq ker(A^*A)
assumptions = add_adj(Pinv_a + [a_dag*a*x])
proof_c4 = certify(assumptions, a_adj * a * x)

# (d)
print("\nProof of (d):")
# ker(A^\dag) \subseteq ker(A^*)
assumptions = add_adj(Pinv_a + [a_dag*x])
proof_d1 = certify(assumptions, a_adj * x)
# ker(A^*) \subseteq ker(A^\dag)
assumptions = add_adj(Pinv_a + [a_adj*x])
proof_d2 = certify(assumptions, a_dag * x)
# ker(A^*) \subseteq ker(AA^*)
assumptions = add_adj(Pinv_a + [a_adj*x])
proof_d3 = certify(assumptions, a * a_adj * x)
# ker(AA^*) \subseteq ker(A^*)
assumptions = add_adj(Pinv_a + [a*a_adj*x])
proof_d4 = certify(assumptions, a_adj * x)
# ker(AA^*) \subseteq ker(AA^\dag)
assumptions = add_adj(Pinv_a + [a*a_adj*x])
proof_d5 = certify(assumptions, a*a_dag * x)
# ker(AA^\dag) \subseteq ker(AA^*)
assumptions = add_adj(Pinv_a + [a*a_dag*x])
proof_d6 = certify(assumptions, a * a_adj * x)
Proof of (a): Factorisations to show range(A) = range(AA^*) a - a*a_adj*a_dag_adj a*a_adj - a*a_dag*a*a_adj Factorisations to show range(AA^*) = range(AA^\dag) a*a_adj - a*a_dag*a*a_adj a*a_dag - a*a_adj*a_dag_adj*a_dag Proof of (b): Factorisations to show range(A^\dag) = range(A^*) a_dag - a_adj*a_dag_adj*a_dag a_adj - a_dag*a*a_adj Factorisations to show range(A^*) = range(A^*A) a_adj - a_adj*a*a_dag a_adj*a - a_adj*a_dag_adj*a_adj*a Factorisations to show range(A^*A) = range(A^\dag A) a_adj*a - a_dag*a*a_adj*a a_dag*a - a_adj*a*a_dag*a_dag_adj Proof of (c): Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! Proof of (d): Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified!

Reverse Order Law for Full Rank Decomposition (Fact 23 in [Hog13, Sec. I.5.7])

If A=BCA = BC is a full rank decomposition, i.e., BB has full column rank and CC has full row rank, then A†=C†B†A^\dag = C^\dag B^\dag. 

F.<a, b, c, i, u, v, x, y, z, a_adj, b_adj, c_adj, i_adj, u_adj, v_adj, x_adj, y_adj, z_adj> = FreeAlgebra(QQ)

Pinv_a = pinv(a, x, a_adj, x_adj)
Pinv_b = pinv(b, y, b_adj, y_adj)
Pinv_c = pinv(c, z, c_adj, z_adj)
rank_decomp = [a - b*c, u*b - i, c*v - i]
id = [i*i - i, i - i_adj, b*i - b, i*y - y, i*c - c, z*i - z, i*u - u, v*i - v]

assumptions = add_adj(Pinv_a + Pinv_b + Pinv_c + rank_decomp + id)
claim = x - z*y

Q = Quiver([(1, 2, u) for u in [a, x_adj]] + 
           [(2, 1, u) for u in [a_adj, x]] + 
           [(1, 3, u) for u in [c, v_adj, z_adj]] + 
           [(3, 1, u) for u in [c_adj, v, z]] + 
           [(2, 3, u) for u in [b_adj, u, y]] + 
           [(3, 2, u) for u in [b, u_adj, y_adj]] + 
           [(3, 3, u) for u in [i, i_adj]])

proof = certify(assumptions, claim, Q)
print("The proof consists of %d steps." % len(proof))
Computing a (partial) Groebner basis and reducing the claims... Starting iteration 5... Done! Ideal membership of all claims could be verified! The proof consists of 37 steps.

Moore-Penrose Inverse of Gram Matrix (Fact 24 in [Hog13, Sec. I.5.7])

It holds that (A∗A)†=A†(A∗)†(A^*A)^\dagger = A^\dagger (A^*)^\dagger.

# inverse of gramian

F.<a, a_adj, a_dag, a_dag_adj, a_adj_dag, a_adj_dag_adj, b, b_adj, b_dag, b_dag_adj> = FreeAlgebra(QQ)

Pinv_a = pinv(a, a_dag, a_adj, a_dag_adj)
Pinv_a_adj = pinv(a_adj, a_adj_dag, a, a_adj_dag_adj)
Pinv_b = pinv(b, b_dag, b, b_dag_adj)

assumptions = add_adj(Pinv_a + Pinv_a_adj + Pinv_b + [b - a_adj*a])
claim = b_dag - a_dag*a_adj_dag
Q = Quiver([(1, 2, u) for u in [a, a_dag_adj, a_adj_dag]] + 
           [(2, 1, u) for u in [a_adj, a_dag, a_adj_dag_adj]] + 
           [(1, 1, u) for u in [b, b_adj, b_dag, b_dag_adj]])

proof = certify(assumptions, claim, Q)
print("The proof consists of %d steps." % len(proof))
Computing a (partial) Groebner basis and reducing the claims... Starting iteration 5... Starting iteration 10... Done! Ideal membership of all claims could be verified! The proof consists of 226 steps.

Reverse Order Law for Moore-Penrose Inverse (Fact 25 in [Hog13, Sec. I.5.7])

Each one of the following conditions is necessary and sufficient for (AB)†=B†A†(AB)^\dag = B^\dag A^\dag:

  1. range(BB∗A∗)⊆range(A∗)\text{range}(BB^\ast A^\ast) \subseteq \text{range}(A^\ast) and range(A∗AB)⊆range(B)\text{range}(A^\ast AB) \subseteq \text{range}(B).

  2. A†ABB∗A^\dag ABB^\ast and A∗ABB†A^\ast A BB^\dag are both Hermitian matrices.

  3. A†ABB∗A∗=BB∗A∗A^\dag ABB^\ast A^\ast = BB^\ast A^\ast and BB†A∗AB=A∗ABBB^\dag A^\ast AB = A^\ast AB.

  4. A†ABB∗A∗ABB†=BB∗A∗AA^\dag ABB^\ast A^\ast ABB^\dag = BB^\ast A^\ast A.

  5. A†AB=B(AB)†ABA^\dag AB = B (AB)^\dag AB and BB†A∗=A∗AB(AB)†BB^\dag A^\ast = A^\ast AB (AB)^\dag.

We show ((AB)†=B†A†)⇔(3)⇒(4)⇒(5)⇒(1)⇒(2)⇒(3)( (AB)^\dag = B^\dag A^\dag) \Leftrightarrow (3) \Rightarrow (4) \Rightarrow (5) \Rightarrow (1) \Rightarrow (2) \Rightarrow (3).

#basic definitions
F.<a,b,a_dag,b_dag,ab_dag,a_adj,b_adj,a_dag_adj,b_dag_adj,ab_dag_adj,u,u_adj,v,v_adj> = FreeAlgebra(QQ)

# quiver encoding the variables
Q = Quiver(
           [(1, 1, x) for x in [v, v_adj]] +
           [(1, 2, x) for x in [b, b_dag_adj]] + 
           [(2, 1, x) for x in [b_adj, b_dag]] + 
           [(2, 3, x) for x in [a, a_dag_adj]] + 
           [(3, 2, x) for x in [a_adj,a_dag]] + 
           [(3, 3, x) for x in [u, u_adj]] +
           [(1, 3, ab_dag_adj), (3, 1, ab_dag)])

Pinv_a = pinv(a, a_dag, a_adj, a_dag_adj)
Pinv_b = pinv(b, b_dag, b_adj, b_dag_adj)
Pinv_ab = pinv(a*b, ab_dag, b_adj*a_adj, ab_dag_adj)

basic_assumptions = Pinv_a + Pinv_b + Pinv_ab

rol = [ab_dag - b_dag * a_dag]
cond_1 = [b*b_adj*a_adj - a_adj*u, a_adj*a*b - b*v]
cond_2 = [a_dag*a*b*b_adj - b*b_adj*a_adj*a_dag_adj, a_adj*a*b*b_dag - b_dag_adj*b_adj*a_adj*a]
cond_3 = [a_dag*a*b*b_adj*a_adj - b*b_adj*a_adj, b*b_dag*a_adj*a*b - a_adj*a*b]
cond_4 = [a_dag*a*b*b_adj*a_adj*a*b*b_dag - b*b_adj*a_adj*a]
cond_5 = [a_dag*a*b - b*ab_dag*a*b, b*b_dag*a_adj - a_adj*a*b*ab_dag]

To prove the implication ((AB)†=B†A†)  ⟹  (3)( (AB)^\dag = B^\dag A^\dag) \implies (3), we first show the following lemma:

Lemma: If AA has a Moore-Penrose inverse, then A∗A=AA∗=0  ⟹  A=0A^*A = AA^* = 0 \implies A = 0.

# proof of lemma
assumptions = add_adj(pinv(a, a_dag, a_adj, a_dag_adj) + [a_adj*a])
proof = certify(assumptions,a)
Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified!

Since every matrix has a Moore-Penrose inverse, we can apply the lemma above to any expression. In particular, instead of proving the identities P=QP = Q appearing in condition 3, we can also show that (P−Q)∗(P−Q)=0(P-Q)^\ast (P - Q) = 0, from which we can conclude P−Q=0P - Q = 0, or equivalently P=QP = Q.

# (ROL) => (3)
assumptions = add_adj(basic_assumptions + rol)
claims = [adj(f)*f for f in cond_3]
proofs = certify(assumptions, claims, Q)
print("\nThe proofs consist of %s steps respectively." % str(list(map(len,proofs))))
Computing a (partial) Groebner basis and reducing the claims... Starting iteration 5... Done! Ideal membership of all claims could be verified! The proofs consist of [7, 7] steps respectively. 
# (3) => (ROL)
assumptions = add_adj(basic_assumptions + cond_3)
claims = rol
proofs = certify(assumptions, claims, Q, maxiter=20)
print("\nThe proofs consist of %s steps respectively." % str(list(map(len,proofs))))
Computing a (partial) Groebner basis and reducing the claims... Starting iteration 5... Starting iteration 10... Done! Ideal membership of all claims could be verified! The proofs consist of [36] steps respectively. 
# (3) => (4)
assumptions = add_adj(basic_assumptions + cond_3)
claims = cond_4
proofs = certify(assumptions, claims, Q)
print("\nThe proofs consist of %s steps respectively." % str(list(map(len,proofs))))
Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! The proofs consist of [3] steps respectively. 
# (4) => (5)
assumptions = add_adj(basic_assumptions + cond_4)
claims = cond_5
proofs = certify(assumptions, claims, Q, maxiter=50)
print("\nThe proofs consist of %s steps respectively." % str(list(map(len,proofs))))
Computing a (partial) Groebner basis and reducing the claims... Starting iteration 5... Starting iteration 10... Starting iteration 15... Done! Ideal membership of all claims could be verified! The proofs consist of [9, 13] steps respectively. 
# (5) => (1)
assumptions = add_adj(basic_assumptions + cond_5)
I = NCIdeal(assumptions)
range_inclusion_1 = I.find_equivalent_expression(b*b_adj*a_adj,prefix=a_adj,heuristic='naive',maxiter=20,quiver=Q)[0]
range_inclusion_2 = I.find_equivalent_expression(a_adj*a*b,prefix=b,heuristic='naive',maxiter=20,quiver=Q)[0]
print("\nFactorisations to show the range inclusions")
print(range_inclusion_1)
print(range_inclusion_2)
Factorisations to show the range inclusions b*b_adj*a_adj - a_adj*a_dag_adj*b*b_adj*a_adj a_adj*a*b - b*b_dag*a_adj*a*b 
# (1) => (2)
assumptions = add_adj(basic_assumptions + cond_1)
claims = cond_2
proofs = certify(assumptions, claims, Q)
print("\nThe proofs consist of %s steps respectively." % str(list(map(len,proofs))))
Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! The proofs consist of [8, 8] steps respectively. 
# (2) => (3)
assumptions = add_adj(basic_assumptions + cond_2)
claims = cond_3
proofs = certify(assumptions, claims, Q)
print("\nThe proofs consist of %s steps respectively." % str(list(map(len,proofs))))
Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! The proofs consist of [2, 3] steps respectively.

Reverse Order Law ([DD10, Thm. 2.2 – 2.4])

The following statement combines the main results of Theorem 2.2 – 2.4 in [DD10].

Let X,Y,ZX,Y,Z be Hilbert spaces, and let A:Y→ZA: Y \to Z and B:X→YB: X \to Y be bounded linear operators such that AA, BB, ABAB have closed ranges. Then the following statements are equivalent:

  1. (AB)†=B†A†(AB)^\dagger = B^\dagger A^\dagger

  2. AB(AB)†=ABB†A†AB(AB)^\dagger = ABB^\dagger A^\dagger and (AB)†AB=B†A†AB(AB)^\dagger AB = B^\dagger A^\dagger AB

  3. A∗AB=BB†A∗ABA^* AB = B B^\dagger A^* AB and ABB∗=ABB∗A†AABB^* = ABB^* A^\dagger A

  4. R(A∗AB)⊆R(B)\mathcal{R}(A^*AB) \subseteq \mathcal{R}(B) and R(BB∗A∗)⊆R(A∗)\mathcal{R}(BB^*A^*) \subseteq \mathcal{R}(A^*)

  5. AB(AB)†A=ABB†AB(AB)^\dagger A = ABB^\dagger and B(AB)†AB=A†ABB(AB)^\dagger AB = A^\dagger AB

  6. A∗ABB†=BB†A∗AA^* ABB^\dagger = BB^\dagger A^*A and A†ABB∗=BB∗A†AA^\dagger ABB^* = BB^*A^\dagger A

  7. (ABB†)†=BB†A†(ABB^\dagger)^\dagger = BB^\dagger A^\dagger and (A†AB)†=B†A†A(A^\dagger AB)^\dagger = B^\dagger A^\dagger A

  8. B†(ABB†)†=B†A†B^\dagger (ABB^\dagger)^\dagger = B^\dagger A^\dagger and (A†AB)†A†=B†A†(A^\dagger AB)^\dagger A^\dagger = B^\dagger A^\dagger

In the following, we show

(1)⇒(2)⇒(3)⇒(4)⇒(5)⇒(6)⇒(7)⇒(8)⇒(1)(1) \Rightarrow(2) \Rightarrow(3) \Rightarrow (4) \Rightarrow(5) \Rightarrow(6) \Rightarrow(7) \Rightarrow(8) \Rightarrow(1).

#basic definitions
F.<a, b, c, d, a_dag, b_dag, ab_dag, c_dag, d_dag, a_adj, b_adj, c_adj, d_adj, a_dag_adj, b_dag_adj, ab_dag_adj, c_dag_adj, d_dag_adj,u,u_adj,v,v_adj> = FreeAlgebra(QQ)

# quiver encoding the variables
Q = Quiver(
           [(1, 1, x) for x in [u, u_adj]] +
           [(1, 2, x) for x in [b, d_dag_adj, b_dag_adj, d]] + 
           [(2, 1, x) for x in [b_adj, d_dag, b_dag, d_adj]] + 
           [(2, 3, x) for x in [a, c_dag_adj, a_dag_adj, c]] + 
           [(3, 2, x) for x in [a_adj, c_dag, a_dag, c_adj]] + 
           [(3, 3, x) for x in [v, v_adj]] +
           [(1, 3, ab_dag_adj), (3, 1, ab_dag)])

Pinv_a = pinv(a, a_dag, a_adj, a_dag_adj)
Pinv_b = pinv(b, b_dag, b_adj, b_dag_adj)
Pinv_ab = pinv(a*b, ab_dag, b_adj*a_adj, ab_dag_adj)

# c = a*b*b_dag
def_c = [c - a*b*b_dag, c_adj - b_dag_adj*b_adj*a_adj]
Pinv_c = pinv(c, c_dag, c_adj, c_dag_adj)

# d = a_dag*a*b
def_d = [d - a_dag*a*b, d_adj - b_adj*a_adj*a_dag_adj]
Pinv_d = pinv(d, d_dag, d_adj, d_dag_adj)

basic_assumptions = Pinv_a + Pinv_b + Pinv_ab

cond_1 = [ab_dag - b_dag*a_dag]
cond_2 = [a*b*ab_dag - a*b*b_dag*a_dag, ab_dag*a*b - b_dag*a_dag*a*b]
cond_3 = [a_adj*a*b - b*b_dag*a_adj*a*b, a*b*b_adj - a*b*b_adj*a_dag*a]
cond_4 = [a_adj*a*b - b*u, b*b_adj*a_adj- a_adj*v]
cond_5 = [a*b*ab_dag*a - a*b*b_dag, b*ab_dag*a*b - a_dag*a*b]
cond_6 = [a_adj*a*b*b_dag - b*b_dag*a_adj*a, a_dag*a*b*b_adj - b*b_adj*a_dag*a]
cond_7 = [c_dag - b*b_dag*a_dag, d_dag - b_dag*a_dag*a]
cond_8 = [b_dag*c_dag - b_dag*a_dag, d_dag*a_dag - b_dag*a_dag]

# (1) => (2)
assumptions = add_adj(basic_assumptions + cond_1)
claims = cond_2
proofs = certify(assumptions, claims, Q, maxiter=50)
print("\nThe proofs consist of %s steps respectively." % str(list(map(len,proofs))))
Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! The proofs consist of [1, 1] steps respectively.

Remark: To prove the implication (2)  ⟹  (3)(2) \implies (3), we note that, for all bounded linear operators AA, we have

A∗A=AA∗=0  ⟹  A=0A^*A = AA^* = 0 \implies A = 0,

which follows from ∥A∥2=∥A∗A∥=∥AA∗∥\lVert A \rVert^2 = \lVert A^* A \rVert = \lVert AA^* \rVert.

Thus, instead of proving the identities P=QP = Q appearing in condition 3, we can also show that (P−Q)∗(P−Q)=0(P-Q)^\ast (P - Q) = 0, or (P−Q)(P−Q)∗=0(P-Q)(P-Q)^\ast = 0 from which we can conclude P−Q=0P - Q = 0, or equivalently P=QP = Q.

# (2) => (3)
# using the remark, we now show the ideal membership of f_adj*f and g*g_adj, where [f,g] = cond_3,
# with this the claim follows from the lemma
assumptions = add_adj(basic_assumptions + cond_2)
f,g = cond_3
claims = [adj(f)*f, g*adj(g)]
proofs = certify(assumptions, claims, Q, maxiter=20)
print("\nThe proofs consist of %s steps respectively." % str(list(map(len,proofs))))
Computing a (partial) Groebner basis and reducing the claims... Starting iteration 5... Starting iteration 10... Starting iteration 15... Done! Ideal membership of all claims could be verified! The proofs consist of [9, 9] steps respectively. 
# (3) => (4)
# to show the range inclusions of (4), we follow the strategy explained in the paper and find corresponding factorisations
# to show R(a_adj*a*b) \subseteq R(b), we find u such that a_adj*a*b - b*u is in the ideal
# to show R(b*b_adj*a_adj) \subseteq R(a_adj), we find v such that b*b_adj*a_adj- a_adj*v is in the ideal
assumptions = add_adj(basic_assumptions + cond_3)
I = NCIdeal(assumptions)
expression_u = I.find_equivalent_expression(a_adj*a*b)[0]
expression_v = I.find_equivalent_expression(b*b_adj*a_adj, prefix=a_adj)[0]
# we found expressions for u and v, showing the claimed range inclusions
print("u = %s" % str(expression_u))
print("v = %s" % str(expression_v))
u = - a_adj*a*b + b*b_dag*a_adj*a*b v = - b*b_adj*a_adj + a_dag*a*b*b_adj*a_adj 
# (4) => (5)
assumptions = add_adj(basic_assumptions + cond_4)
claims = cond_5
proofs = certify(assumptions, claims, Q, maxiter=50)
print("\nThe proofs consist of %s steps respectively." % str(list(map(len,proofs))))
Computing a (partial) Groebner basis and reducing the claims... Starting iteration 5... Done! Ideal membership of all claims could be verified! The proofs consist of [18, 7] steps respectively. 
# (5) => (6)
assumptions = add_adj(basic_assumptions + cond_5)
claims = cond_6
proofs = certify(assumptions, claims, Q, maxiter=50)
print("\nThe proofs consist of %s steps respectively." % str(list(map(len,proofs))))
Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! The proofs consist of [4, 4] steps respectively. 
# (6) => (7)
assumptions = add_adj(basic_assumptions + cond_6 + def_c + Pinv_c + def_d + Pinv_d)
claims = cond_7
proofs = certify(assumptions, claims, Q, maxiter=50)
print("\nThe proofs consist of %s steps respectively." % str(list(map(len,proofs))))
Computing a (partial) Groebner basis and reducing the claims... Starting iteration 5... Done! Ideal membership of all claims could be verified! The proofs consist of [172, 163] steps respectively. 
# (7) => (8)
assumptions = add_adj(basic_assumptions + cond_7 + def_c + Pinv_c + def_d + Pinv_d)
claims = cond_8
proofs = certify(assumptions, claims, Q, maxiter=50)
print("\nThe proofs consist of %s steps respectively." % str(list(map(len,proofs))))
Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! The proofs consist of [2, 2] steps respectively. 
# (8) => (1)
assumptions = add_adj(basic_assumptions + cond_8 + def_c + Pinv_c + def_d + Pinv_d)
claim = cond_1[0]
proof = certify(assumptions, claim, Q, maxiter=50)
print("\nThe proof consists of %d steps." % len(proof))
Computing a (partial) Groebner basis and reducing the claims... Starting iteration 5... Starting iteration 10... Starting iteration 15... Starting iteration 20... Done! Ideal membership of all claims could be verified! The proof consists of 279 steps.

Triple Reverse Order Law

Hartwig's original statement ([CIHHP+{}^+21, Thm. 2.1])

Let A,B,CA, B, C be complex matrices such that the product ABCABC is defined and let P=A†ABCC†P = A^\dag ABCC^\dag, Q=CC†B†A†AQ = C C^\dag B^\dag A^\dag A. The following conditions are equivalent:

  1. (ABC)†=C†B†A†(ABC)^\dag = C^\dag B^\dag A^\dag;

  2. PQP=PPQP = P, QPQ=QQPQ = Q, and both A∗APQA^* APQ and QPCC∗QPCC^* are Hermitian;

  3. PQP=PPQP = P, QPQ=QQPQ = Q, and both A∗APQA^* APQ and QPCC∗QPCC^* are EP;

  4. PQP=PPQP = P, R(A∗AP)=R(Q∗)\mathcal{R}(A^*AP)= \mathcal{R}(Q^*) and R(CC∗P∗)=R(Q)\mathcal{R}(CC^\ast P^\ast) = \mathcal{R}(Q);

  5. PQ=(PQ)2PQ = (PQ)^2, R(A∗AP)=R(Q∗)\mathcal{R}(A^*AP)= \mathcal{R}(Q^*) and R(CC∗P∗)=R(Q)\mathcal{R}(CC^\ast P^\ast) = \mathcal{R}(Q);

In the following, we show (1)⇔(2)⇔(3)(1) \Leftrightarrow(2) \Leftrightarrow (3) and (1)⇔(4)⇔(5)(1) \Leftrightarrow (4) \Leftrightarrow (5).

# basic definitions
F.<p,p_adj,q,q_adj,a,a_adj,a_dag,a_dag_adj,b,b_adj,b_dag,b_dag_adj,c,c_adj,c_dag,c_dag_adj,abc_dag,abc_dag_adj,t,t_adj,u,u_adj,v,v_adj,w,w_adj> = FreeAlgebra(QQ)

# quiver encoding the variables
Q = Quiver([(1, 2, x) for x in [c, c_dag_adj]] + 
           [(2, 1, x) for x in [c_adj, c_dag]] + 
           [(2, 2, x) for x in [v, v_adj, w, w_adj]] +
           [(2, 3, x) for x in [b, b_dag_adj, p, q_adj]] + 
           [(3, 2, x) for x in [b_adj, b_dag, p_adj, q]] + 
           [(3, 3, x) for x in [t, t_adj,u, u_adj]] +
           [(3, 4, x) for x in [a, a_dag_adj]] + 
           [(4, 3, x) for x in [a_adj, a_dag]] + 
           [(4, 1, x) for x in [abc_dag]] + 
           [(1, 4, x) for x in [abc_dag_adj]])

PQ = [p - a_dag * a * b * c * c_dag, q - c * c_dag * b_dag * a_dag * a]
abc = a * b * c
abc_adj = c_adj * b_adj * a_adj
Pinv_A = pinv(a, a_dag, a_adj, a_dag_adj)
Pinv_B = pinv(b, b_dag, b_adj, b_dag_adj)
Pinv_C = pinv(c, c_dag, c_adj, c_dag_adj)
Pinv_ABC = pinv(abc, abc_dag, abc_adj, abc_dag_adj)

cond_1 = [abc_dag - c_dag*b_dag*a_dag]
cond_2 = [p*q*p - p, q*p*q - q, a_adj*a*p*q - q_adj*p_adj*a_adj*a, q*p*c*c_adj - c*c_adj*p_adj*q_adj]
# encode equality of ranges via Douglas' lemma
cond_3 = [p*q*p - p, q*p*q - q, a_adj*a*p*q*t - q_adj*p_adj*a_adj*a, a_adj*a*p*q - q_adj*p_adj*a_adj*a*u,
         q*p*c*c_adj*v - c*c_adj*p_adj*q_adj, q*p*c*c_adj - c*c_adj*p_adj*q_adj*w]
cond_4 = [p*q*p - p, q*t - c*c_adj*p_adj, q - c*c_adj*p_adj*u,
        q_adj*v - a_adj*a*p,q_adj - a_adj*a*p*w]
cond_5 = [p*q*p*q - p*q, q*t - c*c_adj*p_adj, q - c*c_adj*p_adj*u,
        q_adj*v - a_adj*a*p,q_adj - a_adj*a*p*w]

# (1) => (2)
assumptions = add_adj(PQ + Pinv_A + Pinv_B + Pinv_C + Pinv_ABC + cond_1)
claims = cond_2
proofs = certify(assumptions, claims, Q, maxiter=50)
print("\nThe proofs consist of %s steps respectively." % str(list(map(len,proofs))))
Computing a (partial) Groebner basis and reducing the claims... Starting iteration 5... Starting iteration 10... Starting iteration 15... Starting iteration 20... Done! Ideal membership of all claims could be verified! The proofs consist of [44, 30, 21, 17] steps respectively. 
# (2) => (1)
assumptions = add_adj(PQ + Pinv_A + Pinv_B + Pinv_C + Pinv_ABC + cond_2)
claim = cond_1[0]
proof = certify(assumptions, claim, Q, maxiter=50)
print("\nThe proof consists of %d steps." % len(proof))
Computing a (partial) Groebner basis and reducing the claims... Starting iteration 5... Starting iteration 10... Starting iteration 15... Starting iteration 20... Starting iteration 25... Done! Ideal membership of all claims could be verified! The proof consists of 178 steps. 
# (2) => (3)
# holds trivially

# (3) => (2)
assumptions = add_adj(PQ + Pinv_A + Pinv_B + Pinv_C + Pinv_ABC + cond_3)
claims = cond_2
proofs = certify(assumptions, claims, Q, maxiter=50)
print("\nThe proofs consist of %s steps respectively." % str(list(map(len,proofs))))
Computing a (partial) Groebner basis and reducing the claims... Starting iteration 5... Done! Ideal membership of all claims could be verified! The proofs consist of [1, 1, 6, 6] steps respectively. 
# (1) => (4)
assumptions = add_adj(PQ + Pinv_A + Pinv_B + Pinv_C + Pinv_ABC + cond_1)
claims = cond_4

# first, prove the claim that NOT a range inclusion
proof = certify(assumptions, claims[0], Q, maxiter=50)
#print("\nThe proof consists of %d steps.\n" % len(proofs))

# next, show the range inclusions
# to this end, we need to find suitable expressions for the unknown variables
# two of these expressions can be found with the basic find_equivalent_expression
# command, using a suitable monomial order
basic_vars = [abc_dag,abc_dag_adj,a,a_adj,a_dag,a_dag_adj,b,b_adj,b_dag,b_dag_adj,c,c_adj,c_dag,c_dag_adj]
auxiliary_vars = [t,t_adj,u,u_adj,v,v_adj,w,w_adj]
pq_vars = [p,p_adj,q,q_adj]

I = NCIdeal(assumptions, order=[pq_vars+basic_vars, auxiliary_vars])

# R(A^* A P) = R(Q^*)
range_inclusion_1 = I.find_equivalent_expression(a_adj*a*p, maxiter=40)[0]
range_inclusion_2 = I.find_equivalent_expression(q_adj, prefix=a_adj*a*p, maxiter=40, heuristic='naive', quiver=Q, relevant_variables=pq_vars+basic_vars)[0]

# R(C C^* P^*) = R(Q)
range_inclusion_3 = I.find_equivalent_expression(c*c_adj*p_adj, maxiter=40)[0]
range_inclusion_4 = I.find_equivalent_expression(q, prefix=c*c_adj*p_adj, maxiter=40, heuristic='naive', quiver=Q, relevant_variables=pq_vars+basic_vars)[0]

print("\nThe following found expressions prove the range inclusions")
print(range_inclusion_1)
print(range_inclusion_2,"\n")
print(range_inclusion_3)
print(range_inclusion_4)
Computing a (partial) Groebner basis and reducing the claims... Starting iteration 5... Starting iteration 10... Starting iteration 15... Starting iteration 20... Done! Ideal membership of all claims could be verified! The following found expressions prove the range inclusions - a_adj*a*p + q_adj*p_adj*a_adj*a*p q_adj - a_adj*a*p*c*abc_dag*abc_dag_adj*c_adj - c*c_adj*p_adj + q*p*c*c_adj*p_adj q - c*c_adj*p_adj*q_adj*c_dag_adj*c_dag*q 
# (4) => (1)
assumptions = add_adj(PQ + Pinv_A + Pinv_B + Pinv_C + Pinv_ABC + cond_4)
claim = cond_1[0]
proof = certify(assumptions, claim, Q, maxiter=50)
print("\nThe proof consists of %d steps." % len(proof))
Computing a (partial) Groebner basis and reducing the claims... Starting iteration 5... Starting iteration 10... Starting iteration 15... Starting iteration 20... Starting iteration 25... Starting iteration 30... Starting iteration 35... Starting iteration 40... Done! Ideal membership of all claims could be verified! The proof consists of 525 steps. 
# (4) => (5)
assumptions = add_adj(PQ + Pinv_A + Pinv_B + Pinv_C + Pinv_ABC + cond_4)
claims = cond_5
proofs = certify(assumptions, claims, Q, maxiter=50)
print("\nThe proofs consist of %s steps respectively." % str(list(map(len,proofs))))
Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! The proofs consist of [1, 1, 1, 1, 1] steps respectively. 
# (5) => (4)
assumptions = add_adj(PQ + Pinv_A + Pinv_B + Pinv_C + Pinv_ABC + cond_5)
claims = cond_4
proofs = certify(assumptions, claims, Q, maxiter=50)
print("\nThe proofs consist of %s steps respectively." % str(list(map(len,proofs))))
Computing a (partial) Groebner basis and reducing the claims... Starting iteration 5... Starting iteration 10... Starting iteration 15... Starting iteration 20... Starting iteration 25... Starting iteration 30... Starting iteration 35... Done! Ideal membership of all claims could be verified! The proofs consist of [545, 1, 1, 1, 1] steps respectively.

Generalisation 1 ([CIHHP+{}^+21, Thm. 2.3])

Let R\mathcal{R} be a ring with involution ∗\ast. Let a,b,c∈Ra,b,c \in \mathcal{R} be such that a,ca,c are MP-invertible. Let p=a†abcc†p = a^\dag abc c^\dag and q=cc†b~a†aq = c c^\dag \tilde b a^\dag a, for b~∈R\tilde b \in \mathcal{R}. Then the following conditions are equivalent:

  1. abcabc is Moore-Penrose invertible and (abc)†=c†b†a†(abc)^\dag = c^\dag b^\dag a^\dag;

  2. pqp=ppqp = p, a∗apR⊇q∗Ra^\ast a p \mathcal{R} \supseteq q^*\mathcal{R} and cc∗p∗R⊆qRcc^\ast p^\ast \mathcal{R} \subseteq q\mathcal{R};

  3. abcabc is right ∗*-cancellable, pq=(pq)2pq = (pq)^2, a∗apR⊇q∗Ra^\ast a p \mathcal{R} \supseteq q^*\mathcal{R} and cc∗p∗R⊆qRcc^\ast p^\ast \mathcal{R} \subseteq q\mathcal{R};

  4. pqp=ppqp =p, qpq=qqpq = q, a∗apR⊇q∗Ra^\ast a p \mathcal{R} \supseteq q^*\mathcal{R} and cc∗p∗R⊆qRcc^\ast p^\ast \mathcal{R} \subseteq q\mathcal{R};

In the following, we show (1)⇒(2)⇒(3)⇒(4)⇒(1)(1) \Rightarrow(2) \Rightarrow (3) \Rightarrow (4) \Rightarrow (1).

# basic definitions
F.<p,p_adj,q,q_adj,a,a_adj,a_dag,a_dag_adj,b,b_adj,b_tilde,b_tilde_adj,c,c_adj,c_dag,c_dag_adj,u,u_adj,v,v_adj,z,z_adj> = FreeAlgebra(QQ)

# quiver encoding the variables
Q = Quiver([(1, 2, x) for x in [c, c_dag_adj]] + 
           [(2, 1, x) for x in [c_adj, c_dag]] + 
           [(2, 2, x) for x in [u, u_adj]] +
           [(2, 3, x) for x in [b, b_tilde_adj, p, q_adj]] + 
           [(3, 2, x) for x in [b_adj, b_tilde, p_adj, q]] + 
           [(3, 3, x) for x in [v, v_adj]] +
           [(3, 4, x) for x in [a, a_dag_adj]] + 
           [(4, 3, x) for x in [a_adj, a_dag]] + 
           [(4, 4, z), (4, 4, z_adj)])

PQ = [p - a_dag * a * b * c * c_dag, q - c * c_dag * b_tilde * a_dag * a]
abc = a * b * c
abc_adj = c_adj * b_adj * a_adj
Pinv_A = pinv(a, a_dag, a_adj, a_dag_adj)
Pinv_C = pinv(c, c_dag, c_adj, c_dag_adj)

cond_1 = pinv(abc, c_dag * b_tilde * a_dag, abc_adj, a_dag_adj * b_tilde_adj * c_dag_adj)
cond_2 = [p*q*p - p, a_adj*a*p*u - q_adj, c*c_adj*p_adj - q*v]
# leave out *-cancellability for now
cond_3 = [p*q - p*q*p*q,  a_adj*a*p*u - q_adj, c*c_adj*p_adj - q*v]
cond_4 = [p*q*p-p, q*p*q-q,  a_adj*a*p*u - q_adj, c*c_adj*p_adj - q*v]

# (1) => (2)
assumptions = add_adj(PQ + Pinv_A + Pinv_C + cond_1)
claims = cond_2

# first, prove the claim that NOT a range inclusion
proof = certify(assumptions, claims[0], Q, maxiter=50)
print("\nThe proof consists of %d steps." % len(proof))

# next, show the range inclusions
# to this end, we need to find suitable expressions for the unknown variables
# two of these expressions can be found with the basic find_equivalent_expression
# command, using a suitable monomial order
basic_vars = [abc_dag,abc_dag_adj,a,a_adj,a_dag,a_dag_adj,b,b_adj,b_tilde,b_tilde_adj,c,c_adj,c_dag,c_dag_adj]
auxiliary_vars = [u,u_adj,v,v_adj]
pq_vars = [p,p_adj,q,q_adj]

I = NCIdeal(assumptions, order=[pq_vars+basic_vars, auxiliary_vars])
# R(A^* A P) \supseteq R(Q^*)
range_inclusion_1 = I.find_equivalent_expression(q_adj, prefix=a_adj*a*p, maxiter=40, heuristic='naive', quiver=Q, relevant_variables=pq_vars+basic_vars)[0]

# R(C C^* P^*) \subseteq R(Q)
range_inclusion_2 = I.find_equivalent_expression(c*c_adj*p_adj, maxiter=40)[0]

print("\nThe following found expressions prove the range inclusions")
print(range_inclusion_1)
print(range_inclusion_2)
Computing a (partial) Groebner basis and reducing the claims... Starting iteration 5... Starting iteration 10... Done! Ideal membership of all claims could be verified! The proof consists of 43 steps. The following found expressions prove the range inclusions q_adj - a_adj*a*p*q*a_dag*a_dag_adj*q_adj - c*c_adj*p_adj + q*p*c*c_adj*p_adj 
# (2) => (3)
assumptions = add_adj(PQ + Pinv_A + Pinv_C + cond_2)
# first, prove all claims except the *-cancellability
claims = cond_3
proofs = certify(assumptions, claims, Q, maxiter=50)
print("\nThe proofs consist of %s steps respectively." % str(list(map(len,proofs))))

# for the *-cancellability, assume z(abc)(abc)^* = 0 and show z(abc) = 0
assumptions = add_adj(PQ + Pinv_A + Pinv_C + cond_2 + [z * abc * abc_adj])
claim = z * abc
proof = certify(assumptions, claim, Q, maxiter=50)
print("\nThe proof consists of %d steps." % len(proof))
Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! The proofs consist of [1, 1, 1] steps respectively. Computing a (partial) Groebner basis and reducing the claims... Starting iteration 5... Starting iteration 10... Starting iteration 15... Starting iteration 20... Starting iteration 25... Starting iteration 30... Done! Ideal membership of all claims could be verified! The proof consists of 61 steps. 
# (3) => (4)
assumptions = add_adj(PQ + Pinv_A + Pinv_C + cond_3)
claims = cond_4
I = NCIdeal(assumptions)
# apply the *-cancellability of abc to extend assumptions
cancel = I.apply_right_cancellability(abc, abc_adj, maxiter=30)
cancel = [f.to_native() for f in cancel]
# extend the assumptions by the found elements
assumptions = add_adj(PQ + Pinv_A + Pinv_C + cond_3 + cancel)
proofs = certify(assumptions,cond_4,Q,maxiter=40)
print("\nThe proofs consist of %s steps respectively." % str(list(map(len,proofs))))
Computing a (partial) Groebner basis and reducing the claims... Starting iteration 5... Starting iteration 10... Starting iteration 15... Done! Ideal membership of all claims could be verified! The proofs consist of [12, 80, 1, 1] steps respectively. 
# (4) => (1)
assumptions = add_adj(PQ + Pinv_A + Pinv_C + cond_4)
claims = cond_1
proofs = certify(assumptions, claims, Q, maxiter=50)
print("\nThe proofs consist of %s steps respectively." % str(list(map(len,proofs))))
Computing a (partial) Groebner basis and reducing the claims... Starting iteration 5... Starting iteration 10... Starting iteration 15... Done! Ideal membership of all claims could be verified! The proofs consist of [22, 23, 40, 26] steps respectively.

Generalisation 2 ([CIHHP+{}^+21, Thm. 2.4])

Let R\mathcal{R} be a ring with involution ∗\ast. Let a,b,c∈Ra,b,c \in \mathcal{R} be such that a,ca,c are MP-invertible. Let p=a†abcc†p = a^\dag abc c^\dag and q=cc†b~a†aq = c c^\dag \tilde b a^\dag a, for b~∈R\tilde b \in \mathcal{R}. Then the following conditions are equivalent:

  1. abcabc is Moore-Penrose invertible and (abc)†=c†b†a†(abc)^\dag = c^\dag b^\dag a^\dag;

  2. pqp=ppqp = p, a∗apR⊆q∗Ra^\ast a p \mathcal{R} \subseteq q^*\mathcal{R} and cc∗p∗R⊇qRcc^\ast p^\ast \mathcal{R} \supseteq q\mathcal{R};

  3. c†b~a†c^\dag \tilde b a^\dag is left ∗*-cancellable, pq=(pq)2pq = (pq)^2, a∗apR⊆q∗Ra^\ast a p \mathcal{R} \subseteq q^*\mathcal{R} and cc∗p∗R⊇qRcc^\ast p^\ast \mathcal{R} \supseteq q\mathcal{R};

  4. pqp=ppqp =p, qpq=qqpq = q, a∗apR⊆q∗Ra^\ast a p \mathcal{R} \subseteq q^*\mathcal{R} and cc∗p∗R⊇qRcc^\ast p^\ast \mathcal{R} \supseteq q\mathcal{R};

In the following, we show (1)⇒(2)⇒(3)⇒(4)⇒(1)(1) \Rightarrow(2) \Rightarrow (3) \Rightarrow (4) \Rightarrow (1).

# basic definitions
F.<p,p_adj,q,q_adj,a,a_adj,a_dag,a_dag_adj,b,b_adj,b_tilde,b_tilde_adj,c,c_adj,c_dag,c_dag_adj,abc_dag,abc_dag_adj,u,u_adj,v,v_adj,z,z_adj> = FreeAlgebra(QQ)

# quiver encoding the variables
Q = Quiver([(1, 2, x) for x in [c, c_dag_adj]] + 
           [(2, 1, x) for x in [c_adj, c_dag]] + 
           [(2, 2, x) for x in [u, u_adj]] +
           [(2, 3, x) for x in [b, b_tilde_adj, p, q_adj]] + 
           [(3, 2, x) for x in [b_adj, b_tilde, p_adj, q]] + 
           [(3, 3, x) for x in [v, v_adj]] +
           [(3, 4, x) for x in [a, a_dag_adj]] + 
           [(4, 3, x) for x in [a_adj, a_dag]] + 
           [(4, 1, x) for x in [abc_dag]] + 
           [(1, 4, x) for x in [abc_dag_adj]] +
           [(4, 4, z), (4, 4, z_adj)])

PQ = [p - a_dag * a * b * c * c_dag, q - c * c_dag * b_tilde * a_dag * a]
abc = a * b * c
abc_adj = c_adj * b_adj * a_adj
Pinv_A = pinv(a, a_dag, a_adj, a_dag_adj)
Pinv_C = pinv(c, c_dag, c_adj, c_dag_adj)

cond_1 = pinv(abc, c_dag * b_tilde * a_dag, abc_adj, a_dag_adj * b_tilde_adj * c_dag_adj)
cond_2 = [p*q*p - p, a_adj*a*p - q_adj*u, c*c_adj*p_adj*v - q]
# leave out *-cancellability for now
cond_3 = [p*q - p*q*p*q,  a_adj*a*p - q_adj*u, c*c_adj*p_adj*v - q]
cond_4 = [p*q*p-p, q*p*q-q,  a_adj*a*p - q_adj*u, c*c_adj*p_adj*v - q]

# (1) => (2)
assumptions = add_adj(PQ + Pinv_A + Pinv_C + cond_1)
claims = cond_2

# first, prove the claim that NOT a range inclusion
proof = certify(assumptions, claims[0], Q, maxiter=50)
print("\nThe proof consists of %d steps.\n" % len(proof))

# next, show the range inclusions
# to this end, we need to find suitable expressions for the unknown variables
# two of these expressions can be found with the basic find_equivalent_expression
# command, using a suitable monomial order
basic_vars = [abc_dag,abc_dag_adj,a,a_adj,a_dag,a_dag_adj,b,b_adj,b_tilde,b_tilde_adj,c,c_adj,c_dag,c_dag_adj]
auxiliary_vars = [u,u_adj,v,v_adj]
pq_vars = [p,p_adj,q,q_adj]

I = NCIdeal(assumptions, order=[pq_vars+basic_vars, auxiliary_vars])
# R(A^* A P) \supseteq R(Q^*)
range_inclusion_1 = I.find_equivalent_expression(a_adj*a*p, maxiter=40)[0]

# R(C C^* P^*) \subseteq R(Q)
range_inclusion_2 = I.find_equivalent_expression(q, prefix=c*c_adj*p_adj, maxiter=40, heuristic='naive', quiver=Q, relevant_variables=pq_vars+basic_vars)[0]

print("\nThe following found expressions prove the range inclusions")
print(range_inclusion_1)
print(range_inclusion_2)
Computing a (partial) Groebner basis and reducing the claims... Starting iteration 5... Starting iteration 10... Done! Ideal membership of all claims could be verified! The proof consists of 43 steps. The following found expressions prove the range inclusions - a_adj*a*p + q_adj*p_adj*a_adj*a*p q - c*c_adj*p_adj*q_adj*c_dag_adj*c_dag*q 
# (2) => (3)
assumptions = add_adj(PQ + Pinv_A + Pinv_C + cond_2)
# first, prove all claims except the *-cancellability
claims = cond_3
proofs = certify(assumptions, claims, Q, maxiter=50)
print("\nThe proofs consist of %s steps respectively." % str(list(map(len,proofs))))

m = c_dag * b_tilde * a_dag
m_adj = a_dag_adj * b_tilde_adj * c_dag_adj
# for the *-cancellability, assume m^*mz = 0 and show mz = 0
assumptions = add_adj(PQ + Pinv_A + Pinv_C + cond_2 + [m_adj * m * z])
claim = m * z
proof = certify(assumptions, claim, Q, maxiter=50)
print("\nThe proof consists of %d steps." % len(proof))
Computing a (partial) Groebner basis and reducing the claims... Done! Ideal membership of all claims could be verified! The proofs consist of [1, 1, 1] steps respectively. Computing a (partial) Groebner basis and reducing the claims... Starting iteration 5... Starting iteration 10... Starting iteration 15... Starting iteration 20... Starting iteration 25... Starting iteration 30... Done! Ideal membership of all claims could be verified! The proof consists of 32 steps. 
# (3) => (4)
assumptions = add_adj(PQ + Pinv_A + Pinv_C + cond_3)
claims = cond_4
I = NCIdeal(assumptions)
# apply the *-cancellability of abc to extend assumptions
m = c_dag * b_tilde * a_dag
m_adj = a_dag_adj * b_tilde_adj * c_dag_adj
cancel = I.apply_left_cancellability(m_adj, m, maxiter=30)
cancel = [f.to_native() for f in cancel]
# extend the assumptions by the found elements
assumptions = add_adj(PQ + Pinv_A + Pinv_C + cond_3 + cancel)
proofs = certify(assumptions,cond_4,Q,maxiter=40)
print("\nThe proofs consist of %s steps respectively." % str(list(map(len,proofs))))
Computing a (partial) Groebner basis and reducing the claims... Starting iteration 5... Starting iteration 10... Starting iteration 15... Starting iteration 20... Done! Ideal membership of all claims could be verified! The proofs consist of [65, 17, 1, 1] steps respectively. 
# (4) => (1)
assumptions = add_adj(PQ + Pinv_A + Pinv_C + cond_4)
claims = cond_1
proofs = certify(assumptions, claims, Q, maxiter=50)
print("\nThe proofs consist of %s steps respectively." % str(list(map(len,proofs))))
Computing a (partial) Groebner basis and reducing the claims... Starting iteration 5... Starting iteration 10... Starting iteration 15... Done! Ideal membership of all claims could be verified! The proofs consist of [22, 23, 32, 36] steps respectively.

References

[Hog13] Hogben L., Handbook of Linear Algebra. CRC press, 2 edn. (2013)

[DD10] Djordjević, D.S., Dinčić, N.Č.: Reverse order law for the Moore-Penrose inverse. J. Math. Anal. Appl. 361(1), 252–261 (2010)

[CIHHP +{}^+ 21] Cvetković-Ilić, D. S., Hofstadler, C., Hossein Poor, J., Milošević, J., Raab, C. G., Regensburger, G.: Algebraic proof methods for identities of matrices and operators: improvements of Hartwig’s triple reverse order law. Appl. Math. Comput. 409, 126357 (2021)