OAI/Geometry/HyperbolicGroups/CyclicTriangleCochains.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Explicit obstruction cochains for every individual collared-fan triangle.

  1. def OAI.HyperbolicObstruction.CyclicTriangleBoundary.cyclePrimitive line 15
  2. lemma OAI.HyperbolicObstruction.CyclicTriangleBoundary.cyclePrimitive_difference line 18
  3. def OAI.HyperbolicObstruction.CyclicTriangleBoundary.triangleDiagonal line 55
  4. def OAI.HyperbolicObstruction.CyclicTriangleBoundary.triangleOuter line 56
  5. def OAI.HyperbolicObstruction.CyclicTriangleBoundary.triangleIncrement line 57
  6. def OAI.HyperbolicObstruction.CyclicTriangleBoundary.triangleApex line 59
  7. lemma OAI.HyperbolicObstruction.CyclicTriangleBoundary.triangleIncrement_sum line 63
  8. lemma OAI.HyperbolicObstruction.CyclicTriangleBoundary.triangleApex_difference line 75
  9. theorem OAI.HyperbolicObstruction.CyclicTriangleBoundary.triangle_cochain_extension line 83

    Source documentation

    The literal oriented edge cochain has the given value on every triangle boundary. Radial edges have zero value; all other edges are explicit.

    theorem triangle_cochain_extension (q : Corner size) :
    L (edge q) - triangleDiagonal size edge weight L q = weight (q,0) ∧
    triangleDiagonal size edge weight L q - triangleOuter size edge weight L q = weight (q,1) ∧
    triangleOuter size edge weight L q + triangleApex size edge weight L q -
      triangleApex size edge weight L (next size q) = weight (q,2) := by
…

    Mentions: OAI.HyperbolicObstruction.CyclicTriangleBoundary.Corner, OAI.HyperbolicObstruction.CyclicTriangleBoundary.triangleDiagonal, OAI.HyperbolicObstruction.CyclicTriangleBoundary.triangleOuter, OAI.HyperbolicObstruction.CyclicTriangleBoundary.triangleApex, OAI.HyperbolicObstruction.CyclicTriangleBoundary.next