OAI/Geometry/HyperbolicGroups/FinitePolygonVoltage.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Literal source voltages on the mapping-cylinder triangulation.

  1. def OAI.HyperbolicObstruction.FinitePolygonModel.Data.signed line 17
  2. def OAI.HyperbolicObstruction.FinitePolygonModel.Data.segment line 19
  3. def OAI.HyperbolicObstruction.FinitePolygonModel.Data.cornerOffset line 21
  4. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.cornerOffset_next line 25
  5. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.next_next_ne line 34
  6. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.base_next line 40
  7. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.base_ne_next line 50
  8. def OAI.HyperbolicObstruction.FinitePolygonModel.Data.graphValue line 59

    Source documentation

    Only the middle third of each graph edge carries its original voltage.

    def graphValue : (V ⊕ (E × Bool)) → (V ⊕ (E × Bool)) → G
  | .inr (e,a), .inr (f,b) => if e = f ∧ a ≠ b then signed v (e,a) else 1
  | _,_ => 1

    Mentions: OAI.HyperbolicObstruction.FinitePolygonModel.Data.signed

  9. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.graphValue_self line 63
  10. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.graphValue_reverse line 66
  11. def OAI.HyperbolicObstruction.FinitePolygonModel.Data.value line 75

    Source documentation

    The collar and cap formulas retain each occurrence's independent cornerOffset.

    def value : P.Vertex → P.Vertex → G
  | .inl a, .inl b => graphValue (V := V) v a b
…

    Mentions: OAI.HyperbolicObstruction.FinitePolygonModel.Data.graphValue

  12. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.value_self line 85
  13. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.value_reverse line 91
  14. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.base_graph line 101
  15. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.value_outer_base line 105
  16. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.value_outer_nextbase line 111
  17. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.value_outer_next line 117
  18. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.value_apex_outer line 120
  19. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.value_base_next line 123
  20. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.collar_ordered line 129
  21. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.facet_flat line 145
  22. def OAI.HyperbolicObstruction.FinitePolygonModel.Data.voltage line 162

    Source documentation

    Every literal source relation gives a genuine topological voltage cover of its finite simplicial mapping-cylinder realization.

    def voltage (h : ∀ c, (List.ofFn (fun i => signed v (P.side c i))).prod = 1) :
    Voltage P.complex G where
…

    Mentions: OAI.HyperbolicObstruction.FinitePolygonModel.Data.signed