OAI/GroupTheory/ArtinCAT0/Grid.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ArtinCAT0.TrianglePatch line 10

    Source documentation

    A triangular disk may have unpaired boundary darts. No topological theorem is hidden in this interface: exactness is required and subsequently proved for the explicit grid disks used in the controlled-diagram construction.

    structure TrianglePatch (F V : Type*) where
…
  2. def OAI.ArtinCAT0.TrianglePatch.Boundary line 19
  3. def OAI.ArtinCAT0.TrianglePatch.Exact line 21
  4. lemma OAI.ArtinCAT0.TrianglePatch.mate_mate line 27
  5. lemma OAI.ArtinCAT0.TrianglePatch.tail_rotate_mate line 29
  6. abbrev OAI.ArtinCAT0.GridDisk.Face line 38
  7. abbrev OAI.ArtinCAT0.GridDisk.Vertex line 39
  8. abbrev OAI.ArtinCAT0.GridDisk.A line 40
  9. abbrev OAI.ArtinCAT0.GridDisk.B line 41
  10. abbrev OAI.ArtinCAT0.GridDisk.C line 42
  11. def OAI.ArtinCAT0.GridDisk.mateFun line 44
  12. lemma OAI.ArtinCAT0.GridDisk.mateFun_involutive line 58
  13. def OAI.ArtinCAT0.GridDisk.tail line 68
  14. lemma OAI.ArtinCAT0.GridDisk.tail_mateFun line 79
  15. def OAI.ArtinCAT0.GridDisk.patch line 89
  16. def OAI.ArtinCAT0.GridDisk.upper line 95
  17. def OAI.ArtinCAT0.GridDisk.potential line 98
  18. lemma OAI.ArtinCAT0.GridDisk.potential_succ line 103
  19. lemma OAI.ArtinCAT0.GridDisk.cocycle_relations line 107
  20. theorem OAI.ArtinCAT0.GridDisk.exact line 136

    Source documentation

    Exactness of the explicit capped cylindrical disk. The proof constructs a potential by integrating vertically downward from the cap; the square and cap relations verify every horizontal edge.

    theorem exact : (patch H N).Exact := by
…

    Mentions: OAI.ArtinCAT0.GridDisk.patch

  21. structure OAI.ArtinCAT0.TrianglePatch.Sides line 226

    Source documentation

    Three marked, equally subdivided sides of a triangular patch. The marks are combinatorial; the vertices and faces need not be mapped injectively.

    structure Sides (P : TrianglePatch A U) (K : ℕ) where
…

    Mentions: OAI.ArtinCAT0.TrianglePatch

  22. lemma OAI.ArtinCAT0.TrianglePatch.boundary_mate line 236
  23. def OAI.ArtinCAT0.TrianglePatch.Sides.index line 244
  24. lemma OAI.ArtinCAT0.TrianglePatch.Sides.index_dart line 248
  25. lemma OAI.ArtinCAT0.TrianglePatch.Sides.dart_index line 254
  26. lemma OAI.ArtinCAT0.reverse_chain_difference line 262
  27. def OAI.ArtinCAT0.TriangleMesh.Replacement.mateFun line 280
  28. lemma OAI.ArtinCAT0.TriangleMesh.Replacement.mate_boundary line 291
  29. lemma OAI.ArtinCAT0.TriangleMesh.Replacement.mate_internal line 298
  30. lemma OAI.ArtinCAT0.TriangleMesh.Replacement.mateFun_involutive line 303
  31. lemma OAI.ArtinCAT0.TriangleMesh.Replacement.mateFun_ne line 313
  32. def OAI.ArtinCAT0.TriangleMesh.Replacement.Seam line 331

    Source documentation

    Boundary vertices glued with opposite side parametrizations.

    def Seam (u v : F × U) : Prop :=
…
  33. abbrev OAI.ArtinCAT0.TriangleMesh.Replacement.Vertex line 335
  34. def OAI.ArtinCAT0.TriangleMesh.Replacement.vertex line 337
  35. lemma OAI.ArtinCAT0.TriangleMesh.Replacement.vertex_seam line 340
  36. def OAI.ArtinCAT0.TriangleMesh.Replacement.tail line 345
  37. lemma OAI.ArtinCAT0.TriangleMesh.Replacement.tail_mateFun line 348
  38. def OAI.ArtinCAT0.TriangleMesh.Replacement.mesh line 362
  39. theorem OAI.ArtinCAT0.TriangleMesh.Replacement.exact line 371

    Source documentation

    Substituting an exact triangular patch in every coarse face preserves exactness. This is a cochain proof, independent of any triangulation theorem.

    theorem exact (hM : M.Exact) (hP : P.Exact) : (mesh M P S).Exact := by
…

    Mentions: OAI.ArtinCAT0.TriangleMesh.Replacement.mesh, OAI.ArtinCAT0.TriangleMesh.Exact

  40. lemma OAI.ArtinCAT0.GridDisk.boundary_iff line 452
  41. def OAI.ArtinCAT0.GridDisk.sideIndex line 487
  42. def OAI.ArtinCAT0.GridDisk.sideDart line 490
  43. def OAI.ArtinCAT0.GridDisk.sidePoint line 493
  44. lemma OAI.ArtinCAT0.GridDisk.sideIndex_castSucc line 496
  45. lemma OAI.ArtinCAT0.GridDisk.sideIndex_succ line 503
  46. lemma OAI.ArtinCAT0.GridDisk.sidePoint_ends line 511
  47. def OAI.ArtinCAT0.GridDisk.sides line 525
  48. def OAI.ArtinCAT0.TriangleMesh.doubleTriangle line 560

    Source documentation

    The sphere consisting of two oppositely oriented triangles.

    def doubleTriangle : TriangleMesh Bool (Fin 3) where
…

    Mentions: OAI.ArtinCAT0.TriangleMesh

  49. lemma OAI.ArtinCAT0.TriangleMesh.doubleTriangle_exact line 568