CubeDescents.lean`

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Right descents and the cubes in the actual Artin Cayley graph.

theorem OAI.EilenbergGanea.TraceWords.Equivalent.extract line 18
theorem OAI.EilenbergGanea.TraceWords.Swap.reverse line 31
theorem OAI.EilenbergGanea.TraceWords.Equivalent.reverse line 40
theorem OAI.EilenbergGanea.TraceWords.Extract.eq_or_independent line 50
Source documentation
Distinct accessible occurrences commute. In particular two opposite signs of the same vertex can never both be accessible.
```
theorem Extract.eq_or_independent {x y : Letter V} {w u v : Word V}
    (hx : Extract L x w u) (hy : Extract L y w v) :
    x = y ∨ Independent L x y := by
…
```
Mentions: OAI.EilenbergGanea.TraceWords.Letter, OAI.EilenbergGanea.TraceWords.Word, OAI.EilenbergGanea.TraceWords.Extract, OAI.EilenbergGanea.TraceWords.Independent
def OAI.EilenbergGanea.TraceWords.RightExtract line 64
theorem OAI.EilenbergGanea.TraceWords.RightExtract.equivalent line 68
theorem OAI.EilenbergGanea.TraceWords.RightExtract.of_equivalent line 72
theorem OAI.EilenbergGanea.TraceWords.RightExtract.length line 79
theorem OAI.EilenbergGanea.TraceWords.RightExtract.eq_or_independent line 83
theorem OAI.EilenbergGanea.TraceWords.RightExtract.diamond line 87
def OAI.EilenbergGanea.TraceWords.EndsWith line 96
Source documentation
A maximal occurrence of a trace, retaining its sign.
```
def EndsWith (t : Trace L) (x : Letter V) : Prop :=
…
```
Mentions: OAI.EilenbergGanea.TraceWords.Trace, OAI.EilenbergGanea.TraceWords.Letter
def OAI.EilenbergGanea.TraceWords.artinLength line 99
def OAI.EilenbergGanea.TraceWords.rightDescents line 101
theorem OAI.EilenbergGanea.TraceWords.endsWith_ofWord_iff line 105
theorem OAI.EilenbergGanea.TraceWords.endsWith_append_independent line 116
theorem OAI.EilenbergGanea.TraceWords.artinLength_word line 137
theorem OAI.EilenbergGanea.TraceWords.rightDescents_word line 141
theorem OAI.EilenbergGanea.TraceWords.rightDescents_pairwise line 147
Source documentation
The whole descending link is a clique, not just its pairwise choices.
```
theorem rightDescents_pairwise (g : ArtinGroup L) :
    (rightDescents L g).Pairwise (Independent L) := by
…
```
Mentions: OAI.EilenbergGanea.TraceWords.rightDescents, OAI.EilenbergGanea.TraceWords.Independent
theorem OAI.EilenbergGanea.TraceWords.rightDescents_length line 155
theorem OAI.EilenbergGanea.TraceWords.descent_independent_step line 180
Source documentation
Crossing one cube direction does not change the descent status of any independent direction. This is the no-local-maximum obstruction needed for the length filtration of the universal cubical complex.
```
theorem descent_independent_step (g : ArtinGroup L) {x y : Letter V}
    (hxy : Independent L x y) :
    y ∈ rightDescents L (g * letterValue (artinGenerator L) x) ↔ y ∈ rightDescents L g := by
…
```
Mentions: OAI.EilenbergGanea.TraceWords.Letter, OAI.EilenbergGanea.TraceWords.Independent, OAI.EilenbergGanea.TraceWords.rightDescents, OAI.EilenbergGanea.TraceWords.letterValue, OAI.EilenbergGanea.artinGenerator
theorem OAI.EilenbergGanea.TraceWords.artinLength_eq_zero_iff line 188
theorem OAI.EilenbergGanea.TraceWords.rightDescents_nonempty line 206
theorem OAI.EilenbergGanea.TraceWords.artinLength_step line 220
Source documentation
The exact length increment of one generator, with no chosen normal word.
```
theorem artinLength_step (g : ArtinGroup L) (x : Letter V) :
    (artinLength L (g * letterValue (artinGenerator L) x) : ℤ) =
      artinLength L g + if invLetter x ∈ rightDescents L g then -1 else 1 := by
…
```
Mentions: OAI.EilenbergGanea.TraceWords.Letter, OAI.EilenbergGanea.TraceWords.artinLength, OAI.EilenbergGanea.TraceWords.letterValue, OAI.EilenbergGanea.artinGenerator, OAI.EilenbergGanea.TraceWords.invLetter, OAI.EilenbergGanea.TraceWords.rightDescents
theorem OAI.EilenbergGanea.TraceWords.descent_word_invariant line 236
theorem OAI.EilenbergGanea.TraceWords.artinLength_clique_word line 247
Source documentation
On a cube, length is affine: every coordinate has increment +1 or -1, and independent crossings cannot change that increment.
```
theorem artinLength_clique_word (g : ArtinGroup L) (w : Word V)
    (hw : w.Pairwise (Independent L)) :
    (artinLength L (g * wordEval (artinGenerator L) w) : ℤ) = artinLength L g +
      (w.map fun x => if invLetter x ∈ rightDescents L g then (-1 : ℤ) else 1).sum := by
…
```
Mentions: OAI.EilenbergGanea.TraceWords.Word, OAI.EilenbergGanea.TraceWords.Independent, OAI.EilenbergGanea.TraceWords.artinLength, OAI.EilenbergGanea.TraceWords.wordEval, OAI.EilenbergGanea.artinGenerator, OAI.EilenbergGanea.TraceWords.invLetter, OAI.EilenbergGanea.TraceWords.rightDescents
theorem OAI.EilenbergGanea.TraceWords.artinLength_descending_cube line 268
Source documentation
Every face of the full descending cube has precisely the expected length. This proves in particular that its corners are different from its top.
```
theorem artinLength_descending_cube (g : ArtinGroup L) (w : Word V)
    (hw : w.Pairwise (Independent L)) (hd : ∀ x ∈ w, x ∈ rightDescents L g) :
    artinLength L (g * wordEval (artinGenerator L) (w.map invLetter)) + w.length =
      artinLength L g := by
…
```
Mentions: OAI.EilenbergGanea.TraceWords.Word, OAI.EilenbergGanea.TraceWords.Independent, OAI.EilenbergGanea.TraceWords.rightDescents, OAI.EilenbergGanea.TraceWords.artinLength, OAI.EilenbergGanea.TraceWords.wordEval, OAI.EilenbergGanea.artinGenerator, OAI.EilenbergGanea.TraceWords.invLetter