OAI/GroupTheory/PolycyclicRecognition/Algebra/PolynomialQuotientAction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Polynomial coordinates for induced quotient actions

Choose lifts of a quotient basis. Every forward and inverse matrix entry of the induced action is then one linear functional of an ambient translate. This gives continuity for the concrete polynomial matrix topology.

  1. def OAI.PolycyclicRecognition.PolynomialMatrixGroup.coordinateLinearAction line 19
  2. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.coordinateLinearAction_apply line 33
  3. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.coordinateLinearAction_entries line 38
  4. def OAI.PolycyclicRecognition.PolynomialMatrixGroup.functionalPolynomialAt line 45
  5. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.eval_functionalPolynomialAt line 50
  6. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.continuous_quotientLinearAction line 60