OAI/GroupTheory/PolycyclicRecognition/Algebra/ConnectedScalarCommutators.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Scalar commutators of a connected matrix group are trivial

On an invariant subspace a scalar commutator is a root of unity by its determinant. For each vector its orbit under these commutators is therefore finite. Polynomial continuity and connectedness make this orbit constant.

  1. def OAI.PolycyclicRecognition.PolynomialMatrixGroup.vectorPolynomial line 22
  2. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.continuous_vectorAction line 25
  3. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.finite_power_eq_one line 39
  4. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.connected_scalar_commutators_trivial line 44