OAI/Geometry/HyperbolicGroups/FinitePolyhedronPathAlgebra.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The triangle relations and rooted path groupoid calculations in the actual realization.

  1. lemma OAI.HyperbolicObstruction.FinitePolyhedron.edge_of_subset line 16
  2. lemma OAI.HyperbolicObstruction.FinitePolyhedron.edge_self line 22
  3. lemma OAI.HyperbolicObstruction.FinitePolyhedron.edgePath_self line 24
  4. lemma OAI.HyperbolicObstruction.FinitePolyhedron.edgePath_triangle line 31
  5. abbrev OAI.HyperbolicObstruction.FinitePolyhedron.RootedPaths.PiOne line 50
  6. def OAI.HyperbolicObstruction.FinitePolyhedron.RootedPaths.based line 52
  7. lemma OAI.HyperbolicObstruction.FinitePolyhedron.RootedPaths.based_refl line 56
  8. lemma OAI.HyperbolicObstruction.FinitePolyhedron.RootedPaths.based_trans line 62
  9. lemma OAI.HyperbolicObstruction.FinitePolyhedron.RootedPaths.based_route line 75
  10. lemma OAI.HyperbolicObstruction.FinitePolyhedron.RootedPaths.based_loop line 81
  11. def OAI.HyperbolicObstruction.FinitePolyhedron.RootedPaths.edgeLoop line 90

    Source documentation

    Every edge yields the actual loop obtained by the fixed endpoint routes.

    def edgeLoop (a b : V) : PiOne (K := K) o :=
…

    Mentions: OAI.HyperbolicObstruction.FinitePolyhedron.RootedPaths.PiOne

  12. lemma OAI.HyperbolicObstruction.FinitePolyhedron.RootedPaths.edgeLoop_of_edge line 93
  13. def OAI.HyperbolicObstruction.FinitePolyhedron.RootedPaths.voltage line 97

    Source documentation

    The actual triangle disks imply a group-valued flat cocycle.

    def voltage : Voltage K (PiOne (K := K) o) where
…

    Mentions: OAI.HyperbolicObstruction.FinitePolyhedron.Voltage, OAI.HyperbolicObstruction.FinitePolyhedron.RootedPaths.PiOne

  14. lemma OAI.HyperbolicObstruction.FinitePolyhedron.RootedPaths.eval_chain line 109
  15. def OAI.HyperbolicObstruction.FinitePolyhedron.edgeRoutes line 120

    Source documentation

    Actual edge-chain routes exist in every path-connected finite realization.

    def edgeRoutes [PathConnectedSpace (Carrier K)] (o : V) (a : V) : EdgeChain K o a :=
…

    Mentions: OAI.HyperbolicObstruction.FinitePolyhedron.Carrier, OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain

  16. lemma OAI.HyperbolicObstruction.FinitePolyhedron.edgeRoutes_self line 124