OAI/Algebra/GroupRing/PartialLift.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GroupRingTopology.Cellular.PartialLift.onSphere line 18

   Source documentation

   The boundary lift for attaching an n-cell.

   def onSphere (a : PartialLift (C := C) p f n) (i : RelCWComplex.cell C n) :
   …

   Mentions: OAI.GroupRingTopology.Cellular.PartialLift

2. lemma OAI.GroupRingTopology.Cellular.PartialLift.exists_cell_extension line 25
3. def OAI.GroupRingTopology.Cellular.PartialLift.next line 35

   Source documentation

   Extend a partial lift across all cells of the next dimension.

   noncomputable def next (a : PartialLift (C := C) p f n) (hp : DiskRLP p) :
   …

   Mentions: OAI.GroupRingTopology.Cellular.PartialLift, OAI.GroupRingTopology.Cellular.DiskRLP

4. lemma OAI.GroupRingTopology.Cellular.PartialLift.next_eq line 53
5. def OAI.GroupRingTopology.Cellular.PartialLift.zero line 58
6. def OAI.GroupRingTopology.Cellular.stages line 71
7. lemma OAI.GroupRingTopology.Cellular.stages_agree line 75
8. lemma OAI.GroupRingTopology.Cellular.exists_skeleton line 82
9. def OAI.GroupRingTopology.Cellular.liftValue line 86
10. lemma OAI.GroupRingTopology.Cellular.liftValue_eq line 91
11. lemma OAI.GroupRingTopology.Cellular.continuousOn_liftValue line 101
12. lemma OAI.GroupRingTopology.Cellular.liftValue_fac line 112
13. theorem OAI.GroupRingTopology.Cellular.exists_lift line 118
14. def OAI.GroupRingTopology.Cellular.SphereFillable line 129

    Source documentation

    Extension property with respect to the actual sup-norm disks.

    def SphereFillable (Y : Type u) [TopologicalSpace Y] : Prop :=
    …

15. lemma OAI.GroupRingTopology.Cellular.disk_coord line 132
16. lemma OAI.GroupRingTopology.Cellular.disk_mem line 136
17. def OAI.GroupRingTopology.Cellular.diskCons line 141
18. lemma OAI.GroupRingTopology.Cellular.continuous_diskCons line 149
19. def OAI.GroupRingTopology.Cellular.diskTail line 160
20. lemma OAI.GroupRingTopology.Cellular.continuous_diskTail line 163
21. def OAI.GroupRingTopology.Cellular.diskTime line 167
22. lemma OAI.GroupRingTopology.Cellular.continuous_diskTime line 170
23. lemma OAI.GroupRingTopology.Cellular.diskTail_cons line 173
24. lemma OAI.GroupRingTopology.Cellular.diskTime_cons line 178
25. lemma OAI.GroupRingTopology.Cellular.sphere_iff_coord line 184
26. lemma OAI.GroupRingTopology.Cellular.cons_mem_sphere_of_boundary line 190
27. lemma OAI.GroupRingTopology.Cellular.cons_zero_mem_sphere line 195
28. lemma OAI.GroupRingTopology.Cellular.cons_one_mem_sphere line 200
29. lemma OAI.GroupRingTopology.Cellular.sphere_split line 205
30. lemma OAI.GroupRingTopology.Cellular.continuous_liftCover line 216

    Source documentation

    Finite closed pasting, in a form usable for the three cylinder faces.

    lemma continuous_liftCover {A : Type u} {Y : Type v} {ι : Type w}
        [TopologicalSpace A] [TopologicalSpace Y] [Finite ι]
        (S : ι → Set A) (f : ∀ i, C(S i,Y))
        (hcompat : ∀ i j x (hi : x ∈ S i) (hj : x ∈ S j), f i ⟨x,hi⟩ = f j ⟨x,hj⟩)
        (hcover : ⋃ i, S i = Set.univ) (hclosed : ∀ i, IsClosed (S i)) :
        Continuous (Set.liftCover S (fun i => f i) hcompat hcover) := by
    …

31. def OAI.GroupRingTopology.Cellular.cylinderFace line 227
32. lemma OAI.GroupRingTopology.Cellular.cylinderFace_closed line 232
33. lemma OAI.GroupRingTopology.Cellular.cylinderFace_cover line 241
34. def OAI.GroupRingTopology.Cellular.pathEndpoint line 251
35. def OAI.GroupRingTopology.Cellular.faceTail line 257
36. def OAI.GroupRingTopology.Cellular.faceSphere line 261
37. def OAI.GroupRingTopology.Cellular.faceTime line 264
38. def OAI.GroupRingTopology.Cellular.faceMap line 268
39. lemma OAI.GroupRingTopology.Cellular.faceTime_eq_zero line 276
40. lemma OAI.GroupRingTopology.Cellular.faceTime_eq_one line 283
41. lemma OAI.GroupRingTopology.Cellular.faceMap_compat line 293
42. def OAI.GroupRingTopology.Cellular.cylinderBoundaryMap line 326
43. lemma OAI.GroupRingTopology.Cellular.cylinderBoundaryMap_face line 331
44. theorem OAI.GroupRingTopology.Cellular.pathEndpoint_RLP line 340

    Source documentation

    A disk filling extends the three compatible boundary faces of a cylinder.

    theorem pathEndpoint_RLP (hY : SphereFillable Y) : DiskRLP (@pathEndpoint Y _) := by
    …

    Mentions: OAI.GroupRingTopology.Cellular.SphereFillable, OAI.GroupRingTopology.Cellular.DiskRLP, OAI.GroupRingTopology.Cellular.pathEndpoint

45. theorem OAI.GroupRingTopology.Cellular.contractible_of_sphereFillable line 381