OAI/GroupTheory/ArtinCAT0/Presentation.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ArtinCAT0.lift_alternating_constant line 11
2. def OAI.ArtinCAT0.artinExponent line 18

   Source documentation

   Exponent sum, valid for every Artin matrix (including infinity labels).

   def artinExponent (M : S → S → Label) : ArtinGroup M →* Multiplicative ℤ :=
   …

   Mentions: OAI.ArtinCAT0.Label, OAI.ArtinCAT0.ArtinGroup

3. lemma OAI.ArtinCAT0.artinExponent_of line 23
4. lemma OAI.ArtinCAT0.artin_generator_infinite_order line 27
5. def OAI.ArtinCAT0.braidRelators line 37

   Source documentation

   Positive braid presentation on n generators, i.e. the group B_(n+1).

   def braidRelators (n : ℕ) : Set (FreeGroup (Fin n)) :=
   …

6. abbrev OAI.ArtinCAT0.BraidGroup line 44
7. def OAI.ArtinCAT0.braidGen line 46
8. lemma OAI.ArtinCAT0.braidGroup_relation line 49
9. lemma OAI.ArtinCAT0.braidGroup_commute line 56
10. lemma OAI.ArtinCAT0.braidGroup_relations line 63
11. def OAI.ArtinCAT0.braidLift line 68

    Source documentation

    Universal property, with equations rather than escaped relator words.

    def braidLift {n : ℕ} (s : Fin n → H)
        (hb : ∀ (i : ℕ) (hi : i+1 < n),
          s ⟨i, by omega⟩ * s ⟨i+1, hi⟩ * s ⟨i, by omega⟩ =
            s ⟨i+1, hi⟩ * s ⟨i, by omega⟩ * s ⟨i+1, hi⟩)
        (hc : ∀ i j : Fin n, i.val+2 ≤ j.val → Commute (s i) (s j)) : BraidGroup n →* H :=
    …

    Mentions: OAI.ArtinCAT0.BraidGroup

12. lemma OAI.ArtinCAT0.braidLift_of line 78
13. lemma OAI.ArtinCAT0.braidLift_gen line 81
14. def OAI.ArtinCAT0.braidTokenRepresentation line 86

    Source documentation

    Token representation. Unlike naive strand deletion, it is defined on every selected-position state, so respects arbitrary signed prefixes and suffixes.

    def braidTokenRepresentation (n : ℕ) : BraidGroup n →* Equiv.Perm (TokenState (BraidGroup 2)) :=
    …

    Mentions: OAI.ArtinCAT0.BraidGroup, OAI.ArtinCAT0.TokenState

15. def OAI.ArtinCAT0.initialSelected line 91
16. lemma OAI.ArtinCAT0.tokenPerm_initial line 93
17. lemma OAI.ArtinCAT0.braidTokenRepresentation_initial line 100
18. lemma OAI.ArtinCAT0.braidTokenRepresentation_two_injective line 119
19. def OAI.ArtinCAT0.initialBraidInclusion line 125

    Source documentation

    Initial B3 inclusion in every B_(n+1), for n≥2.

    def initialBraidInclusion (n : ℕ) (hn : 2 ≤ n) : BraidGroup 2 →* BraidGroup n :=
    …

    Mentions: OAI.ArtinCAT0.BraidGroup

20. lemma OAI.ArtinCAT0.initialBraidInclusion_injective line 130
21. def OAI.ArtinCAT0.triangleRelators line 145
22. abbrev OAI.ArtinCAT0.TriangleGroup line 150
23. def OAI.ArtinCAT0.triangleGen line 152
24. lemma OAI.ArtinCAT0.triangle_braid line 154
25. def OAI.ArtinCAT0.triangleLift line 160
26. lemma OAI.ArtinCAT0.triangleLift_gen line 167
27. def OAI.ArtinCAT0.trianglePair line 170
28. def OAI.ArtinCAT0.trianglePairRetraction line 178
29. lemma OAI.ArtinCAT0.trianglePair_leftInverse line 184
30. lemma OAI.ArtinCAT0.trianglePair_injective line 191
31. def OAI.ArtinCAT0.triangleExponent line 196
32. lemma OAI.ArtinCAT0.triangleExponent_gen line 199
33. lemma OAI.ArtinCAT0.triangle_generator_infinite_order line 202
34. def OAI.ArtinCAT0.triangleX line 209
35. def OAI.ArtinCAT0.triangleH line 213
36. lemma OAI.ArtinCAT0.triangular_relation line 215
37. lemma OAI.ArtinCAT0.triangleExponent_X line 227
38. lemma OAI.ArtinCAT0.triangleExponent_H line 231
39. abbrev OAI.ArtinCAT0.LinkDirection line 240

    Source documentation

    Signed edge directions in the nine-letter triangular presentation. Indices 0..8 are positive; indices 9..17 are negative.

    abbrev LinkDirection := Fin 18

40. def OAI.ArtinCAT0.linkNeighbors line 243

    Source documentation

    The three theta graphs, glued at a±, b±, c±, with cell identities retained.

    def linkNeighbors (d : LinkDirection) : Finset LinkDirection :=
    …

    Mentions: OAI.ArtinCAT0.LinkDirection

41. lemma OAI.ArtinCAT0.linkNeighbors_symm line 264
42. lemma OAI.ArtinCAT0.linkNeighbors_irrefl line 267
43. def OAI.ArtinCAT0.linkEnds line 270

    Source documentation

    Endpoints of nonbacktracking walks with a prescribed first oriented edge.

    def linkEnds : ℕ → LinkDirection → LinkDirection → Finset LinkDirection
      | 0, _, q => {q}
      | n+1, p, q => ((linkNeighbors q).erase p).biUnion (fun r => linkEnds n q r)

    Mentions: OAI.ArtinCAT0.LinkDirection, OAI.ArtinCAT0.linkNeighbors

44. lemma OAI.ArtinCAT0.link_girth0 line 274
45. lemma OAI.ArtinCAT0.link_girth1 line 275
46. lemma OAI.ArtinCAT0.link_girth2 line 276
47. lemma OAI.ArtinCAT0.link_girth3 line 277
48. lemma OAI.ArtinCAT0.link_girth4 line 278
49. lemma OAI.ArtinCAT0.link_girth line 280
50. lemma OAI.ArtinCAT0.mem_linkEnds_of_path line 289
51. lemma OAI.ArtinCAT0.link_closed_walk_length line 302

    Source documentation

    Every nonempty closed nonbacktracking walk in the exact link has at least six edges.

    lemma link_closed_walk_length (n : ℕ) (hn : 0 < n) (v : ℕ → LinkDirection)
        (hadj : ∀ i < n, v (i+1) ∈ linkNeighbors (v i))
        (hnob : ∀ i, i+2 ≤ n → v (i+2) ≠ v i) (hclosed : v n = v 0) : 6 ≤ n := by
    …

    Mentions: OAI.ArtinCAT0.LinkDirection, OAI.ArtinCAT0.linkNeighbors