Nonsolvability of GL₂

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

Main declarations

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

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

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

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

The general linear group GL₂ over an infinite field is not solvable.