Nonsolvability of SL₂

If a field contains an element a with a ≠ 0 and a² ≠ 1, then SL₂ is nonsolvable. In particular, this holds over every infinite field.

Main declarations

• TauCeti.Matrix.SpecialLinearGroup.not_isSolvable_fin_two: SL₂ is not solvable when the field contains an element outside the roots of X * (X² - 1).
• TauCeti.Matrix.SpecialLinearGroup.not_isSolvable_fin_two_of_infinite: the infinite-field specialization.

theorem TauCeti.Matrix.SpecialLinearGroup.not_isSolvable_fin_two (F : Type u) [Field F] (hF : ∃ (a : F), a ≠ 0 ∧ a ^ 2 ≠ 1) : ¬Group.IsSolvable (Matrix.SpecialLinearGroup (Fin 2) F)

The special linear group SL₂(F) is not solvable if F contains a nonzero element whose square is not one.

theorem TauCeti.Matrix.SpecialLinearGroup.not_isSolvable_fin_two_of_infinite (F : Type u) [Field F] [Infinite F] : ¬Group.IsSolvable (Matrix.SpecialLinearGroup (Fin 2) F)

The special linear group SL₂ over an infinite field is not solvable.