OAI/GroupTheory/PolycyclicRecognition/Algebra/PolynomialMatrixCommutator.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Polynomial continuity of commutator sections

For a fixed matrix, conjugation by the variable matrix is polynomial in the matrix and inverse coordinates. Hence the commutator is continuous in either variable separately in the polynomial topology.

  1. def OAI.PolycyclicRecognition.PolynomialMatrixGroup.conjugationPolynomial line 19
  2. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.coordinates_conjugation_fixed line 25
  3. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.continuous_conjugation_fixed line 34
  4. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.continuous_commutator_right line 38
  5. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.continuous_commutator_left line 43