OAI/AlgebraicGeometry/CharacterVarieties/Seams/MarkedSurface.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Surface equations for marked atomic surgery

The marked band boundary words and handle coordinates preserve every surface equation after the ordered boundary and handle gauges.

  1. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.surfaceTarget_eval_count_zero line 22
  2. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutOldSideValues_replacement line 28
  3. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundary_cycleWord_raw line 47
  4. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutBoundaryWord_cycle line 60
  5. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.fin_sum_comparison line 76
  6. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedGeneratorValues line 92

    Source documentation

    Invertible matrix values on the generators of a marked cut.

    def MarkedGeneratorValues : Type :=
…
  7. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedHandles line 102
  8. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedBandValues line 108
  9. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedBandWord_old line 115
  10. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedBandWord_mirror line 124
  11. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedBandWord_inl line 133
  12. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedBandSurface_inl line 157
  13. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedBandSurface_fresh line 169
  14. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedPunctures line 195
  15. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedLiftValues line 207
  16. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedLiftSurface_inl line 214
  17. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedLiftFreshSurface line 225

    Source documentation

    The surface equation on a fresh strip of a marked lift.

    def MarkedLiftFreshSurface (x : d.atomicBand.FreshStrip) : Prop :=
…
  18. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedLiftSurface_fresh line 229
  19. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedSolutionSurface line 244

    Source documentation

    Atomic surgery preserves every surface equation after the ordered boundary and handle gauges.

    lemma refinedMarkedSolutionSurface (f : D.ports.RefinedBandFacet q d) :
    let v := D.refinedMarkedLiftValues q d hp hc hc' hproper hmax (algebraMap R A)
…