cj_mul
plain-language theorem explainer
Conjugation by a determinant-one matrix is a monoid homomorphism on 2×2 matrices over Z/3Z: cj_G(X)·cj_G(Y)=cj_G(X·Y). Loom invariant proofs cite it to push conjugation inside products and commutators. The argument is a short cancellation: adj G·G=1 collapses the middle factors after unfolding cj.
Claim. Let $G,X,Y$ be $2\times 2$ matrices over $\mathbb{Z}/3\mathbb{Z}$ with $\det G=1$. Writing $\mathrm{cj}_G(M)$ for conjugation of $M$ by $G$ (via the adjugate inverse), one has $\mathrm{cj}_G(X)\,\mathrm{cj}_G(Y)=\mathrm{cj}_G(X Y)$.
background
Loom treats finished recognition histories as finite lists of freely reduced words in five signed generators (the free group of rank $E-V+1=5$ on the eight-state, three-axis window). Content is quotiented by free reduction and by simultaneous conjugation of every loop, so that spelling and basepoint are not observables. The computable invariant lands in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$: it records loop traces and traces of pairwise commutators.
Mat is the hand-rolled $2\times 2$ matrix type over $\mathbb{Z}/3\mathbb{Z}$ (components $a,b,c,d$), chosen so kernel evaluation of thousands of products stays cheap. Conjugation $\mathrm{cj}_G$ is the usual $G M G^{-1}$ written with the adjugate; the hypothesis $\det G=1$ supplies the inverse identity $\mathrm{adj},G\cdot G=1$ used below. Trace is a class function, so conjugation-blindness is a ring identity rather than a canonicalisation step.
proof idea
From $\det G=1$ obtain $\mathrm{adj},G\cdot G=1$ via adj_mul_of_det_one. Unfold the definition of conjugation on both sides and normalise associations with mul_assoc. The product $\mathrm{cj}_G(X),\mathrm{cj}_G(Y)$ then contains the contiguous block $\mathrm{adj},G\cdot G$ in the middle; rewrite that block to $1$ and cancel with one_mul, leaving $\mathrm{cj}_G(X Y)$. Purely algebraic; no case splits on $\mathbb{Z}/3\mathbb{Z}$.
why it matters
Parent use is comm_cj in the same module: commutators of conjugates equal the conjugate of the commutator, proved by three applications of this homomorphism law plus adj_cj. That identity is what lets the Loom invariant (loop traces plus pairwise commutator traces) ignore simultaneous conjugation of every generator word. Module doc ties the move to the basepoint-non-content premise and to Loom.BasepointForced / rotate_is_conjugation: closed walks are circle maps, so prefix conjugation is forced; extending to arbitrary conjugators is the same label-blindness already used for the 48 window automorphisms. Without the monoid law, the depth-two lower-central data would not descend to conjugation classes, and the certificate checker could not treat basepoint as non-content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.