adj_cj
plain-language theorem explainer
Adjugation and conjugation commute on 2×2 matrices over Z/3Z: adj(cj_G(X)) equals cj_G(adj X), with no determinant hypothesis. Downstream commutator-conjugation identities in the Loom invariant cite it. The proof is a one-line simp that unfolds conjugation and applies the multiplicative and involutive laws for the adjugate.
Claim. For all $2\times 2$ matrices $G,X$ with entries in $\mathbb{Z}/3\mathbb{Z}$, $\mathrm{adj}(\mathrm{cj}_G(X)) = \mathrm{cj}_G(\mathrm{adj}\, X)$, where $\mathrm{cj}_G$ denotes conjugation by $G$ written with the adjugate in place of an inverse.
background
Loom is a certificate language for finished configurations of closed recognition walks on the eight-state, three-axis window fixed by the forcing chain. Closed walks up to free reduction and simultaneous conjugation form the content; the module supplies a total well-formedness checker and a computable invariant valued in traces in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$, including traces of pairwise commutators.
Mat is an explicit four-component $2\times 2$ matrix over $\mathbb{Z}/3\mathbb{Z}$ (not Mathlib Matrix), chosen so kernel evaluation of thousands of products stays cheap. Conjugation cj G X is the usual sandwich $G X (\mathrm{adj}, G)$; the adjugate is used because it is total and, on determinant-one matrices, recovers the inverse. The identities adj_mul (adjugate of a product) and adj_adj (adjugate is an involution up to the usual scalar, here an identity on this ring) are available unconditionally.
proof idea
One-line wrapper. Unfold the definition of conjugation, then simp with adj_mul, adj_adj, and mul_assoc. The two adjugate laws rearrange the sandwich so the outer adjugate slides onto $X$ while the conjugating factors reassemble as cj G (adj X). No determinant hypothesis is needed because both adjugate identities hold for every matrix.
why it matters
The Loom invariant is blind to simultaneous conjugation of every loop by the same word; that blindness is a ring identity (trace is a class function), not a canonicalisation. Commutator traces supply the depth-two data that plain loop traces fail to separate. This lemma is the adjugate half of that story: it lets conjugation pass through the adjugate factors inside the commutator formula.
Its sole recorded consumer is comm_cj, which states that the commutator of two conjugates equals the conjugate of the commutator (under $\det G = 1$). Without adj_cj, that rewrite cannot open the comm definition. In the broader Recognition picture this sits under the eight-tick octave and the free group of rank five on the window: it is pure matrix algebra supporting the certificate, not a new forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.