OAI/Algebra/GroupRing/LoopSphere.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

The path-class extension of an acting group. This is geometric support for the finite presentation Cayley cover, not an assumption of simple connectivity.

  1. theorem OAI.GroupRingTopology.Cellular.cylinderFill line 16

    Source documentation

    One cylinder boundary filling is enough for its path-space lift.

    theorem cylinderFill {n : ℕ} (a : C(Sphere n,C(unitInterval,Y))) (b : C(Disk n,Y × Y))
    (h : ∀ x, pathEndpoint (a x) = b (boundary n x))
    (F : C(Disk (n+1),Y)) (hF : ∀ x, F (boundary (n+1) x) = cylinderBoundaryMap a b h x) :
    ∃ e : C(Disk n,C(unitInterval,Y)),
      (∀ x, e (boundary n x) = a x) ∧ (∀ x, pathEndpoint (e x) = b x) := by
…

    Mentions: OAI.GroupRingTopology.Cellular.Sphere, OAI.GroupRingTopology.Cellular.Disk, OAI.GroupRingTopology.Cellular.pathEndpoint, OAI.GroupRingTopology.Cellular.boundary, OAI.GroupRingTopology.Cellular.cylinderBoundaryMap

  2. def OAI.GroupRingTopology.LoopSphere.sides line 66
  3. def OAI.GroupRingTopology.LoopSphere.ends line 67
  4. lemma OAI.GroupRingTopology.LoopSphere.ends_sides line 70
  5. def OAI.GroupRingTopology.LoopSphere.map line 78
  6. theorem OAI.GroupRingTopology.LoopSphere.homotopic_of_fill line 81

    Source documentation

    Attaching one ordinary 2-cell along this square boundary kills its loop.

    theorem homotopic_of_fill (p : Path x x) (F : C(Disk 2,X))
    (hF : ∀ z, F (boundary 2 z) = map p z) : p.Homotopic (Path.refl x) := by
…

    Mentions: OAI.GroupRingTopology.LoopSphere.map

  7. lemma OAI.GroupRingTopology.LoopSphere.natural line 109
  8. lemma OAI.GroupRingTopology.LoopSphere.homotopic_map_of_fill line 120
  9. lemma OAI.GroupRingTopology.PathExtension.Q.trans_cast line 141
  10. lemma OAI.GroupRingTopology.PathExtension.Q.map_trans line 145
  11. lemma OAI.GroupRingTopology.PathExtension.Q.map_refl line 151
  12. lemma OAI.GroupRingTopology.PathExtension.Q.map_symm line 153
  13. structure OAI.GroupRingTopology.PathExtension.Q.Equal line 158

    Source documentation

    Equality of path classes together with equality of both endpoint labels.

    structure Equal {x' y' : X} (p : Path.Homotopic.Quotient x y)
    (q : Path.Homotopic.Quotient x' y') : Prop where
…
  14. lemma OAI.GroupRingTopology.PathExtension.Q.Equal.refl line 165
  15. lemma OAI.GroupRingTopology.PathExtension.Q.Equal.ofEq line 166
  16. lemma OAI.GroupRingTopology.PathExtension.Q.Equal.symm line 167
  17. lemma OAI.GroupRingTopology.PathExtension.Q.Equal.trans line 170
  18. lemma OAI.GroupRingTopology.PathExtension.Q.Equal.map line 174
  19. lemma OAI.GroupRingTopology.PathExtension.Q.Equal.comp line 181
  20. lemma OAI.GroupRingTopology.PathExtension.Q.cast_equal line 191
  21. lemma OAI.GroupRingTopology.PathExtension.Q.refl_equal line 193
  22. def OAI.GroupRingTopology.PathExtension.smulMap line 202
  23. lemma OAI.GroupRingTopology.PathExtension.map_one_equal line 204
  24. lemma OAI.GroupRingTopology.PathExtension.map_mul_equal line 210
  25. abbrev OAI.GroupRingTopology.PathExtension.Extension line 217
  26. lemma OAI.GroupRingTopology.PathExtension.ext line 221
  27. instance OAI.GroupRingTopology.PathExtension.(instance at line 224) line 224
  28. instance OAI.GroupRingTopology.PathExtension.(instance at line 226) line 226
  29. instance OAI.GroupRingTopology.PathExtension.(instance at line 228) line 228
  30. lemma OAI.GroupRingTopology.PathExtension.mul_path_equal line 231
  31. lemma OAI.GroupRingTopology.PathExtension.one_path_equal line 236
  32. lemma OAI.GroupRingTopology.PathExtension.mul_assoc line 240
  33. lemma OAI.GroupRingTopology.PathExtension.one_mul line 251
  34. lemma OAI.GroupRingTopology.PathExtension.mul_one line 258
  35. lemma OAI.GroupRingTopology.PathExtension.inv_mul_cancel line 266
  36. instance OAI.GroupRingTopology.PathExtension.(instance at line 275) line 275
  37. def OAI.GroupRingTopology.PathExtension.projection line 282

    Source documentation

    Endpoint projection of the genuine path-class extension.

    def projection : Extension G x₀ →* G where
…

    Mentions: OAI.GroupRingTopology.PathExtension.Extension

  38. lemma OAI.GroupRingTopology.PathExtension.natural_smul_equal line 296
  39. def OAI.GroupRingTopology.PathExtension.mapFun line 303
  40. lemma OAI.GroupRingTopology.PathExtension.mapFun_equal line 306
  41. lemma OAI.GroupRingTopology.PathExtension.mapFun_one line 309
  42. lemma OAI.GroupRingTopology.PathExtension.mapFun_mul line 316
  43. def OAI.GroupRingTopology.PathExtension.map line 327
  44. lemma OAI.GroupRingTopology.PathExtension.projection_map line 332
  45. lemma OAI.GroupRingTopology.Cayley.smul_vertex line 341
  46. def OAI.GroupRingTopology.Cayley.pathGenerator line 343
  47. def OAI.GroupRingTopology.Cayley.wordLift line 346
  48. lemma OAI.GroupRingTopology.Cayley.projection_wordLift line 348
  49. lemma OAI.GroupRingTopology.Cayley.wordLift_fst line 352
  50. def OAI.GroupRingTopology.Cayley.relatorClass line 356
  51. def OAI.GroupRingTopology.Cayley.relatorLoop line 358
  52. lemma OAI.GroupRingTopology.Cayley.relatorLoop_eq line 360
  53. lemma OAI.GroupRingTopology.Cayley.relatorLoop_equal line 363
  54. def OAI.GroupRingTopology.Cayley.relatorAttaching line 368
  55. abbrev OAI.GroupRingTopology.Cayley.PresentationCover line 369
  56. def OAI.GroupRingTopology.Cayley.presentationBase line 370
  57. lemma OAI.GroupRingTopology.Cayley.presentationBase_smul line 371
  58. def OAI.GroupRingTopology.Cayley.coverWordLift line 374
  59. lemma OAI.GroupRingTopology.Cayley.mapped_relator_homotopic line 378
  60. lemma OAI.GroupRingTopology.Cayley.coverWordLift_relator line 389
  61. lemma OAI.GroupRingTopology.Cayley.coverWordLift_ker line 399
  62. def OAI.GroupRingTopology.Cayley.presentationSection line 406
  63. lemma OAI.GroupRingTopology.Cayley.presentationSection_lift line 410
  64. lemma OAI.GroupRingTopology.Cayley.presentationSection_fst line 414