OAI/AlgebraicTopology/Cubical/ArtinChains.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EilenbergGanea.TraceWords.CubeDescents.descentFinset line 14
  2. theorem OAI.EilenbergGanea.TraceWords.CubeDescents.mem_descentFinset line 18
  3. def OAI.EilenbergGanea.TraceWords.CubeDescents.leastDescent line 21
  4. theorem OAI.EilenbergGanea.TraceWords.CubeDescents.leastDescent_le line 25
  5. theorem OAI.EilenbergGanea.TraceWords.CubeDescents.leastDescent_mem line 31
  6. def OAI.EilenbergGanea.TraceWords.CubeDescents.artinDescentSystem line 43

    Source documentation

    The actual RAAG satisfies every hypothesis of the descending-chain contraction, as a consequence of the independently proved trace normal form.

    def artinDescentSystem : DescentSystem (fun x => letterValue (artinGenerator L) (invLetter x)) where
…

    Mentions: OAI.EilenbergGanea.TraceWords.letterValue, OAI.EilenbergGanea.artinGenerator, OAI.EilenbergGanea.TraceWords.invLetter

  7. def OAI.EilenbergGanea.TraceWords.CubeDescents.descendingChains line 60
  8. theorem OAI.EilenbergGanea.TraceWords.CubeDescents.descending_finite_bound line 63
  9. theorem OAI.EilenbergGanea.TraceWords.CubeDescents.descending_cycle_bounds line 75

    Source documentation

    Exactness of the genuine descending cubical chain complex in every positive degree, with no finite-support bound imposed on the cycle.

    theorem descending_cycle_bounds {k : ℕ} (hk : 0 < k)
    (c : Chains (ArtinGroup L) (Letter V)) (hc : c ∈ descendingChains L k)
    (hz : boundary (fun x => letterValue (artinGenerator L) (invLetter x)) c = 0) :
    ∃ b ∈ descendingChains L (k+1),
      boundary (fun x => letterValue (artinGenerator L) (invLetter x)) b = c := by
…

    Mentions: OAI.EilenbergGanea.TraceWords.Letter, OAI.EilenbergGanea.TraceWords.CubeDescents.descendingChains, OAI.EilenbergGanea.TraceWords.letterValue, OAI.EilenbergGanea.artinGenerator, OAI.EilenbergGanea.TraceWords.invLetter

  10. abbrev OAI.CubicalChains.Reorientation.Signed line 94
  11. def OAI.CubicalChains.Reorientation.step line 96
  12. def OAI.CubicalChains.Reorientation.origin line 98
  13. def OAI.CubicalChains.Reorientation.sign line 102
  14. theorem OAI.CubicalChains.Reorientation.origin_nil line 106
  15. theorem OAI.CubicalChains.Reorientation.sign_nil line 107
  16. theorem OAI.CubicalChains.Reorientation.sign_sq line 109
  17. theorem OAI.CubicalChains.Reorientation.origin_shift line 114
  18. def OAI.CubicalChains.Reorientation.normalTerm line 127
  19. def OAI.CubicalChains.Reorientation.normalize line 130
  20. theorem OAI.CubicalChains.Reorientation.normalize_single line 133
  21. theorem OAI.CubicalChains.Reorientation.normalize_front line 136
  22. theorem OAI.CubicalChains.Reorientation.normalize_boundaryTerm line 154

    Source documentation

    Reversing selected coordinates changes the signs and origin but not the actual integral cubical boundary. No asphericity input is used here.

    theorem normalize_boundaryTerm (g : G) (w : List (Signed V))
    (hw : w.Pairwise (fun x y => Commute (f x.1) (f y.1))) :
    normalize f (boundaryTerm (step f) g w) = boundary f (normalTerm f g w) := by
…

    Mentions: OAI.CubicalChains.Reorientation.Signed, OAI.CubicalChains.Reorientation.normalize, OAI.CubicalChains.boundaryTerm, OAI.CubicalChains.Reorientation.step, OAI.CubicalChains.boundary, OAI.CubicalChains.Reorientation.normalTerm

  23. theorem OAI.EilenbergGanea.TraceWords.CubeDescents.reverse_step_descent line 196
  24. theorem OAI.EilenbergGanea.TraceWords.CubeDescents.origin_descent_invariant line 208
  25. def OAI.EilenbergGanea.TraceWords.CubeDescents.orient line 222

    Source documentation

    Orient a positive cube toward its unique word-length maximum.

    def orient (g : ArtinGroup L) : List V → ArtinGroup L × Word V
  | [] => (g,[])
  | q::w => if (q,false) ∈ rightDescents L g then
      let t := orient g w
…

    Mentions: OAI.EilenbergGanea.TraceWords.Word, OAI.EilenbergGanea.TraceWords.rightDescents

  26. theorem OAI.EilenbergGanea.TraceWords.CubeDescents.orient_nil line 231
  27. theorem OAI.EilenbergGanea.TraceWords.CubeDescents.orient_map line 233
  28. theorem OAI.EilenbergGanea.TraceWords.CubeDescents.orient_descent_invariant line 239
  29. theorem OAI.EilenbergGanea.TraceWords.CubeDescents.orient_descents line 252
  30. theorem OAI.EilenbergGanea.TraceWords.CubeDescents.origin_orient line 274
  31. theorem OAI.EilenbergGanea.TraceWords.CubeDescents.orient_origin line 295

    Source documentation

    Reorientation is invertible on every actual descending cube.

    theorem orient_origin (g : ArtinGroup L) (w : Word V)
    (hw : w.Pairwise (Independent L)) (hd : ∀ x ∈ w, x ∈ rightDescents L g) :
    orient L (origin (artinGenerator L) g w) (w.map Prod.fst) = (g,w) := by
…

    Mentions: OAI.EilenbergGanea.TraceWords.Word, OAI.EilenbergGanea.TraceWords.Independent, OAI.EilenbergGanea.TraceWords.rightDescents, OAI.EilenbergGanea.TraceWords.CubeDescents.orient, OAI.EilenbergGanea.artinGenerator

  32. def OAI.EilenbergGanea.TraceWords.CubeDescents.positiveChains line 332
  33. theorem OAI.EilenbergGanea.TraceWords.CubeDescents.descending_independent line 335
  34. theorem OAI.EilenbergGanea.TraceWords.CubeDescents.signed_sorted_iff line 342
  35. theorem OAI.EilenbergGanea.TraceWords.CubeDescents.normalize_descending line 355
  36. def OAI.EilenbergGanea.TraceWords.CubeDescents.denormalTerm line 366
  37. def OAI.EilenbergGanea.TraceWords.CubeDescents.denormalize line 369
  38. theorem OAI.EilenbergGanea.TraceWords.CubeDescents.denormalize_single line 373
  39. theorem OAI.EilenbergGanea.TraceWords.CubeDescents.denormalize_positive line 377
  40. theorem OAI.EilenbergGanea.TraceWords.CubeDescents.normal_denormal_term line 395
  41. theorem OAI.EilenbergGanea.TraceWords.CubeDescents.denormal_normal_term line 405
  42. theorem OAI.EilenbergGanea.TraceWords.CubeDescents.normal_denormal line 413
  43. theorem OAI.EilenbergGanea.TraceWords.CubeDescents.denormal_normal line 424
  44. theorem OAI.EilenbergGanea.TraceWords.CubeDescents.step_eq_inverse_letter line 436
  45. theorem OAI.EilenbergGanea.TraceWords.CubeDescents.descending_boundary line 441
  46. theorem OAI.EilenbergGanea.TraceWords.CubeDescents.normalize_boundary line 451
  47. theorem OAI.EilenbergGanea.TraceWords.CubeDescents.positive_cycle_bounds line 469

    Source documentation

    Exactness of the standard positively oriented RAAG cube chains. This is an actual finite integral filling, derived from the descending contraction.

    theorem positive_cycle_bounds {k : ℕ} (hk : 0 < k)
    (c : Chains (ArtinGroup L) V) (hc : c ∈ positiveChains L k)
    (hz : boundary (artinGenerator L) c = 0) :
    ∃ b ∈ positiveChains L (k+1), boundary (artinGenerator L) b = c := by
…

    Mentions: OAI.EilenbergGanea.TraceWords.CubeDescents.positiveChains, OAI.EilenbergGanea.artinGenerator