OAI/AlgebraicTopology/CWComplex/Collar.lean

GitHub source file

114 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.EilenbergGanea.CWCollar.Attachment line 23

    Source documentation

    Single-dimensional ordinary disk attachment. All fields will be derived from the actual CW structure, not posited for the classifying-space theorem.

    structure Attachment (X : Type u) [TopologicalSpace X] (J : Type v) (n : ℕ) where
…
  2. abbrev OAI.EilenbergGanea.CWCollar.Attachment.Rep line 36
  3. def OAI.EilenbergGanea.CWCollar.Attachment.q line 37
  4. def OAI.EilenbergGanea.CWCollar.Attachment.coordinate line 38
  5. theorem OAI.EilenbergGanea.CWCollar.Attachment.disk_norm_le line 40
  6. theorem OAI.EilenbergGanea.CWCollar.Attachment.coordinate_eq_of_q_eq line 43
  7. def OAI.EilenbergGanea.CWCollar.Attachment.representative line 77
  8. theorem OAI.EilenbergGanea.CWCollar.Attachment.q_representative line 78
  9. def OAI.EilenbergGanea.CWCollar.Attachment.radius line 81
  10. theorem OAI.EilenbergGanea.CWCollar.Attachment.radius_q line 82
  11. theorem OAI.EilenbergGanea.CWCollar.Attachment.coordinate_continuous line 85
  12. theorem OAI.EilenbergGanea.CWCollar.Attachment.radius_continuous line 89
  13. theorem OAI.EilenbergGanea.CWCollar.Attachment.radius_lower line 94
  14. theorem OAI.EilenbergGanea.CWCollar.Attachment.radius_chart line 95
  15. theorem OAI.EilenbergGanea.CWCollar.Attachment.radius_nonneg line 98
  16. theorem OAI.EilenbergGanea.CWCollar.Attachment.radius_le_one line 104
  17. theorem OAI.EilenbergGanea.CWCollar.Attachment.radius_eq_one_iff line 112
  18. def OAI.EilenbergGanea.CWCollar.Attachment.outer line 124
  19. def OAI.EilenbergGanea.CWCollar.Attachment.inner line 125
  20. theorem OAI.EilenbergGanea.CWCollar.Attachment.outer_open line 126
  21. theorem OAI.EilenbergGanea.CWCollar.Attachment.inner_open line 127
  22. theorem OAI.EilenbergGanea.CWCollar.Attachment.outer_union_inner line 128
  23. theorem OAI.EilenbergGanea.CWCollar.Attachment.lower_subset_outer line 136
  24. def OAI.EilenbergGanea.CWCollar.lowerSkeleton line 149
  25. theorem OAI.EilenbergGanea.CWCollar.characteristic_mem_lower line 151
  26. def OAI.EilenbergGanea.CWCollar.topAttachmentQuotient line 157
  27. theorem OAI.EilenbergGanea.CWCollar.topAttachmentQuotient_continuous line 161
  28. theorem OAI.EilenbergGanea.CWCollar.topAttachmentQuotient_surjective line 165
  29. theorem OAI.EilenbergGanea.CWCollar.topAttachmentQuotient_quotient line 179
  30. def OAI.EilenbergGanea.CWCollar.actualAttachment line 203

    Source documentation

    The abstract single-stage attachment is obtained from the given ordinary CW complex itself, with no restriction on or enumeration of its cells.

    def actualAttachment (m : ℕ) (hd : ∀ k, m < k → IsEmpty (Cell (X := X) k)) :
…
  31. abbrev OAI.EilenbergGanea.CWCollar.PuncturedDisk line 237
  32. def OAI.EilenbergGanea.CWCollar.radialScale line 238
  33. theorem OAI.EilenbergGanea.CWCollar.radialScale_nonneg line 240
  34. def OAI.EilenbergGanea.CWCollar.radialCoords line 243
  35. theorem OAI.EilenbergGanea.CWCollar.radialCoords_norm line 245
  36. theorem OAI.EilenbergGanea.CWCollar.radialCoords_pos line 251
  37. theorem OAI.EilenbergGanea.CWCollar.radialCoords_le line 258
  38. def OAI.EilenbergGanea.CWCollar.radialDisk line 263
  39. theorem OAI.EilenbergGanea.CWCollar.radialDisk_zero line 267
  40. theorem OAI.EilenbergGanea.CWCollar.radialDisk_norm_one line 272
  41. theorem OAI.EilenbergGanea.CWCollar.radialDisk_boundary line 277
  42. theorem OAI.EilenbergGanea.CWCollar.radialDisk_continuous line 284
  43. abbrev OAI.EilenbergGanea.CWCollar.Attachment.OuterRep line 302
  44. def OAI.EilenbergGanea.CWCollar.Attachment.outerIn line 304
  45. def OAI.EilenbergGanea.CWCollar.Attachment.outerQ line 305
  46. theorem OAI.EilenbergGanea.CWCollar.Attachment.outerIn_continuous line 312
  47. theorem OAI.EilenbergGanea.CWCollar.Attachment.outerIn_openMap line 315
  48. theorem OAI.EilenbergGanea.CWCollar.Attachment.outerQ_continuous line 319
  49. theorem OAI.EilenbergGanea.CWCollar.Attachment.range_outerIn line 322
  50. theorem OAI.EilenbergGanea.CWCollar.Attachment.outerQ_surjective line 334
  51. theorem OAI.EilenbergGanea.CWCollar.Attachment.outerQ_quotient line 345
  52. theorem OAI.EilenbergGanea.CWCollar.continuous_sum_prod line 373
  53. theorem OAI.EilenbergGanea.CWCollar.continuous_sigma_prod line 381
  54. def OAI.EilenbergGanea.CWCollar.Attachment.repFlow line 391
  55. theorem OAI.EilenbergGanea.CWCollar.Attachment.repFlow_continuous line 396
  56. theorem OAI.EilenbergGanea.CWCollar.Attachment.repFlow_zero line 403
  57. theorem OAI.EilenbergGanea.CWCollar.Attachment.outerQ_repFlow_one line 408
  58. theorem OAI.EilenbergGanea.CWCollar.Attachment.repFlow_respects line 413
  59. def OAI.EilenbergGanea.CWCollar.Attachment.outerRepresentative line 470
  60. theorem OAI.EilenbergGanea.CWCollar.Attachment.outerQ_representative line 471
  61. def OAI.EilenbergGanea.CWCollar.Attachment.flow line 474
  62. theorem OAI.EilenbergGanea.CWCollar.Attachment.flow_q line 475
  63. theorem OAI.EilenbergGanea.CWCollar.Attachment.flow_continuous line 478
  64. theorem OAI.EilenbergGanea.CWCollar.Attachment.flow_zero line 483
  65. theorem OAI.EilenbergGanea.CWCollar.Attachment.flow_one_lower line 487
  66. def OAI.EilenbergGanea.CWCollar.Attachment.sectionMap line 490
  67. def OAI.EilenbergGanea.CWCollar.Attachment.retractMap line 493
  68. theorem OAI.EilenbergGanea.CWCollar.Attachment.flow_section line 497
  69. theorem OAI.EilenbergGanea.CWCollar.Attachment.retract_section line 502
  70. def OAI.EilenbergGanea.CWCollar.Attachment.collarHomotopy line 509

    Source documentation

    The radial collar is a genuine strong deformation neighborhood of the lower-dimensional CW skeleton.

    def collarHomotopy : (ContinuousMap.id a.outer).Homotopy (a.sectionMap.comp a.retractMap) where
…
  71. abbrev OAI.EilenbergGanea.CWCollar.OpenDisk line 520
  72. theorem OAI.EilenbergGanea.CWCollar.Attachment.q_injective_interior line 524
  73. def OAI.EilenbergGanea.CWCollar.Attachment.innerIn line 536
  74. def OAI.EilenbergGanea.CWCollar.Attachment.innerQ line 537
  75. theorem OAI.EilenbergGanea.CWCollar.Attachment.innerIn_continuous line 542
  76. theorem OAI.EilenbergGanea.CWCollar.Attachment.innerIn_openMap line 545
  77. theorem OAI.EilenbergGanea.CWCollar.Attachment.innerQ_continuous line 549
  78. theorem OAI.EilenbergGanea.CWCollar.Attachment.innerQ_injective line 552
  79. theorem OAI.EilenbergGanea.CWCollar.Attachment.innerQ_surjective line 567
  80. theorem OAI.EilenbergGanea.CWCollar.Attachment.innerQ_openMap line 576
  81. def OAI.EilenbergGanea.CWCollar.Attachment.innerHomeomorph line 594

    Source documentation

    Actual pairwise-disjoint open top-dimensional cells, including arbitrary index universes, with their ordinary disk interiors.

    def innerHomeomorph : (Σ _ : J, OpenDisk n) ≃ₜ a.inner :=
…

    Mentions: OAI.EilenbergGanea.CWCollar.OpenDisk

  82. abbrev OAI.EilenbergGanea.CWCollar.Annulus line 604
  83. def OAI.EilenbergGanea.CWCollar.annulusSigmaIn line 606
  84. theorem OAI.EilenbergGanea.CWCollar.annulusSigmaIn_continuous line 609
  85. theorem OAI.EilenbergGanea.CWCollar.annulusSigmaIn_openMap line 612
  86. def OAI.EilenbergGanea.CWCollar.annulusSigmaHomeomorph line 616
  87. def OAI.EilenbergGanea.CWCollar.Attachment.innerOuterHomeomorph line 628
  88. def OAI.EilenbergGanea.CWCollar.Attachment.annulusHomeomorph line 638

    Source documentation

    The actual overlap of the two CW collar open sets is the disjoint union of punctured open disks, even for an unrestricted cell index.

    def annulusHomeomorph : (Σ _ : J, Annulus n) ≃ₜ (a.outer ∩ a.inner : Set X) :=
…

    Mentions: OAI.EilenbergGanea.CWCollar.Annulus

  89. def OAI.EilenbergGanea.CWCollar.openDiskBallHomeomorph line 651
  90. def OAI.EilenbergGanea.CWCollar.spaceOpenDiskHomeomorph line 659
  91. theorem OAI.EilenbergGanea.CWCollar.spaceOpenDiskHomeomorph_zero line 662
  92. def OAI.EilenbergGanea.CWCollar.puncturedAnnulusHomeomorph line 665
  93. instance OAI.EilenbergGanea.CWCollar.annulusTwoPathConnected line 680
  94. def OAI.EilenbergGanea.CWCollar.planeComplexHomeomorph line 692
  95. theorem OAI.EilenbergGanea.CWCollar.planeComplexHomeomorph_zero line 695
  96. def OAI.EilenbergGanea.CWCollar.puncturedPlaneComplexHomeomorph line 698
  97. def OAI.EilenbergGanea.CWCollar.circleSphereHomeomorph line 712
  98. def OAI.EilenbergGanea.CWCollar.annulusCircleProdHomeomorph line 715
  99. instance OAI.EilenbergGanea.CWCollar.positiveRealsContractible line 719
  100. def OAI.EilenbergGanea.CWCollar.annulusCircleEquiv line 722
  101. def OAI.EilenbergGanea.CWCollar.homotopyFundamentalEquiv line 727
  102. def OAI.EilenbergGanea.CWCollar.periodIntEquiv line 732
  103. def OAI.EilenbergGanea.CWCollar.circleFundamentalInt line 748
  104. def OAI.EilenbergGanea.CWCollar.annulusFundamentalInt line 754
  105. def OAI.EilenbergGanea.CWCollar.annulusOppositeInt line 763
  106. def OAI.EilenbergGanea.CWCollar.annulusAbInt line 766
  107. def OAI.EilenbergGanea.CWCollar.annulusHomologyInt line 769
  108. def OAI.EilenbergGanea.CWCollar.annulusGenerator line 772
  109. theorem OAI.EilenbergGanea.CWCollar.annulusGenerator_class line 775
  110. theorem OAI.EilenbergGanea.CWCollar.annulus_loop_power line 780
  111. def OAI.EilenbergGanea.CWCollar.loopCycle line 790
  112. def OAI.EilenbergGanea.CWCollar.loopHomology line 797
  113. theorem OAI.EilenbergGanea.CWCollar.hurewiczOne_loop line 800
  114. theorem OAI.EilenbergGanea.CWCollar.annulusGenerator_homology line 807