adj_mul
plain-language theorem explainer
The adjugate reverses products of 2×2 matrices: adj(XY) equals adj(Y) adj(X), with no determinant hypothesis. Loom conjugation and inverse-word evaluation cite this constantly. The proof destructures both matrices and closes the four entries by ring arithmetic.
Claim. Let $X,Y$ be $2\times 2$ matrices with entries in $\mathbb{Z}/3\mathbb{Z}$. Writing $\mathrm{adj}\begin{pmatrix}a&b\\c&d\end{pmatrix}=\begin{pmatrix}d&-b\\-c&a\end{pmatrix}$, one has $\mathrm{adj}(XY)=\mathrm{adj}(Y)\,\mathrm{adj}(X)$.
background
Loom is a certificate language for closed recognition walks on the eight-state, three-axis window. Configurations are finite lists of freely reduced words in five signed generators; the computable invariant reads traces and pairwise-commutator traces in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$, so conjugation-blindness is a ring identity rather than a canonicalisation.
Mat is a four-component record $(a,b,c,d)$ over $\mathbb{Z}/3\mathbb{Z}$, preferred to Mathlib matrices because later kernel evaluation multiplies thousands of them. The adjugate is the total map $\mathrm{adj}(X)=\langle d,-b,-c,a\rangle$; it is the inverse precisely when $\det=1$, which holds for every matrix the module evaluates. Equality of matrices is componentwise via eq_of.
The classical identity $\mathrm{adj}(XY)=\mathrm{adj}(Y),\mathrm{adj}(X)$ holds over any commutative ring and needs no unit-determinant hypothesis; that is exactly what keeps conjugation arguments short.
proof idea
Term-mode proof by cases on both matrix constructors, then eq_of to reduce matrix equality to four scalar goals. Each goal is discharged by simp only on the local multiplication and adjugate definitions, followed by ring on $\mathbb{Z}/3\mathbb{Z}$. No external lemmas beyond the in-module definitions are required.
why it matters
This is the algebraic hinge for basepoint change. Conjugation is defined as $\mathrm{cj}(G,X)=G X,\mathrm{adj}(G)$; the theorem adj_cj (conjugation commutes with adjugate, no hypotheses) is a one-line rewrite through adj_mul and adj_adj. Downstream, evalWord_invWord identifies the image of an inverted word with the adjugate of the forward image, and trN_comm_adj shows that reversing every loop is invisible to the commutator-trace invariant, because in this group the inverse is the adjugate.
In the Loom story that means free reduction and simultaneous conjugation (the two non-content operations) stay invisible to the certificate. The module doc ties this to the free group of rank five on the eight-tick window and to the refusal to let observables depend on basepoint labels. Without the reverse-order product law the component expansions of conjugated words do not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.