OAI/AlgebraicGeometry/CharacterVarieties/Frames/ShortCoordinates.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.sigmaFin_ext_val line 9
  2. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.sigmaFinCongr_val line 13
  3. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.sigmaFinCongr_symm_val line 16
  4. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.sigmaFinRefl_symm_val line 22
  5. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.transportFrames_frameCoordinates line 28
  6. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutFirstOldColumns line 49
  7. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutFirstOldRows line 52
  8. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutFirstOldActualColumns line 58
  9. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutFirstOldActualRows line 59
  10. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutFirstNewActualColumns line 60
  11. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutFirstNewActualRows line 61
  12. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.CutColumnCoordinatesAligned line 63

    Source documentation

    Column coordinates at two ports are compatible with transport across the cut seam.

    def CutColumnCoordinatesAligned {I : Type}
    (p u : LocalPort _ (C).ports.kind) (h : D.CutPortsAdjacent q w p u)
    (e : I ≃ ((C).vertexRanks p.1).Columns p.2)
    (eu : I ≃ ((C).vertexRanks u.1).Columns u.2) : Prop :=
…

    Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.vertexRanks

  13. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.FirstCutColumnsCompatible line 70

    Source documentation

    Compatibility of column coordinates at the negative endpoint of the cut band.

    def FirstCutColumnsCompatible : Prop :=
…
  14. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutFirstColumn_match line 75
  15. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.FirstCutRowsCompatible line 110

    Source documentation

    Compatibility of row coordinates at the negative endpoint of the cut band.

    def FirstCutRowsCompatible : Prop :=
…
  16. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutFirstRow_match line 115
  17. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.lastAdjacentSame line 137
  18. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutLastChild line 145
  19. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutLastChild_enumeration line 152
  20. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.lastCutChildTransport line 161

    Source documentation

    Child transport from the old positive end to the last vertex of the cut band.

    def lastCutChildTransport :
    (D.ports.kind (oo).1).table.Child (oo).2 ≃
      (w.shape.atomicBand.kind (Fin.last w.shape.atomicBand.length)).table.Child
        (w.shape.atomicBand.kind (Fin.last w.shape.atomicBand.length)).output :=
…
  21. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.lastChildMatch line 170
  22. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutLastOldColumns line 193
  23. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutLastOldRows line 196
  24. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutLastOldActualColumns line 202
  25. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutLastOldActualRows line 203
  26. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutLastNewActualColumns line 204
  27. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutLastNewActualRows line 205
  28. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.LastCutColumnsCompatible line 207

    Source documentation

    Compatibility of column coordinates at the positive endpoint of the cut band.

    def LastCutColumnsCompatible : Prop :=
…
  29. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutLastColumn_match line 213
  30. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.LastCutRowsCompatible line 249

    Source documentation

    Compatibility of row coordinates at the positive endpoint of the cut band.

    def LastCutRowsCompatible : Prop :=
…
  31. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutLastRow_match line 254
  32. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.LastCutOldFrameCompatible line 284

    Source documentation

    The old positive frame retains its named seam coordinates after the cut.

    def LastCutOldFrameCompatible : Prop :=
…
  33. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.LastCutNewFrameCompatible line 290

    Source documentation

    The new positive frame has the terminal coordinates of the identified band.

    def LastCutNewFrameCompatible : Prop :=
…
  34. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutLast_old_frameCoordinates line 294
  35. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutLast_new_frameCoordinates line 303
  36. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.LastCutColumnHasGrade line 310

    Source documentation

    A positive endpoint column has the grade of its original child coordinate.

    def LastCutColumnHasGrade (i : (i : Fin (arity q)) × Fin (D.childDim q i)) : Prop :=
…
  37. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutLast_grade line 314
  38. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.oldSignatureMatch line 341
  39. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.oldPlusSignature line 346
  40. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.oldMinusSignature line 354
  41. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutOldSeam line 365
  42. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutOldSeam_arity line 367
  43. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutOldSideRank line 371
  44. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCutOldSideValues line 381

    Source documentation

    Side values of the cut diagram expressed in the original seam ranks.

    def refinedCutOldSideValues : D.SideValues (R:=R) :=
…
  45. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCutSideValues_old line 386
  46. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCutSideValues_last_parent line 393
  47. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCutSideValues_old_child line 398
  48. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCutSideValues_unchanged_parent line 403