OAI/Geometry/HyperbolicGroups/FinitePolyhedronDeck.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The literal voltage cover has a free transitive deck action. This supplies an actual quotient covering to Mathlib's monodromy theorems.

  1. def OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.coordinate line 17
  2. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.totalSpace_ext line 19
  3. instance OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.deckAction line 27
  4. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.deck_proj line 32
  5. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.deck_coordinate line 33
  6. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.chart_deck line 36
  7. instance OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.deckContinuous line 43
  8. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.same_fiber_iff_orbit line 60
  9. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.disjoint_deck_neighborhood line 71
  10. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.isQuotientCoveringMap line 87