The quotient of $ by the full twist squared has no proper quotient
OpenBurauFaithful.braid_three_fullTwistQuotient_surjection_injectiveThe trefoil quotient of \mathrm{SL}(2,\mathbb Z)$.
Let $ be Artin's braid group on three strands and let
\Delta^4 = (\sigma_1\sigma_2)^6
be the full twist squared. Write
Q = B_3 \big/ \langle!\langle \Delta^4 \rangle!\rangle
for the quotient by its normal closure. The claim is that every surjective homomorphism is injective, i.e. $ has no proper quotient isomorphic to the modular group.
The reason is structural. The images = \begin{pmatrix} 0 & -1 \ 1 & 0\end{pmatrix} of the standard generators generate , so is generated by the two classes of and , which satisfy exactly the amalgam relations
s^4 = 1, \qquad u^6 = 1, \qquad s^2 = u^3
with = \sigma_0^2\sigma_1 in is the amalgamated product *_{C_2} C_6$, the standard presentation
\mathrm{SL}(2,\mathbb Z) ;=; \langle S, R \mid S^4 = 1,; R^3 = S^2 \rangle
of the modular group, with \mapsto \begin{pmatrix} 0 & -1 \ 1 & 0\end{pmatrix}. So \cong \mathrm{SL}(2,\mathbb Z)$.
Finally, is finitely generated and residually finite (it is linear over , and reduction of matrix entries modulo a prime bigger than the entries of - 1), and by Mal'cev's theorem a finitely generated residually finite group is Hopfian: every surjective endomorphism is injective. Composing a surjection with an isomorphism yields a surjective endomorphism of \varphi$ itself is injective.
This is the group-theoretic core of the description of the kernel of the = -1\psi : Q \twoheadrightarrow \mathrm{SL}(2,\mathbb Z)\Delta^4$.
import Definitions.Def_BurauFaithful_UnreducedBurau set_option autoImplicit false open Matrix BraidsLinksMCG
theorem BurauFaithful.braid_three_fullTwistQuotient_surjection_injective
(φ : (BraidsLinksMCG.ArtinBraidGroup 3 ⧸
Subgroup.normalClosure
({(BraidsLinksMCG.sigma (n := 3) ⟨0, by decide⟩ *
BraidsLinksMCG.sigma (n := 3) ⟨1, by decide⟩) ^ 6} :
Set (BraidsLinksMCG.ArtinBraidGroup 3))) →*
Matrix.SpecialLinearGroup (Fin 2) ℤ)
(hφ : Function.Surjective φ) : Function.Injective φ := by sorry