OAI/GroupTheory/PolycyclicRecognition/Algebra/ConnectedSolvableEigenvector.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A common eigenvector for a connected solvable matrix action

Induct on the derived length. The connected derived subgroup has a common eigenspace. The whole group preserves it, and acts there with scalar commutators. Those commutators are trivial by connectedness and determinant one, leaving a commuting action on this nonzero subspace.

  1. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.connected_solvable_commonEigenspace_of_bound line 20
  2. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.connected_solvable_commonEigenspace line 106