OAI/Algebra/GroupRing/AttachmentFurther.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.GroupRingTopology.Attachment.sphere_filling_preserved line 23
  2. lemma OAI.GroupRingTopology.Attachment.dimH_disk_subtype_le line 36
  3. lemma OAI.GroupRingTopology.Attachment.filling_reflected line 43

    Source documentation

    Relative cellular approximation implies that a low-dimensional sphere that bounds after a high-dimensional attachment already bounded beforehand.

    lemma filling_reflected {m : ℕ} (hm : m < n) (b : C(Sphere m,X))
    (hb : SphereTopology.Extends ((⟨base a,continuous_base a⟩ : C(X,Space a)).comp b)) :
    SphereTopology.Extends b := by
…

    Mentions: OAI.GroupRingTopology.Attachment.Sphere, OAI.GroupRingTopology.SphereTopology.Extends, OAI.GroupRingTopology.Attachment.base, OAI.GroupRingTopology.Attachment.continuous_base, OAI.GroupRingTopology.Attachment.Space

  4. lemma OAI.GroupRingTopology.Attachment.pathConnectedSpace line 61
  5. instance OAI.GroupRingTopology.Cayley.presentationCoverT2 line 85
  6. instance OAI.GroupRingTopology.Cayley.presentationCoverCW line 88
  7. lemma OAI.GroupRingTopology.Cayley.presentationCover_pathConnected line 92
  8. lemma OAI.GroupRingTopology.Cayley.presentationCover_sphereFill line 101
  9. lemma OAI.GroupRingTopology.Cayley.presentationCover_simplyConnected line 111
  10. abbrev OAI.GroupRingTopology.Orbits line 125
  11. lemma OAI.GroupRingTopology.orbit_mk_smul line 127
  12. lemma OAI.GroupRingTopology.orbit_out_translate line 131
  13. lemma OAI.GroupRingTopology.orbitCoordinates_bijective line 140
  14. def OAI.GroupRingTopology.orbitCoordinates line 156
  15. lemma OAI.GroupRingTopology.orbitCoordinates_apply line 159
  16. def OAI.GroupRingTopology.Cellular.actionChart line 172
  17. lemma OAI.GroupRingTopology.Cellular.actionChart_apply line 175
  18. lemma OAI.GroupRingTopology.Cellular.actionChart_image line 178
  19. lemma OAI.GroupRingTopology.Cellular.actionChart_source line 182
  20. lemma OAI.GroupRingTopology.Cellular.actionChart_continuousOn line 186
  21. lemma OAI.GroupRingTopology.Cellular.actionChart_continuousOn_symm line 190
  22. lemma OAI.GroupRingTopology.Cellular.actionChart_open line 204
  23. lemma OAI.GroupRingTopology.Cellular.actionChart_closed line 210
  24. lemma OAI.GroupRingTopology.Cellular.closedCell_smul line 217
  25. def OAI.GroupRingTopology.Cellular.actionCW line 228

    Source documentation

    A free permutation of cell orbits can be made strictly equivariant at the level of characteristic maps. This changes neither the space nor the cells.

    def actionCW : CWComplex (univ : Set X) where
…
  26. lemma OAI.GroupRingTopology.Cellular.actionChart_smul line 285
  27. lemma OAI.GroupRingTopology.Milnor.vertexTranslate_injective line 296
  28. lemma OAI.GroupRingTopology.Milnor.translate_card line 303
  29. abbrev OAI.GroupRingTopology.Milnor.StageCell line 306
  30. def OAI.GroupRingTopology.Milnor.cellTranslate line 308
  31. instance OAI.GroupRingTopology.Milnor.cellAction line 311
  32. lemma OAI.GroupRingTopology.Milnor.cell_smul_val line 316
  33. lemma OAI.GroupRingTopology.Milnor.cellAction_free line 319
  34. abbrev OAI.GroupRingTopology.Milnor.CellOrbits line 328
  35. def OAI.GroupRingTopology.Milnor.cellCoordinates line 330
  36. lemma OAI.GroupRingTopology.Milnor.cellCoordinates_apply line 333
  37. instance OAI.GroupRingTopology.Milnor.cellOrbits_finite line 336
  38. lemma OAI.GroupRingTopology.Milnor.stage_smul_support line 355
  39. lemma OAI.GroupRingTopology.Milnor.stage_openCell line 359
  40. lemma OAI.GroupRingTopology.Milnor.stage_closedCell line 363
  41. lemma OAI.GroupRingTopology.Milnor.stage_openCell_smul line 368
  42. lemma OAI.GroupRingTopology.Milnor.stage_closedCell_smul line 382
  43. def OAI.GroupRingTopology.Milnor.stageEquivariantCW line 399