OAI/GroupTheory/PolycyclicRecognition/Algebra/PolynomialMatrixStabilizer.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Closed linear stabilizers in the polynomial matrix topology

Membership of a matrix translate in a subspace is a family of polynomial equations, obtained from its annihilating linear functionals. Consequently the finite-index common eigenspace stabilizer is dense and fixes that eigenspace under a connected matrix group.

  1. def OAI.PolycyclicRecognition.PolynomialMatrixGroup.linearAction line 21
  2. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.linearAction_apply line 26
  3. def OAI.PolycyclicRecognition.PolynomialMatrixGroup.functionalPolynomial line 29
  4. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.eval_functionalPolynomial line 34
  5. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.isClosed_linearAction_mem line 42
  6. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.isClosed_preserves_subspace line 59
  7. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.connected_invariant_commonEigenspace line 68
  8. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.connected_normal_invariant_eigenspace line 91
  9. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.connected_normalAbelian_invariant_eigenspace line 103