OAI/Geometry/HyperbolicGroups/FinitePolyhedronMonodromy.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Actual path-homotopy invariance of edge voltages, obtained from the constructed covering and its literal charts.

  1. def OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.inChart line 18
  2. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.inChart_proj line 21
  3. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.inChart_coordinate line 24
  4. def OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.chartFiber line 27
  5. def OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.vertexFiber line 30
  6. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.indexAt_vertex line 33
  7. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.chartFiber_vertex line 36
  8. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.chartFiber_change line 44
  9. def OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.liftInChart line 53
  10. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.monodromy_inChart line 62
  11. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.monodromy_starPath line 68
  12. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.monodromy_symm line 74
  13. def OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.edgeMid line 82

    Source documentation

    The midpoint lies in both endpoint stars, even for a collapsed edge.

    def edgeMid {a b : V} (h : {a,b} ∈ K.faces) : Carrier K :=
…

    Mentions: OAI.HyperbolicObstruction.FinitePolyhedron.Carrier

  14. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.edgeMid_left line 85
  15. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.edgeMid_right line 95
  16. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.monodromy_edge line 105
  17. def OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.EdgeChain.eval line 119
  18. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.EdgeChain.eval_nil line 125
  19. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.EdgeChain.eval_cons line 127
  20. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.EdgeChain.monodromy line 130
  21. theorem OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.eval_eq_of_homotopic line 142

    Source documentation

    Every literal triangular cocycle is invariant under actual continuous relative-endpoint path homotopies, not just formal triangle moves.

    theorem eval_eq_of_homotopic {a b : V} (p q : FinitePolyhedron.EdgeChain K a b)
    (h : p.path.Homotopic q.path) : EdgeChain.eval v p = EdgeChain.eval v q := by
…

    Mentions: OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain, OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.EdgeChain.eval