OAI/GroupTheory/PolycyclicRecognition/Algebra/PolynomialMatrixGroup.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Polynomial topology on invertible matrices

Both a matrix and its inverse are retained as affine coordinates. Inversion then exchanges coordinates, and translations are polynomial coordinate maps. The resulting topology is Noetherian and T1. Only separate continuity of multiplication is asserted; the product topology need not be the affine polynomial topology on a product.

  1. structure OAI.PolycyclicRecognition.PolynomialMatrixGroup line 20
  2. def OAI.PolycyclicRecognition.PolynomialMatrixGroup.equivGL line 27
  3. instance OAI.PolycyclicRecognition.PolynomialMatrixGroup.(instance at line 33) line 33
  4. def OAI.PolycyclicRecognition.PolynomialMatrixGroup.mulEquivGL line 35
  5. def OAI.PolycyclicRecognition.PolynomialMatrixGroup.entries line 38
  6. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.entries_mul line 40
  7. abbrev OAI.PolycyclicRecognition.PolynomialMatrixGroup.Coord line 43
  8. def OAI.PolycyclicRecognition.PolynomialMatrixGroup.coordinates line 45
  9. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.coordinates_injective line 48
  10. instance OAI.PolycyclicRecognition.PolynomialMatrixGroup.(instance at line 55) line 55
  11. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.inducing_coordinates line 58
  12. instance OAI.PolycyclicRecognition.PolynomialMatrixGroup.(instance at line 61) line 61
  13. instance OAI.PolycyclicRecognition.PolynomialMatrixGroup.(instance at line 65) line 65
  14. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.continuous_of_polynomial line 68
  15. def OAI.PolycyclicRecognition.PolynomialMatrixGroup.leftPolynomial line 77
  16. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.coordinates_mul_left line 84
  17. def OAI.PolycyclicRecognition.PolynomialMatrixGroup.rightPolynomial line 92
  18. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.coordinates_mul_right line 99
  19. instance OAI.PolycyclicRecognition.PolynomialMatrixGroup.(instance at line 107) line 107
  20. instance OAI.PolycyclicRecognition.PolynomialMatrixGroup.(instance at line 111) line 111