OAI/Geometry/HyperbolicGroups/VoltageEdgeAgreement.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Gluing of edge data is proved from the literal lifted coordinates. No agreement of independent choices on intersecting edges is assumed.

  1. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.vertexLift_eq_iff line 18
  2. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.edgeLift_sheet_injective line 22
  3. structure OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.EdgeData line 30
  4. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.EdgeData.at_vertex line 42
  5. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.EdgeData.agree line 58
  6. def OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.graphEdgeData line 90
  7. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.edgeHomotopy_agree line 98