OAI/Algebra/GroupRing/CayleyFurther.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GroupRingTopology.Cayley.vertex_action line 23
2. lemma OAI.GroupRingTopology.Cayley.pathGenerator_equal line 26
3. lemma OAI.GroupRingTopology.Cayley.edge_smul_equal line 32
4. def OAI.GroupRingTopology.Cayley.coherentClass line 47
5. def OAI.GroupRingTopology.Cayley.coherentPath line 49
6. lemma OAI.GroupRingTopology.Cayley.coherentPath_equal line 51
7. lemma OAI.GroupRingTopology.Cayley.coherentPath_edge line 57
8. def OAI.GroupRingTopology.Cayley.nullhomotopyOfSection line 77
9. lemma OAI.GroupRingTopology.Cayley.presentationSection_generator line 88
10. def OAI.GroupRingTopology.Cayley.presentationGraphNullhomotopy line 100
11. lemma OAI.GroupRingTopology.Attachment.exists_equivariant_extension line 116

    Source documentation

    Fill one disk per orbit and translate the fillings, preserving the action.

    lemma exists_equivariant_extension (f : C(X,Y))
        (hf : ∀ (g : G) x, f (g • x) = g • f x) (hY : Cellular.SphereFillable Y) :
        ∃ F : C(Space (equivariantFamily (G := G) a),Y),
    …

    Mentions: OAI.GroupRingTopology.Cellular.SphereFillable, OAI.GroupRingTopology.Attachment.Space, OAI.GroupRingTopology.Attachment.equivariantFamily

12. lemma OAI.GroupRingTopology.Attachment.compactFundamentalSet line 135

    Source documentation

    Finitely many free cell orbits preserve existence of a compact fundamental set.

    lemma compactFundamentalSet [Finite ι] (hX : Milnor.CompactFundamentalSet G (X := X)) :
    …

    Mentions: OAI.GroupRingTopology.Milnor.CompactFundamentalSet

13. lemma OAI.GroupRingTopology.Milnor.group_compactFundamentalSet line 163
14. lemma OAI.GroupRingTopology.Milnor.graph_compactFundamentalSet line 168
15. lemma OAI.GroupRingTopology.Milnor.presentation_compactFundamentalSet line 172
16. lemma OAI.GroupRingTopology.Milnor.presentation_equivariant_map line 178
17. lemma OAI.GroupRingTopology.Milnor.exists_stage_section line 192

    Source documentation

    Finite presentability supplies a coherent group section in ONE Milnor stage. This is genuine low-dimensional control, not a simply-connected-stage assumption.

    lemma exists_stage_section [Finite A] (hrels : rels.Finite)
        (hs : Function.Surjective (FreeGroup.lift s))
        (hker : (FreeGroup.lift s).ker = Subgroup.normalClosure rels) :
        ∃ (S : Shapes G) (x : Stage G S) (τ : G →* PathExtension.Extension G x), ∀ g, (τ g).1 = g := by
    …

    Mentions: OAI.GroupRingTopology.Milnor.Shapes, OAI.GroupRingTopology.Milnor.Stage, OAI.GroupRingTopology.PathExtension.Extension

18. def OAI.GroupRingTopology.Attachment.cellCenter line 212
19. def OAI.GroupRingTopology.Attachment.punctured line 213
20. def OAI.GroupRingTopology.Attachment.rawCoordinate line 215
21. lemma OAI.GroupRingTopology.Attachment.base_mem_punctured line 218
22. lemma OAI.GroupRingTopology.Attachment.cell_mem_punctured line 222
23. lemma OAI.GroupRingTopology.Attachment.punctured_open line 245
24. lemma OAI.GroupRingTopology.Attachment.continuous_punctured line 263
25. abbrev OAI.GroupRingTopology.Attachment.PuncturedDisk line 305
26. def OAI.GroupRingTopology.Attachment.puncturedBoundary line 307
27. def OAI.GroupRingTopology.Attachment.puncturedCell line 316
28. def OAI.GroupRingTopology.Attachment.puncturedBase line 319
29. lemma OAI.GroupRingTopology.Attachment.puncturedCell_boundary line 321
30. def OAI.GroupRingTopology.Attachment.puncturedLift line 325
31. lemma OAI.GroupRingTopology.Attachment.puncturedLift_base line 356
32. lemma OAI.GroupRingTopology.Attachment.puncturedLift_cell line 361
33. lemma OAI.GroupRingTopology.Attachment.punctured_surjective line 380
34. def OAI.GroupRingTopology.Attachment.radialSphere line 390

    Source documentation

    Radial projection of a nonzero disk point onto its sphere.

    def radialSphere : C(PuncturedDisk n,Sphere n) := by
    …

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

35. lemma OAI.GroupRingTopology.Attachment.radialSphere_boundary line 399
36. def OAI.GroupRingTopology.Attachment.radialDisk line 406

    Source documentation

    Radial straight-line deformation, in the full disk.

    def radialDisk : C(unitInterval × PuncturedDisk n,Disk n) := by
    …

    Mentions: OAI.GroupRingTopology.Attachment.PuncturedDisk, OAI.GroupRingTopology.Attachment.Disk

37. lemma OAI.GroupRingTopology.Attachment.radialDisk_zero line 420
38. lemma OAI.GroupRingTopology.Attachment.radialDisk_one line 423
39. lemma OAI.GroupRingTopology.Attachment.radialDisk_boundary line 426