OAI/Algebra/GroupRing/HomotopyFunctor.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GroupRingTopology.HomotopyFunctor.map_eq_of_homotopy line 16
2. abbrev OAI.GroupRingTopology.Milnor.Shapes line 35
3. def OAI.GroupRingTopology.Milnor.basedShapes line 36
4. def OAI.GroupRingTopology.Milnor.stage line 37
5. lemma OAI.GroupRingTopology.Milnor.stage_mono line 39
6. lemma OAI.GroupRingTopology.Milnor.stage_point_face line 42
7. def OAI.GroupRingTopology.Milnor.stagePoint line 47
8. def OAI.GroupRingTopology.Milnor.stageIncl line 51
9. lemma OAI.GroupRingTopology.Milnor.stageIncl_point line 54
10. def OAI.GroupRingTopology.Milnor.stageHom line 57
11. instance OAI.GroupRingTopology.Milnor.(instance at line 62) line 62
12. instance OAI.GroupRingTopology.Milnor.(instance at line 78) line 78
13. instance OAI.GroupRingTopology.Milnor.(instance at line 93) line 93
14. lemma OAI.GroupRingTopology.Milnor.smul_weight line 96
15. lemma OAI.GroupRingTopology.Milnor.smul_weight_inv line 104
16. lemma OAI.GroupRingTopology.Milnor.exists_disjoint_nhds line 107
17. lemma OAI.GroupRingTopology.Milnor.quotientCovering line 126
18. abbrev OAI.GroupRingTopology.Milnor.Stage line 140
19. def OAI.GroupRingTopology.Milnor.stageFull line 142
20. lemma OAI.GroupRingTopology.Milnor.stageFull_embedding line 144
21. lemma OAI.GroupRingTopology.Milnor.stage_translate line 147
22. def OAI.GroupRingTopology.Milnor.stageSmul line 150
23. instance OAI.GroupRingTopology.Milnor.stageAction line 153
24. instance OAI.GroupRingTopology.Milnor.stageContinuousAction line 169
25. lemma OAI.GroupRingTopology.Milnor.stageFull_smul line 172
26. lemma OAI.GroupRingTopology.Milnor.stageIncl_smul line 174
27. lemma OAI.GroupRingTopology.Milnor.compact_controlled line 178

    Source documentation

    Any one compact set is contained in a finite-orbit Milnor stage.

    lemma compact_controlled {K : Set (Space G)} (hK : IsCompact K) :
        ∃ S : Shapes G, K ⊆ Set.range (stageFull G S) := by
    …

    Mentions: OAI.GroupRingTopology.Milnor.Space, OAI.GroupRingTopology.Milnor.Shapes, OAI.GroupRingTopology.Milnor.stageFull

28. lemma OAI.GroupRingTopology.Milnor.compact_orbit_controlled line 189

    Source documentation

    Arbitrarily many translates of a compact set have ONE controlled target.

    lemma compact_orbit_controlled {K : Set (Space G)} (hK : IsCompact K) :
        ∃ S : Shapes G, ∀ g : G, (g • ·) '' K ⊆ Set.range (stageFull G S) := by
    …

    Mentions: OAI.GroupRingTopology.Milnor.Space, OAI.GroupRingTopology.Milnor.Shapes, OAI.GroupRingTopology.Milnor.stageFull

29. def OAI.GroupRingTopology.Milnor.CompactFundamentalSet line 200

    Source documentation

    A compact fundamental set need not be disjoint or a strict domain.

    def CompactFundamentalSet : Prop :=
    …

30. lemma OAI.GroupRingTopology.Milnor.equivariant_controlled line 203
31. def OAI.GroupRingTopology.Milnor.factorStage line 216

    Source documentation

    Factoring through a stage preserves topology and equivariance, rather than only factoring an underlying set map.

    def factorStage (f : C(X,Space G)) (S : Shapes G)
        (hf : Set.range f ⊆ Set.range (stageFull G S)) : C(X,Stage G S) where
    …

    Mentions: OAI.GroupRingTopology.Milnor.Space, OAI.GroupRingTopology.Milnor.Shapes, OAI.GroupRingTopology.Milnor.stageFull, OAI.GroupRingTopology.Milnor.Stage

32. lemma OAI.GroupRingTopology.Milnor.factorStage_spec line 224
33. lemma OAI.GroupRingTopology.Milnor.factorStage_smul line 227
34. abbrev OAI.GroupRingTopology.Attachment.Disk line 237
35. abbrev OAI.GroupRingTopology.Attachment.Sphere line 238
36. abbrev OAI.GroupRingTopology.Attachment.OpenDisk line 239
37. def OAI.GroupRingTopology.Attachment.boundary line 241
38. def OAI.GroupRingTopology.Attachment.interior line 243
39. lemma OAI.GroupRingTopology.Attachment.continuous_boundary line 245
40. lemma OAI.GroupRingTopology.Attachment.continuous_interior line 247
41. lemma OAI.GroupRingTopology.Attachment.boundary_closedEmbedding line 249
42. def OAI.GroupRingTopology.Attachment.Space line 256

    Source documentation

    The points of an adjunction are the old points and the interiors of the new disks.

    def Space (_a : ι → C(Sphere n,X)) := X ⊕ (Σ _ : ι, OpenDisk n)

    Mentions: OAI.GroupRingTopology.Attachment.Sphere, OAI.GroupRingTopology.Attachment.OpenDisk

43. def OAI.GroupRingTopology.Attachment.quotient line 258
44. instance OAI.GroupRingTopology.Attachment.(instance at line 270) line 270
45. lemma OAI.GroupRingTopology.Attachment.quotient_inl line 272
46. lemma OAI.GroupRingTopology.Attachment.quotient_interior line 274
47. lemma OAI.GroupRingTopology.Attachment.quotient_boundary line 280
48. lemma OAI.GroupRingTopology.Attachment.quotient_surjective line 289
49. lemma OAI.GroupRingTopology.Attachment.continuous_quotient line 295
50. def OAI.GroupRingTopology.Attachment.base line 298

    Source documentation

    The old space embeds as a closed subspace of the adjunction.

    def base : X → Space a := Sum.inl

    Mentions: OAI.GroupRingTopology.Attachment.Space

51. def OAI.GroupRingTopology.Attachment.cell line 299
52. lemma OAI.GroupRingTopology.Attachment.continuous_base line 302
53. lemma OAI.GroupRingTopology.Attachment.cell_boundary line 305
54. lemma OAI.GroupRingTopology.Attachment.cell_interior line 307
55. lemma OAI.GroupRingTopology.Attachment.continuous_iff line 310
56. lemma OAI.GroupRingTopology.Attachment.isClosed_iff line 316
57. lemma OAI.GroupRingTopology.Attachment.cell_preimage_base_image line 322
58. lemma OAI.GroupRingTopology.Attachment.base_isClosedMap line 352
59. lemma OAI.GroupRingTopology.Attachment.base_closedEmbedding line 362
60. def OAI.GroupRingTopology.Attachment.lift line 367

    Source documentation

    The universal mapping property, with all attaching equations explicit.

    noncomputable def lift {Y : Type w} [TopologicalSpace Y] (f : C(X,Y))
        (g : ι → C(Disk n,Y)) (h : ∀ i x, g i (boundary n x) = f (a i x)) : C(Space a,Y) := by
    …

    Mentions: OAI.GroupRingTopology.Attachment.Disk, OAI.GroupRingTopology.Attachment.boundary, OAI.GroupRingTopology.Attachment.Space

61. lemma OAI.GroupRingTopology.Attachment.lift_base line 386
62. lemma OAI.GroupRingTopology.Attachment.lift_cell line 390
63. lemma OAI.GroupRingTopology.Attachment.lift_unique line 405
64. lemma OAI.GroupRingTopology.Attachment.interior_openEmbedding line 414
65. def OAI.GroupRingTopology.Attachment.openCell line 418

    Source documentation

    Open disks are inserted as genuine open embeddings.

    def openCell (i : ι) : OpenDisk n → Space a := fun x => Sum.inr ⟨i,x⟩

    Mentions: OAI.GroupRingTopology.Attachment.OpenDisk, OAI.GroupRingTopology.Attachment.Space

66. lemma OAI.GroupRingTopology.Attachment.openCell_eq line 420
67. lemma OAI.GroupRingTopology.Attachment.quotient_preimage_openCell_image line 424
68. lemma OAI.GroupRingTopology.Attachment.openCell_openEmbedding line 472
69. lemma OAI.GroupRingTopology.Attachment.exists_real_extension line 484

    Source documentation

    Real-valued maps on the old space extend over any family of attached disks.

    lemma exists_real_extension (f : C(X,ℝ)) :
        ∃ F : C(Space a,ℝ), ∀ x, F (base a x) = f x := by
    …

    Mentions: OAI.GroupRingTopology.Attachment.Space, OAI.GroupRingTopology.Attachment.base

70. def OAI.GroupRingTopology.Attachment.RealSeparated line 495

    Source documentation

    Functional Hausdorffness is convenient for iterated attachments: separating functions, unlike chosen open neighborhoods, extend across every new disk.

    def RealSeparated (Y : Type*) [TopologicalSpace Y] : Prop :=
    …

71. lemma OAI.GroupRingTopology.Attachment.RealSeparated.t2Space line 498
72. lemma OAI.GroupRingTopology.Attachment.realSeparated_of_tychonoff line 505
73. lemma OAI.GroupRingTopology.Attachment.exists_interior_separator line 515
74. lemma OAI.GroupRingTopology.Attachment.realSeparated line 581
75. lemma OAI.GroupRingTopology.Attachment.t2Space line 609
76. def OAI.GroupRingTopology.Attachment.characteristic line 615

    Source documentation

    The characteristic map is defined on the entire parameter space, as required by Mathlib's classical CW definition, but only its closed-disk values matter.

    def characteristic (i : ι) (x : Fin n → ℝ) : Space a := by
    …

    Mentions: OAI.GroupRingTopology.Attachment.Space

77. lemma OAI.GroupRingTopology.Attachment.characteristic_disk line 619
78. lemma OAI.GroupRingTopology.Attachment.characteristic_open line 623
79. lemma OAI.GroupRingTopology.Attachment.characteristic_bijOn line 627
80. def OAI.GroupRingTopology.Attachment.characteristicPE line 640
81. lemma OAI.GroupRingTopology.Attachment.characteristicPE_continuousOn line 643
82. lemma OAI.GroupRingTopology.Attachment.characteristicPE_continuousOn_symm line 652
83. lemma OAI.GroupRingTopology.Attachment.characteristicPE_image_ball line 666
84. lemma OAI.GroupRingTopology.Attachment.characteristicPE_image_closedBall line 670
85. abbrev OAI.GroupRingTopology.Attachment.CellIndex line 679
86. def OAI.GroupRingTopology.Attachment.cellMap line 681
87. def OAI.GroupRingTopology.Attachment.relCWComplex line 690

    Source documentation

    Attaching disks is a classical relative CW complex, not merely an abstract cell-complex object in a category.

    def relCWComplex : RelCWComplex (Set.univ : Set (Space a)) (Set.range (base a)) where
    …

    Mentions: OAI.GroupRingTopology.Attachment.Space, OAI.GroupRingTopology.Attachment.base