OAI/Algebra/GroupRing/CellularFurther2.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GroupRingTopology.Cellular.skeletonBoundary line 26

   Source documentation

   The actual attaching maps of a classical CW skeleton.

   def skeletonBoundary (n : ℕ) (i : RelCWComplex.cell C n) :
       C(Attachment.Sphere n,Skeleton C n) :=
   …

   Mentions: OAI.GroupRingTopology.Attachment.Sphere, OAI.GroupRingTopology.Cellular.Skeleton

2. def OAI.GroupRingTopology.Cellular.skeletonBase line 31
3. def OAI.GroupRingTopology.Cellular.skeletonCell line 34
4. def OAI.GroupRingTopology.Cellular.skeletonAssembly line 39
5. lemma OAI.GroupRingTopology.Cellular.skeletonAssembly_base line 42
6. lemma OAI.GroupRingTopology.Cellular.skeletonAssembly_cell line 46
7. lemma OAI.GroupRingTopology.Cellular.skeletonAssembly_interior line 50
8. lemma OAI.GroupRingTopology.Cellular.skeletonAssembly_injective line 54
9. lemma OAI.GroupRingTopology.Cellular.skeletonAssembly_surjective line 84
10. lemma OAI.GroupRingTopology.Cellular.skeletonAssembly_closed line 99
11. def OAI.GroupRingTopology.Cellular.skeletonHomeomorph line 146

    Source documentation

    A classical CW skeleton is literally the topological adjunction of the previous skeleton and its disks, including arbitrary infinite cell families.

    def skeletonHomeomorph (n : ℕ) :
        Attachment.Space (skeletonBoundary (C := C) n) ≃ₜ Skeleton C (n+1) :=
    …

    Mentions: OAI.GroupRingTopology.Attachment.Space, OAI.GroupRingTopology.Cellular.skeletonBoundary, OAI.GroupRingTopology.Cellular.Skeleton

12. lemma OAI.GroupRingTopology.Cellular.skeleton_smul_mem line 165
13. def OAI.GroupRingTopology.Cellular.skeletonTranslate line 175
14. lemma OAI.GroupRingTopology.Cellular.skeletonTranslate_base line 179
15. lemma OAI.GroupRingTopology.Cellular.skeletonTranslate_cell line 183
16. lemma OAI.GroupRingTopology.Cellular.exists_equivariant_skeleton_extension line 191
17. lemma OAI.GroupRingTopology.Cellular.exists_equivariant_skeleton_lift line 257
18. lemma OAI.GroupRingTopology.Cellular.isEmpty_skeleton_zero line 343
19. lemma OAI.GroupRingTopology.Cellular.exists_equivariant_lift_on_skeleton line 353
20. lemma OAI.GroupRingTopology.Cellular.exists_equivariant_map_on_skeleton line 370
21. lemma OAI.GroupRingTopology.Cellular.exists_equivariant_homotopy_on_skeleton line 384
22. def OAI.GroupRingTopology.Cellular.skeletonChart line 405
23. lemma OAI.GroupRingTopology.Cellular.skeleton_compact_representatives line 410