ProducedSolution.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

A solution on the produced marked diagram

Every seam of the produced marked diagram satisfies its framed flag equation. The surface, seam, and vertex equations assemble a field-valued solution.

lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.framedSeamEquations_of_values_eq line 18

Source documentation

Equal generator values satisfy the same framed seam equations.

lemma framedSeamEquations_of_values_eq
    {F S V R K : Type} {arity : S → ℕ} [CommRing R] [Field K]
    (C : Diagram F S V arity) (φ : R →+* K)
    {v v' : (e : C.Generator) →
      (Matrix (Fin (C.generatorRank e)) (Fin (C.generatorRank e)) K)ˣ}
    (h : v = v')
    (hseam : ∀ s, FramedSeamEquation (D:=C) (g:=v) (φ:=φ) s) :
…

Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram, OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.FramedSeamEquation

theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.producedMarkedValues_allSeams line 37
Distinct definitions of this name: ComparatorChallenges/CharacterVarietiesAllSeamsSupport.lean:17 (same statement text; different proof or body). Qualify references as OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.producedMarkedValues_allSeams@path.
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.producedMarkedValues_firstShort line 95
Source documentation
The first short seam of the produced marked diagram.
```
lemma producedMarkedValues_firstShort :
    D.ProducedMarkedFirstShortEquation q hproper hmax hg P x b0 i0 := by
…
```

def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.solutionOfEquations line 111

Source documentation

Assemble a solution from its surface, seam, and vertex equations.

def solutionOfEquations
    (surface : ∀ f, (D.surfaceWord f).eval (algebraMap R A) g =
      (D.surfaceTarget P f).eval (algebraMap R A) g)
    (seam : ∀ s, SameFramedFlag (D.seamGrade s)
      (matrixUnitEquiv ((D.seamLeft s).eval (algebraMap R A) g))
      (matrixUnitEquiv ((D.seamRight s).eval (algebraMap R A) g)))
    (vertex : D.VertexHolds g) : D.Solution P A := by
…

Mentions: OAI.IntegralCharacterVarieties.SameFramedFlag

def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.producedMarkedSolution line 144