OAI/AlgebraicGeometry/CharacterVarieties/Seams/CutWords.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Ordered words for nonseparating surgery

Group identities describe the boundary words before and after a cut at a specified occurrence of the parent side.

  1. lemma OAI.IntegralCharacterVarieties.SurfaceSurgery.ofFn_reverse_prod_blocks line 16
  2. lemma OAI.IntegralCharacterVarieties.SurfaceSurgery.inverse_cut_ordered_word line 32

    Source documentation

    The group identity for inverse nonseparating surgery at an arbitrary position in the ordered surface word.

    lemma inverse_cut_ordered_word (H R1 R2 c t a : G) :
    (t⁻¹*H*t)*((t⁻¹*(t*a*t⁻¹*a⁻¹))*R1*(t⁻¹*(t*a*t⁻¹*a⁻¹))⁻¹)*a*
      ((t⁻¹*a⁻¹*c)*R2*(t⁻¹*a⁻¹*c)⁻¹)*(t⁻¹*a⁻¹*c*t) =
        t⁻¹*(H*(t*a*t⁻¹*a⁻¹)*R1*c*R2)*t := by group
…
  3. lemma OAI.IntegralCharacterVarieties.SurfaceSurgery.ofFn_take_congr line 41
  4. lemma OAI.IntegralCharacterVarieties.SurfaceSurgery.ofFn_drop_congr line 53
  5. lemma OAI.IntegralCharacterVarieties.SurfaceSurgery.list_split_at line 64
  6. lemma OAI.IntegralCharacterVarieties.SurfaceSurgery.ofFn_three_regions line 70
  7. lemma OAI.IntegralCharacterVarieties.SurfaceSurgery.ofFn_reverse_replace line 88
  8. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.rebaseUnit_index line 112
  9. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutReplacement line 117
  10. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutLongValue line 124
  11. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutLongValue_triple line 129
  12. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundaryEdge_eval_unit line 200
  13. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutBoundaryEdge_long line 209
  14. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutBoundaryWord_long line 228
  15. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutBoundaryEdge_short line 260
  16. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutBoundaryWord_short line 277
  17. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundaryPrefix line 304

    Source documentation

    The ordered prefix preceding a chosen boundary occurrence.

    def boundaryPrefix (f : F) (b : Fin (D.boundaryCount f)) (i : Fin (D.boundaryLength f b)) :=
…
  18. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundaryTail line 307
  19. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundaryWord_split line 310
  20. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCut_other_side line 321
  21. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCut_other_circle line 328
  22. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutChosenEdge line 335
  23. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutBoundaryWord_selected line 343
  24. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutBoundaryWord_other line 358