OAI/Geometry/HyperbolicGroups/VoltageClosedCells.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Closed simplices in the actual voltage cover. The extended chart formula is continuous even when its anchor coordinate is zero, by the triangle cocycle.

  1. instance OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.totalSpace_t2 line 17
  2. def OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.closedFace line 33
  3. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.closedFace_isClosed line 35
  4. instance OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.closedFace_compact line 37
  5. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.member_of_positive line 40
  6. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.inChart_change_face line 46
  7. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.inChart_continuous_face line 62
  8. def OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.faceLift line 79
  9. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.faceLift_proj line 83
  10. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.faceLift_injective line 87
  11. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.faceLift_closedEmbedding line 92
  12. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.faceLift_chart line 96
  13. abbrev OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.FaceAnchor line 114

    Source documentation

    Anchor is finite data; no choice of deck coordinate is lost.

    abbrev FaceAnchor := {sa : Finset V × V // sa.1 ∈ K.faces ∧ sa.2 ∈ sa.1}
  14. def OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.liftedClosedFace line 116
  15. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.liftedClosedFace_closed line 119
  16. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.liftedClosedFace_cover line 123
  17. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.liftedClosedFace_locallyFinite line 140

    Source documentation

    The original covering topology has a locally finite closed simplex cover. There are only finitely many base faces/anchors and at most one deck label per anchored face in a fixed small chart neighborhood.

    lemma liftedClosedFace_locallyFinite : LocallyFinite v.liftedClosedFace := by
…