OAI/GroupTheory/ArtinCAT0/Refinement.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ArtinCAT0.WordDiagram.Side line 8
  2. def OAI.ArtinCAT0.WordDiagram.inverseWord line 10
  3. def OAI.ArtinCAT0.WordDiagram.sideWord line 11
  4. def OAI.ArtinCAT0.WordDiagram.sideFlip line 12
  5. def OAI.ArtinCAT0.WordDiagram.sideFull line 13
  6. lemma OAI.ArtinCAT0.WordDiagram.eval_inverseWord line 16
  7. lemma OAI.ArtinCAT0.WordDiagram.eval_sideFlip line 19
  8. lemma OAI.ArtinCAT0.WordDiagram.sideFull_reverse line 23
  9. lemma OAI.ArtinCAT0.WordDiagram.sideFull_length line 28
  10. lemma OAI.ArtinCAT0.WordDiagram.sideFull_contract line 33
  11. lemma OAI.ArtinCAT0.WordDiagram.fullSide_head line 41
  12. lemma OAI.ArtinCAT0.WordDiagram.fullSide_last line 44
  13. lemma OAI.ArtinCAT0.WordDiagram.sideFull_head line 49
  14. lemma OAI.ArtinCAT0.WordDiagram.sideFull_last line 54
  15. def OAI.ArtinCAT0.WordDiagram.startLabel line 59
  16. def OAI.ArtinCAT0.WordDiagram.closedSides line 63
  17. lemma OAI.ArtinCAT0.WordDiagram.startLabel_next line 66
  18. def OAI.ArtinCAT0.WordDiagram.sideBoundary line 71
  19. lemma OAI.ArtinCAT0.WordDiagram.sideBoundary_contract line 76
  20. lemma OAI.ArtinCAT0.WordDiagram.sideBoundary_length line 94
  21. lemma OAI.ArtinCAT0.WordDiagram.path_grid_pos line 99
  22. theorem OAI.ArtinCAT0.WordDiagram.finite_template_fillers line 112

    Source documentation

    A finite collection of triangular loop types admits one common boundary width and one common disk height. The boundary parametrizations reverse literally, rather than merely up to homotopy.

    theorem finite_template_fillers {I : Type*} [Fintype I] (s : I → Fin 3 → Side)
    (hs : ∀ i, closedSides (s i)) :
    ∃ K H : ℕ, ∃ hK : 0 < K, letI : NeZero (3*K) := ⟨by omega⟩;
…

    Mentions: OAI.ArtinCAT0.WordDiagram.Side, OAI.ArtinCAT0.WordDiagram.closedSides

  23. lemma OAI.ArtinCAT0.WordDiagram.getD_dropLast line 154
  24. lemma OAI.ArtinCAT0.WordDiagram.sideBoundary_get_interior line 159
  25. lemma OAI.ArtinCAT0.WordDiagram.sideBoundary_get line 185
  26. lemma OAI.ArtinCAT0.WordDiagram.walk_translate line 226
  27. lemma OAI.ArtinCAT0.WordDiagram.fullSide_translate line 232
  28. lemma OAI.ArtinCAT0.WordDiagram.sideFull_translate line 236
  29. lemma OAI.ArtinCAT0.WordDiagram.sideFull_getTranslate line 241
  30. lemma OAI.ArtinCAT0.WordDiagram.sideFull_getReverse line 249
  31. lemma OAI.ArtinCAT0.WordDiagram.TargetLegal_translate line 264
  32. lemma OAI.ArtinCAT0.WordDiagram.template_seam line 286
  33. def OAI.ArtinCAT0.WordDiagram.refinedLabels line 302
  34. lemma OAI.ArtinCAT0.WordDiagram.refinedLabels_tail line 309
  35. lemma OAI.ArtinCAT0.WordDiagram.refinedLabels_legal line 314
  36. lemma OAI.ArtinCAT0.mirrorLinear_one line 328
  37. lemma OAI.ArtinCAT0.mirrorLinear_inv line 329
  38. lemma OAI.ArtinCAT0.mirrorLinear_zpow line 331
  39. lemma OAI.ArtinCAT0.mirrorVector_pure_mul line 335
  40. lemma OAI.ArtinCAT0.mirrorVector_pure_pow line 341
  41. lemma OAI.ArtinCAT0.mirrorVector_pure_zpow line 350
  42. def OAI.ArtinCAT0.mirrorPlane line 364
  43. lemma OAI.ArtinCAT0.mirrorPlane_one line 368
  44. lemma OAI.ArtinCAT0.mirrorPlane_pure_mul line 370
  45. lemma OAI.ArtinCAT0.mirrorPlane_pure_zpow line 375
  46. lemma OAI.ArtinCAT0.mirrorPlane_mul_bound line 379
  47. def OAI.ArtinCAT0.SixSector.planeRay line 401
  48. lemma OAI.ArtinCAT0.SixSector.ray_rep_even line 404
  49. lemma OAI.ArtinCAT0.SixSector.ray_rep_odd line 409
  50. lemma OAI.ArtinCAT0.SixSector.ray_pure line 416
  51. lemma OAI.ArtinCAT0.SixSector.ray_plane line 429
  52. lemma OAI.ArtinCAT0.SixSector.lattice_plane line 443