OAI/AlgebraicGeometry/CharacterVarieties/Seams/PortEquations.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Seam equations from port values

Identity side transports and equal port frames imply the framed seam equation.

  1. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.valuesFromPorts_trivialSides_seamHolds line 17

    Source documentation

    Port values with trivial side transports and equal frames satisfy the seam equation.

    lemma valuesFromPorts_trivialSides_seamHolds
    {F S V R K : Type} {arity : S → ℕ} [CommRing R] [CommRing K]
    (D : Diagram F S V arity) (φ : R →+* K)
    (frames : D.PortFrames (R:=K)) (side : D.SideValues (R:=K))
…

    Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram