OAI/AlgebraicGeometry/CharacterVarieties/Seams/ProducedDiagram.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

A marked diagram from a field-valued solution

A solution of positive genus determines the band, marked diagram, punctures, frames, and generator values for a nonseparating cut.

  1. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.producedCutSeed line 26

    Source documentation

    The old generator coordinates after the necessary based-circle gauge.

    def producedCutSeed := D.bandCutLiftGenerators q (algebraMap R K) x.val.val b0
…
  2. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.producedCutJ line 29
  3. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.producedCutT line 32
  4. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.producedCutBand line 36
  5. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.producedMarkedDiagram line 39
  6. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.producedMarkedFrames line 44
  7. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.producedMarkedPunctures line 49
  8. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.producedMarkedValues line 54
  9. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.producedCutSeed_vertexHolds line 62
  10. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.ProducedMarkedVertexEquation line 68

    Source documentation

    The vertex equations of the produced marked diagram.

    def ProducedMarkedVertexEquation : Prop :=
…
  11. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.producedMarkedValues_vertexHolds line 72
  12. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.ProducedMarkedSurfaceEquation line 80

    Source documentation

    The surface equation of the produced marked diagram.

    def ProducedMarkedSurfaceEquation
    (f : D.ports.RefinedBandFacet q (D.producedCutBand q hg P x b0 i0).shape) : Prop :=
…
  13. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.producedMarkedValues_surface line 88
  14. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.namedSeam_of_seamHolds line 106
  15. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.producedCutSeed_namedSeam line 135
  16. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutMirror_rebase line 148