OAI/AlgebraicGeometry/CharacterVarieties/Seams/Handles.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Handles and boundary gauges for a cut

The retained handle coordinates and boundary gauges determine the new transport values for inverse nonseparating surgery.

  1. abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.FacetUnit line 19
  2. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutHandleIndex line 22

    Source documentation

    Retain the old handle slots after deleting the last handle on the chosen parent.

    def bandCutHandleIndex (f : F) (k : Fin ((D.bandCutDiagram q).genus f)) : Fin (D.genus f) :=
…
  3. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutHandleBase line 28
  4. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutRetainedHandles line 31
  5. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutCircleBases line 38

    Source documentation

    Boundary gauges determined by the old boundary order.

    def bandCutCircleBases (b0 : Fin (D.boundaryCount (D.bandCutParent q)))
    (U V : D.FacetUnit (A:=A) (D.bandCutParent q)) : D.CircleBases (R:=A) := fun B =>
…
  6. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutChosenJ line 54

    Source documentation

    The transport along the new seam with an identity child.

    def bandCutChosenJ : D.BandCutUnit (A:=A) q :=
…
  7. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutChosenT line 58
  8. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutChosen_long line 77
  9. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutChosen_short line 88
  10. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutCircleBases_parent line 107
  11. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutCircleBases_other line 114
  12. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutRetainedProduct line 133

    Source documentation

    The ordered product of the retained handle commutators.

    def bandCutRetainedProduct (f : F) : D.FacetUnit (A:=A) f :=
…
  13. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutCommutator_eval line 136
  14. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutHandleProduct_eval line 149
  15. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutHandleBase_parent line 159
  16. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutHandleBase_other line 162
  17. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutLastHandle line 169
  18. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutOldHandleProduct_parent line 174
  19. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutOldHandleProduct_other line 182