OAI/Algebra/GroupRing/Cayley.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GroupRingTopology.Attachment.map line 20
  2. lemma OAI.GroupRingTopology.Attachment.map_base line 25
  3. lemma OAI.GroupRingTopology.Attachment.map_cell line 29
  4. lemma OAI.GroupRingTopology.Attachment.map_openCell line 33
  5. lemma OAI.GroupRingTopology.Attachment.map_surjective line 39
  6. lemma OAI.GroupRingTopology.Attachment.map_isQuotientMap line 52
  7. def OAI.GroupRingTopology.Attachment.FreeIndex line 77
  8. instance OAI.GroupRingTopology.Attachment.(instance at line 79) line 79
  9. instance OAI.GroupRingTopology.Attachment.(instance at line 84) line 84
  10. def OAI.GroupRingTopology.Attachment.equivariantFamily line 92
  11. lemma OAI.GroupRingTopology.Attachment.equivariantFamily_smul line 95
  12. instance OAI.GroupRingTopology.Attachment.equivariantAttachmentContinuousAction line 98
  13. lemma OAI.GroupRingTopology.Attachment.equivariantFamily_over line 106
  14. def OAI.GroupRingTopology.Attachment.coverMap line 110
  15. lemma OAI.GroupRingTopology.Attachment.coverMap_isQuotient line 113
  16. lemma OAI.GroupRingTopology.Attachment.coverMap_fibers line 116
  17. lemma OAI.GroupRingTopology.Attachment.coverMap_isQuotientCovering line 170

    Source documentation

    Free, equivariant cell attachments preserve a genuine regular covering. The proof constructs collars of disjoint slices; no local-finiteness or local-compactness hypothesis is imposed.

    lemma coverMap_isQuotientCovering : IsQuotientCoveringMap (coverMap a p hp b h) G where
…

    Mentions: OAI.GroupRingTopology.Attachment.coverMap

  18. lemma OAI.GroupRingTopology.Attachment.coverMap_isCovering line 176
  19. lemma OAI.GroupRingTopology.Cayley.sphere_one_cases line 185
  20. instance OAI.GroupRingTopology.Cayley.(instance at line 191) line 191
  21. instance OAI.GroupRingTopology.Cayley.(instance at line 203) line 203
  22. def OAI.GroupRingTopology.Cayley.minus line 205
  23. def OAI.GroupRingTopology.Cayley.plus line 206
  24. def OAI.GroupRingTopology.Cayley.attaching line 211
  25. abbrev OAI.GroupRingTopology.Cayley.Graph line 214
  26. instance OAI.GroupRingTopology.Cayley.(instance at line 216) line 216
  27. def OAI.GroupRingTopology.Cayley.vertex line 218
  28. lemma OAI.GroupRingTopology.Cayley.discrete_dimension line 221
  29. instance OAI.GroupRingTopology.Cayley.graphCW line 226
  30. instance OAI.GroupRingTopology.Cayley.(instance at line 229) line 229
  31. lemma OAI.GroupRingTopology.Cayley.graph_dimension line 232
  32. lemma OAI.GroupRingTopology.Cayley.vertex_injective line 235
  33. lemma OAI.GroupRingTopology.Cayley.cell_minus line 237
  34. lemma OAI.GroupRingTopology.Cayley.cell_plus line 243
  35. instance OAI.GroupRingTopology.Cayley.disk_pathConnected line 249
  36. lemma OAI.GroupRingTopology.Cayley.cell_joined line 252
  37. lemma OAI.GroupRingTopology.Cayley.vertex_smul line 257
  38. lemma OAI.GroupRingTopology.Cayley.vertices_joined line 259
  39. lemma OAI.GroupRingTopology.Cayley.graph_pathConnected line 281
  40. lemma OAI.GroupRingTopology.PathSquares.turn line 303
  41. def OAI.GroupRingTopology.PathSquares.spanContract line 309
  42. lemma OAI.GroupRingTopology.PathSquares.spanContract_source line 318
  43. lemma OAI.GroupRingTopology.PathSquares.spanContract_target line 323
  44. def OAI.GroupRingTopology.PathSquares.pauseReverse line 329
  45. theorem OAI.GroupRingTopology.PathSquares.edgeSquare line 333

    Source documentation

    Compatible vertex paths fill every edge square, without any path-word approximation assertion. The pause at the vertex is the same for every edge.

    theorem edgeSquare (p : Path x a) (q : Path x b) (e : Path a b)
    (h : (p.trans e).Homotopic q) :
    ∃ H : e.toContinuousMap.Homotopy (.const _ x),
      (∀ t, H (t,0) = pauseReverse p t) ∧ (∀ t, H (t,1) = pauseReverse q t) := by
…

    Mentions: OAI.GroupRingTopology.PathSquares.pauseReverse

  46. def OAI.GroupRingTopology.Cayley.edgeParam line 365
  47. lemma OAI.GroupRingTopology.Cayley.continuous_edgeParam line 370
  48. def OAI.GroupRingTopology.Cayley.edgeTime line 372
  49. lemma OAI.GroupRingTopology.Cayley.continuous_edgeTime line 379
  50. lemma OAI.GroupRingTopology.Cayley.edgeParam_time line 382
  51. lemma OAI.GroupRingTopology.Cayley.edgeTime_param line 389
  52. lemma OAI.GroupRingTopology.Cayley.edgeParam_zero line 393
  53. lemma OAI.GroupRingTopology.Cayley.edgeParam_one line 397
  54. lemma OAI.GroupRingTopology.Cayley.edgeTime_minus line 401
  55. lemma OAI.GroupRingTopology.Cayley.edgeTime_plus line 403
  56. lemma OAI.GroupRingTopology.Cayley.sphere_one_eq line 405
  57. def OAI.GroupRingTopology.Cayley.edge line 413
  58. def OAI.GroupRingTopology.Cayley.edgeSquare line 423
  59. lemma OAI.GroupRingTopology.Cayley.edgeSquare_source line 425
  60. lemma OAI.GroupRingTopology.Cayley.edgeSquare_target line 428
  61. def OAI.GroupRingTopology.Cayley.edgePaths line 432
  62. def OAI.GroupRingTopology.Cayley.vertexPaths line 436
  63. lemma OAI.GroupRingTopology.Cayley.edgePaths_boundary line 437
  64. def OAI.GroupRingTopology.Cayley.graphPaths line 450
  65. lemma OAI.GroupRingTopology.Cayley.graphPaths_zero line 453
  66. lemma OAI.GroupRingTopology.Cayley.graphPaths_one line 463
  67. def OAI.GroupRingTopology.Cayley.graphNullhomotopy line 473

    Source documentation

    A coherent system of vertex paths contracts the entire graph map.

    def graphNullhomotopy : f.Homotopy (.const _ y) where
…