OAI/AlgebraicGeometry/CharacterVarieties/Seams/ProducedEquations.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Framed seam equations on the produced marked diagram

The complete seam equations and the first short-seam equation use the marked diagram and generator values determined by a field-valued solution.

  1. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.ProducedMarkedSeamEquations line 25

    Source documentation

    The framed flag equations at every produced marked seam.

    def ProducedMarkedSeamEquations : Prop :=
…
  2. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.ProducedMarkedFirstShortEquation line 33

    Source documentation

    The framed flag equation at the first produced short seam.

    def ProducedMarkedFirstShortEquation : Prop :=
…