OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanSemidirectCover.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The genuine product cover of the Cartan factors

The factors in the ambient group may overlap. Their semidirect product instead has unique product coordinates; the projection is surjective and has compact lifts, which suffices to descend compact coboundary approximations.

  1. theorem OAI.PolycyclicRecognition.CartanFactorModel.continuous_action line 34
  2. def OAI.PolycyclicRecognition.CartanFactorModel.semidirectProjection line 48
  3. theorem OAI.PolycyclicRecognition.CartanFactorModel.continuous_semidirectProjection line 52
  4. theorem OAI.PolycyclicRecognition.CartanFactorModel.surjective_semidirectProjection line 58
  5. theorem OAI.PolycyclicRecognition.CartanFactorModel.compact_lifts_semidirectProjection line 64
  6. theorem OAI.PolycyclicRecognition.CartanFactorModel.semidirect_topologicalGroup line 75
  7. theorem OAI.PolycyclicRecognition.CartanFactorModel.unitaryReducedVanishing_of_cover line 79