OAI/GroupTheory/PolycyclicRecognition/Analysis/ConnectedHomCovering.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Inverting a local group isomorphism over a simply connected group

Local injectivity and the neighborhood-image identity at one suffice. Translations propagate them, connectedness gives surjectivity, and the proved covering-space argument gives the global inverse.

  1. theorem OAI.PolycyclicRecognition.surjective_of_hom_map_nhds_one line 22
  2. theorem OAI.PolycyclicRecognition.covering_of_hom_local_coordinates line 40
  3. theorem OAI.PolycyclicRecognition.bijective_of_hom_local_coordinates line 58