OAI/Algebra/GroupRing/WordBlocks.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.TorsionFreeZeroDivisors.WordBlocks.lengths line 12
  2. abbrev OAI.TorsionFreeZeroDivisors.WordBlocks.Occ line 13
  3. lemma OAI.TorsionFreeZeroDivisors.WordBlocks.total_length line 14
  4. def OAI.TorsionFreeZeroDivisors.WordBlocks.coordinates line 18
  5. def OAI.TorsionFreeZeroDivisors.WordBlocks.letter line 20
  6. lemma OAI.TorsionFreeZeroDivisors.WordBlocks.coordinates_inl line 23
  7. lemma OAI.TorsionFreeZeroDivisors.WordBlocks.coordinates_inr line 25
  8. lemma OAI.TorsionFreeZeroDivisors.WordBlocks.letter_eq line 27
  9. lemma OAI.TorsionFreeZeroDivisors.WordBlocks.finRotate_congr line 43
  10. lemma OAI.TorsionFreeZeroDivisors.WordBlocks.full_eq line 45
  11. structure OAI.TorsionFreeZeroDivisors.WordBlocks.Matching line 54

    Source documentation

    A full inverse-letter matching on the separate literal word boundaries, with actual combinatorial genus zero. This is not a PL-picture assertion.

    structure Matching (inv : A→A) (ws : List (List A)) where
…
  12. def OAI.TorsionFreeZeroDivisors.WordBlocks.ofDisk line 61
  13. theorem OAI.TorsionFreeZeroDivisors.WordBlocks.of_identity line 76

    Source documentation

    The literal free identity has a planar matching on its blocks, even if some of the blocks are empty. No nonempty-relator premise is added.

    theorem of_identity {B : Type*} (ws : List (List (B×Bool)))
    (h : FreeGroup.mk ws.flatten=1) : Nonempty (Matching WordPairing.inverseLetter ws) := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.WordBlocks.Matching, OAI.TorsionFreeZeroDivisors.WordPairing.inverseLetter

  14. def OAI.TorsionFreeZeroDivisors.AlgebraicPictures.blockWords line 85
  15. lemma OAI.TorsionFreeZeroDivisors.AlgebraicPictures.blockWords_flatten line 87
  16. theorem OAI.TorsionFreeZeroDivisors.AlgebraicPictures.quotient_block_matching line 93

    Source documentation

    The algebraic null word yields a literal genus-zero matching after separating the outer word and every conjugated relator into distinct cyclic boundaries. Conjugator suppression and graph lifts are not assumed here.

    theorem quotient_block_matching (h : PresentedGroup.mk (relations rel) (mk outer)=1) :
    ∃ts : List (Term (A:=A) (I:=I)),
…

    Mentions: OAI.TorsionFreeZeroDivisors.AlgebraicPictures.relations, OAI.TorsionFreeZeroDivisors.AlgebraicPictures.Term

  17. abbrev OAI.TorsionFreeZeroDivisors.CyclicCaps.O line 105
  18. abbrev OAI.TorsionFreeZeroDivisors.CyclicCaps.p line 106
  19. abbrev OAI.TorsionFreeZeroDivisors.CyclicCaps.q line 107
  20. lemma OAI.TorsionFreeZeroDivisors.CyclicCaps.distinct line 108
  21. def OAI.TorsionFreeZeroDivisors.CyclicCaps.raise line 113
  22. def OAI.TorsionFreeZeroDivisors.CyclicCaps.embed line 114
  23. lemma OAI.TorsionFreeZeroDivisors.CyclicCaps.embed_injective line 124
  24. lemma OAI.TorsionFreeZeroDivisors.CyclicCaps.embed_surjective line 135
  25. def OAI.TorsionFreeZeroDivisors.CyclicCaps.coordinates line 149
  26. def OAI.TorsionFreeZeroDivisors.CyclicCaps.rotation line 152
  27. lemma OAI.TorsionFreeZeroDivisors.CyclicCaps.next line 153
  28. lemma OAI.TorsionFreeZeroDivisors.CyclicCaps.rotation_commutes line 154
  29. lemma OAI.TorsionFreeZeroDivisors.CyclicCaps.rotation_conjugate line 197
  30. def OAI.TorsionFreeZeroDivisors.CyclicCaps.partner line 207
  31. lemma OAI.TorsionFreeZeroDivisors.CyclicCaps.involutive line 210
  32. lemma OAI.TorsionFreeZeroDivisors.CyclicCaps.fixed_free line 213
  33. theorem OAI.TorsionFreeZeroDivisors.CyclicCaps.genusZero line 217

    Source documentation

    Removing the two literal end letters of a cyclic block preserves genus zero with the forced matching splice. The enclosed block may be empty.

    theorem genusZero (hz : MapEuler.GenusZero (rotation n ρ) α) :
    MapEuler.GenusZero (Equiv.sumCongr (finRotate n) ρ) (partner n α hi hf) := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.GenusZero, OAI.TorsionFreeZeroDivisors.CyclicCaps.rotation, OAI.TorsionFreeZeroDivisors.CyclicCaps.partner

  34. lemma OAI.TorsionFreeZeroDivisors.CyclicCaps.compatible line 235
  35. def OAI.TorsionFreeZeroDivisors.WordBlocks.Matching.rename line 250
  36. def OAI.TorsionFreeZeroDivisors.WordBlocks.exchange line 270
  37. lemma OAI.TorsionFreeZeroDivisors.WordBlocks.exchange_rotation line 281
  38. lemma OAI.TorsionFreeZeroDivisors.WordBlocks.exchange_letter line 286
  39. def OAI.TorsionFreeZeroDivisors.WordBlocks.focus line 290

    Source documentation

    Expose any literal word block while retaining all other blocks, in order.

    def focus (pre : List (List A)) (w : List A) (suffix : List (List A)) :
    Occ (pre++w::suffix)≃Occ (w::(pre++suffix)) := match pre with
…

    Mentions: OAI.TorsionFreeZeroDivisors.WordBlocks.Occ

  40. lemma OAI.TorsionFreeZeroDivisors.WordBlocks.focus_letter line 294
  41. lemma OAI.TorsionFreeZeroDivisors.WordBlocks.focus_rotation line 307
  42. def OAI.TorsionFreeZeroDivisors.WordBlocks.Matching.focus line 325
  43. def OAI.TorsionFreeZeroDivisors.WordBlocks.Matching.unfocus line 327
  44. def OAI.TorsionFreeZeroDivisors.WordBlocks.capCoordinates line 338
  45. lemma OAI.TorsionFreeZeroDivisors.WordBlocks.capRotation line 340
  46. abbrev OAI.TorsionFreeZeroDivisors.WordBlocks.capLabel line 351
  47. lemma OAI.TorsionFreeZeroDivisors.WordBlocks.capLabel_q line 353
  48. lemma OAI.TorsionFreeZeroDivisors.WordBlocks.capLabel_p line 354
  49. lemma OAI.TorsionFreeZeroDivisors.WordBlocks.capLabel_embed line 357
  50. def OAI.TorsionFreeZeroDivisors.WordBlocks.Matching.removeCaps line 366

    Source documentation

    Tighten inverse end caps of one literal word boundary. The matching is spliced, and its genuine genus zero remains valid even for an empty interior.

    def Matching.removeCaps (d : Matching inv ((a::(w++[inv a]))::ws)) : Matching inv (w::ws) := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.WordBlocks.Matching