adj_adj
plain-language theorem explainer
Applying the adjugate twice recovers the original matrix with entries in Z/3Z. Anyone using conjugation or inverses in the Loom SL(2,Z/3) representation cites this involution. The proof is a four-component ring calculation after unfolding the adjugate definition.
Claim. For every $2\times 2$ matrix $X$ with entries in $\mathbb{Z}/3\mathbb{Z}$, $\mathrm{adj}(\mathrm{adj}(X))=X$, where $\mathrm{adj}\begin{pmatrix}a&b\\c&d\end{pmatrix}=\begin{pmatrix}d&-b\\-c&a\end{pmatrix}$.
background
Loom treats closed recognition walks on the eight-state, three-axis window as words in a free group of rank five, then reads finished configurations through matrices in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$. Trace is the class function that makes the invariant blind to conjugation; the inverse of a unit-determinant matrix is its adjugate, so adjugate identities are the algebraic engine of gauge blindness.
Mat stores the four entries $a,b,c,d\in\mathbb{Z}/3\mathbb{Z}$ as a structure rather than a Mathlib matrix, so thousands of kernel products stay cheap. The adjugate is the total map $(a,b,c,d)\mapsto(d,-b,-c,a)$. Componentwise equality is packaged as a four-hypothesis constructor used throughout the file.
proof idea
Case-split on the four-field structure. Discharge equality by the componentwise constructor, then for each of the four goals unfold the adjugate and finish by the ring tactic on $\mathbb{Z}/3\mathbb{Z}$ (double negation cancels). No external lemmas beyond that constructor and the adjugate definition.
why it matters
This involution is the reason conjugation by a unit-determinant matrix can be written $G X,\mathrm{adj}(G)$ and still commute with taking adjugates: the parent identity that conjugation commutes with the adjugate is a one-line rewrite using this fact and the multiplicative rule for adjugates. Downstream, the same identity shows that simultaneous reversal of every loop is invisible to the depth-two trace invariant, because in this group the inverse is the adjugate; the gate can therefore treat reversal as gauge at no cost. That supports the Loom claim that the computable invariant is blind exactly to the two non-content operations (free reduction and basepoint change) on closed recognition walks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.