OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanRepresentationDescent.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Descending continuous representations from the Cartan factors

The existing factor model includes surjectivity and compact lifts. Thus the algebraic descent also preserves continuity, without choosing a global continuous factorization.

  1. theorem OAI.PolycyclicRecognition.CartanFactorModel.descend_representation line 27