OAI/Algebra/GroupRing/Path.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TorsionFreeZeroDivisors.GraphPresentation.Path.join_rotation line 11
2. lemma OAI.TorsionFreeZeroDivisors.GraphPresentation.Path.end_rotation line 21
3. lemma OAI.TorsionFreeZeroDivisors.GraphPresentation.Path.first_get line 31
4. lemma OAI.TorsionFreeZeroDivisors.GraphPresentation.Path.closed_rotation line 33
5. def OAI.TorsionFreeZeroDivisors.WordBlocks.AllClosed line 47
6. lemma OAI.TorsionFreeZeroDivisors.WordBlocks.closed_consistent line 48
7. def OAI.TorsionFreeZeroDivisors.WordBlocks.root line 59
8. lemma OAI.TorsionFreeZeroDivisors.WordBlocks.root_begin line 60
9. lemma OAI.TorsionFreeZeroDivisors.WordBlocks.boundary_join line 61
10. lemma OAI.TorsionFreeZeroDivisors.WordBlocks.boundary_end line 69
11. def OAI.TorsionFreeZeroDivisors.WordBlocks.LiftedMatching.picture line 77

    Source documentation

    All endpoints are furnished by literal graph paths, not by equality of labels. Inserting the single exterior marker gives an actual finite picture.

    def LiftedMatching.picture (d : LiftedMatching label inv (p.darts::ws)) (hc : AllClosed Γ ws) :
        FinitePicture.Data (O:=Option (Occ (p.darts::ws))) Γ label inv x y :=
    …

    Mentions: OAI.TorsionFreeZeroDivisors.WordBlocks.LiftedMatching, OAI.TorsionFreeZeroDivisors.WordBlocks.AllClosed, OAI.TorsionFreeZeroDivisors.FinitePicture.Data, OAI.TorsionFreeZeroDivisors.WordBlocks.Occ

12. lemma OAI.TorsionFreeZeroDivisors.AlgebraicPictures.quotient_direct_matching line 88
13. abbrev OAI.TorsionFreeZeroDivisors.InitialPicture.Loop line 102
14. def OAI.TorsionFreeZeroDivisors.InitialPicture.relWords line 104
15. def OAI.TorsionFreeZeroDivisors.InitialPicture.signedLoop line 105
16. lemma OAI.TorsionFreeZeroDivisors.InitialPicture.signedLoop_letters line 108
17. def OAI.TorsionFreeZeroDivisors.InitialPicture.innerWords line 114
18. lemma OAI.TorsionFreeZeroDivisors.InitialPicture.innerWords_labels line 117
19. lemma OAI.TorsionFreeZeroDivisors.InitialPicture.innerWords_closed line 123
20. theorem OAI.TorsionFreeZeroDivisors.InitialPicture.lifted_matching line 132

    Source documentation

    Algebraic nullity produces an actual lifted full matching on the given outer path and literal signed closed relators. Empty relators are allowed.

    theorem lifted_matching (h : PresentedGroup.mk (relations (relWords Γ label rel))
          (FreeGroup.mk (p.letters label))=1) :
        ∃ts : List (Term (A:=A) (I:=I)),Nonempty
    …

    Mentions: OAI.TorsionFreeZeroDivisors.InitialPicture.relWords

21. theorem OAI.TorsionFreeZeroDivisors.InitialPicture.exists_picture line 143

    Source documentation

    The initial finite marked certificate is derived from nullity in the literal graph-loop presentation. No preexisting picture, surface map, or asphericity hypothesis is assumed.

    theorem exists_picture (hxy : x≠y)
        (h : PresentedGroup.mk (relations (relWords Γ label rel)) (FreeGroup.mk (p.letters label))=1) :
        ∃(O : Type) (_ : Fintype O),Nonempty
          (FinitePicture.Data (O:=O) Γ label WordPairing.inverseLetter x y) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.InitialPicture.relWords, OAI.TorsionFreeZeroDivisors.FinitePicture.Data, OAI.TorsionFreeZeroDivisors.WordPairing.inverseLetter

22. structure OAI.TorsionFreeZeroDivisors.GraphPresentation.Routes line 160

    Source documentation

    A finite choice of routes from the same base on each graph component.

    structure Routes where
    …

23. def OAI.TorsionFreeZeroDivisors.GraphPresentation.word line 166
24. def OAI.TorsionFreeZeroDivisors.GraphPresentation.relator line 167
25. def OAI.TorsionFreeZeroDivisors.GraphPresentation.relations line 169
26. abbrev OAI.TorsionFreeZeroDivisors.GraphPresentation.Group line 170
27. def OAI.TorsionFreeZeroDivisors.GraphPresentation.value line 171
28. def OAI.TorsionFreeZeroDivisors.GraphPresentation.letter line 172
29. lemma OAI.TorsionFreeZeroDivisors.GraphPresentation.edge line 173
30. lemma OAI.TorsionFreeZeroDivisors.GraphPresentation.path_value line 180

    Source documentation

    Every literal path has the source's path-order value, independently of which route was chosen to define the finite fundamental-cycle presentation.

    lemma path_value {a b : V} (p : Path Γ a b) :
        p.eval (letter Γ letters R)=(value Γ letters R a)⁻¹*value Γ letters R b := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.GraphPresentation.Path, OAI.TorsionFreeZeroDivisors.GraphPresentation.letter, OAI.TorsionFreeZeroDivisors.GraphPresentation.value

31. lemma OAI.TorsionFreeZeroDivisors.GraphPresentation.closed_value line 187
32. def OAI.TorsionFreeZeroDivisors.GraphPresentation.loopLabels line 192

    Source documentation

    Labels of all closed walks, exactly as in the cone presentation.

    def loopLabels : Set (FreeGroup S) := {w | ∃ a,∃ p : Path Γ a a,p.eval letters=w}

    Mentions: OAI.TorsionFreeZeroDivisors.GraphPresentation.Path

33. lemma OAI.TorsionFreeZeroDivisors.GraphPresentation.loopLabels_subset_closure line 193
34. lemma OAI.TorsionFreeZeroDivisors.GraphPresentation.relator_mem_loopLabels line 200
35. theorem OAI.TorsionFreeZeroDivisors.GraphPresentation.normalClosure_eq_loops line 211

    Source documentation

    The finite edge-route presentation has precisely the normal closure of all labels of graph loops, not merely some chosen graph relations.

    theorem normalClosure_eq_loops
        (hl : ∀ d,letters (Γ.reverse d)=(letters d)⁻¹) :
        Subgroup.normalClosure (relations Γ letters R)=Subgroup.normalClosure (loopLabels Γ letters) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.GraphPresentation.relations, OAI.TorsionFreeZeroDivisors.GraphPresentation.loopLabels

36. instance OAI.TorsionFreeZeroDivisors.GraphPresentation.(instance at line 220) line 220
37. def OAI.TorsionFreeZeroDivisors.GraphPresentation.loopPath line 230
38. def OAI.TorsionFreeZeroDivisors.GraphPresentation.roseLabel line 233
39. lemma OAI.TorsionFreeZeroDivisors.GraphPresentation.roseLabel_reverse line 235
40. lemma OAI.TorsionFreeZeroDivisors.GraphPresentation.loopPath_word line 239
41. lemma OAI.TorsionFreeZeroDivisors.GraphPresentation.loopPath_relations line 247
42. theorem OAI.TorsionFreeZeroDivisors.GraphPresentation.route_picture line 257

    Source documentation

    A null word in the finite EDGE-ROUTE presentation used for the main construction has an initial literal lifted picture; no relators were enlarged or replaced by assumed graph-loop relations.

    theorem route_picture {x y : V} (p : Path Γ x y) (hxy : x≠y)
        (h : p.eval (letter Γ (roseLabel label) R)=1) :
        ∃(O : Type) (_ : Fintype O),Nonempty
          (FinitePicture.Data (O:=O) Γ label WordPairing.inverseLetter x y) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.GraphPresentation.Path, OAI.TorsionFreeZeroDivisors.GraphPresentation.letter, OAI.TorsionFreeZeroDivisors.GraphPresentation.roseLabel, OAI.TorsionFreeZeroDivisors.FinitePicture.Data, OAI.TorsionFreeZeroDivisors.WordPairing.inverseLetter

43. def OAI.TorsionFreeZeroDivisors.FinitePicture.Data.relabel line 276

    Source documentation

    Relabel the alphabet, retaining the actual graph dart and endpoint data. This does not change the path, partner, rotation, or exterior marker.

    def relabel : Data (O:=O) Γ label' inv' x y := {a with
    …

    Mentions: OAI.TorsionFreeZeroDivisors.FinitePicture.Data

44. def OAI.TorsionFreeZeroDivisors.GraphPresentation.Path.ofWalk line 293
45. def OAI.TorsionFreeZeroDivisors.GraphPresentation.routes line 299
46. def OAI.TorsionFreeZeroDivisors.ConcreteGroup.freeLetter line 312

    Source documentation

    The literal rose letters, with the fixed source inverse pairing.

    def freeLetter (t : Types.Letter) : FreeGroup Types.Generator :=
    …

    Mentions: OAI.TorsionFreeZeroDivisors.Types.Letter, OAI.TorsionFreeZeroDivisors.Types.Generator

47. lemma OAI.TorsionFreeZeroDivisors.ConcreteGroup.freeLetter_inverse line 315
48. abbrev OAI.TorsionFreeZeroDivisors.ConcreteGroup.Γ line 320
49. def OAI.TorsionFreeZeroDivisors.ConcreteGroup.labels line 321
50. lemma OAI.TorsionFreeZeroDivisors.ConcreteGroup.labels_reverse line 322
51. def OAI.TorsionFreeZeroDivisors.ConcreteGroup.routes line 324
52. abbrev OAI.TorsionFreeZeroDivisors.ConcreteGroup.G line 325
53. def OAI.TorsionFreeZeroDivisors.ConcreteGroup.value line 326
54. def OAI.TorsionFreeZeroDivisors.ConcreteGroup.letter line 327
55. instance OAI.TorsionFreeZeroDivisors.ConcreteGroup.(instance at line 328) line 328
56. lemma OAI.TorsionFreeZeroDivisors.ConcreteGroup.presentation_exact line 329
57. lemma OAI.TorsionFreeZeroDivisors.ConcreteGroup.edge line 333
58. lemma OAI.TorsionFreeZeroDivisors.ConcreteGroup.path_value line 336
59. lemma OAI.TorsionFreeZeroDivisors.ConcreteGroup.freeLetter_mk line 343
60. lemma OAI.TorsionFreeZeroDivisors.ConcreteGroup.signed_label_reverse line 347
61. lemma OAI.TorsionFreeZeroDivisors.ConcreteGroup.letter_signed line 352
62. theorem OAI.TorsionFreeZeroDivisors.ConcreteGroup.reduced_picture line 357

    Source documentation

    A literal path null in the exact constructed group yields a reduced finite marked disk picture on the original source alphabet and graph darts.

    theorem reduced_picture {z w : VA rep⊕VB rep} (p : GraphPresentation.Path (Γ rep r) z w)
        (hzw : z≠w) (h : p.eval (letter rep r ∘ SampleGraph.label rep)=1) :
        ∃n,∃a : FinitePicture.Data (O:=Fin n) (Γ rep r) (SampleGraph.label rep) Types.inverse z w,
    …

    Mentions: OAI.TorsionFreeZeroDivisors.GraphPresentation.Path, OAI.TorsionFreeZeroDivisors.ConcreteGroup.Γ, OAI.TorsionFreeZeroDivisors.ConcreteGroup.letter, OAI.TorsionFreeZeroDivisors.SampleGraph.label, OAI.TorsionFreeZeroDivisors.FinitePicture.Data, OAI.TorsionFreeZeroDivisors.Types.inverse