OAI/Geometry/HyperbolicGroups/PolygonTriangleCochains.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Cochain extension with literal initial-sheet coordinates for every collar triangle. Its only algebraic input is the precise polygon boundary equation.

  1. def OAI.HyperbolicObstruction.FinitePolygonModel.Data.signedCochain line 16
  2. def OAI.HyperbolicObstruction.FinitePolygonModel.Data.segmentCochain line 18
  3. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.cochain_base_next line 21
  4. def OAI.HyperbolicObstruction.FinitePolygonModel.Data.triangleWeight line 29
  5. def OAI.HyperbolicObstruction.FinitePolygonModel.Data.correctionDiagonal line 31
  6. def OAI.HyperbolicObstruction.FinitePolygonModel.Data.correctionOuter line 32
  7. def OAI.HyperbolicObstruction.FinitePolygonModel.Data.correctionIncrement line 33
  8. def OAI.HyperbolicObstruction.FinitePolygonModel.Data.correctionApex line 36
  9. def OAI.HyperbolicObstruction.FinitePolygonModel.Data.triangleCochain line 38
  10. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.correctionIncrement_sum line 49
  11. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.correctionApex_difference line 60
  12. theorem OAI.HyperbolicObstruction.FinitePolygonModel.Data.triangleCochain_coboundary line 74

    Source documentation

    Values on the three LITERAL oriented triangle boundaries. The second collar orientation uses a plus rather than silently sharing the polygon sign.

    theorem triangleCochain_coboundary (g : G) (q : P.Position) :
    (P.triangleCochain v w T g (P.outer q) (P.base q) +
      P.triangleCochain v w T (g*P.value v (P.outer q) (P.base q)) (P.base q) (P.base (P.next q)) -
      P.triangleCochain v w T g (P.outer q) (P.base (P.next q)) = T g q 0) ∧
    (P.triangleCochain v w T g (P.outer q) (P.outer (P.next q)) +
      P.triangleCochain v w T (g*P.value v (P.outer q) (P.outer (P.next q))) (P.outer (P.next q)) (P.base (P.next q)) -
      P.triangleCochain v w T g (P.outer q) (P.base (P.next q)) = T g q 1) ∧
    (P.triangleCochain v w T g (P.outer q) (P.outer (P.next q)) +
      P.triangleCochain v w T (g*P.value v (P.outer q) (P.outer (P.next q))) (P.outer (P.next q)) (P.apex q.1) -
      P.triangleCochain v w T g (P.outer q) (P.apex q.1) = T g q 2) := by
…