OAI/AlgebraicGeometry/CharacterVarieties/Seams/InverseSolution.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Solutions under inverse nonseparating surgery

The boundary and handle identities preserve the surface relations. Together with the seam and vertex equations they define a solution over the coefficient algebra.

  1. abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutU line 24
  2. abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutV line 25
  3. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutLiftGauge line 27
  4. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutLiftGenerators line 30
  5. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutLiftValues line 32
  6. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutLiftGauge_selected line 38
  7. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutLiftGenerators_selected line 43
  8. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutLiftBoundary_selected line 52
  9. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutLiftBoundary_short line 57
  10. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutLiftBoundary_parent line 63
  11. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutLiftBoundary_other line 81
  12. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutEarlier line 111

    Source documentation

    The two ordered products on either side of the selected old circle.

    def bandCutEarlier : D.FacetUnit (A:=A) (D.bandCutParent q) :=
…
  13. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutLater line 114
  14. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutOldBoundaryProduct_parent line 117
  15. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutBoundaryProduct_split line 127
  16. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutBoundaryProduct_long_parent line 143
  17. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutBoundaryProduct_parent line 162
  18. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutBoundaryProduct_other line 178
  19. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.surfaceWord_eval_raw line 202
  20. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutLiftHandleProduct_parent line 208
  21. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutLiftHandleProduct_other line 215
  22. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutLiftSurfaceRaw_parent line 226
  23. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutLiftSurface_other line 246
  24. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutLiftSurface_parent line 256
  25. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.sameFramedFlag_unit_self line 279
  26. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCut_seamHolds line 283
  27. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCut_vertexHolds line 301
  28. abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutHandleT line 326
  29. abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutHandleA line 328
  30. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutSolutionValues line 331
  31. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutSolutionSurface line 335
  32. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutSolutionAt line 352

    Source documentation

    Lift a solution over the coefficient algebra at a chosen parent occurrence.

    def bandCutSolutionAt : (D.bandCutDiagram q).Solution (D.bandCutPunctures q P) A := by
…

    Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.Solution

  33. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.inverseBandSolution line 379

    Source documentation

    Choose an inverse nonseparating arc and preserve all vertex, boundary, and surface equations over the coefficient algebra.

    def inverseBandSolution : (D.bandCutDiagram q).Solution (D.bandCutPunctures q P) A := by
…

    Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.Solution