OAI/AlgebraicGeometry/CharacterVarieties/Frames/SeamValues.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.valuesFromPorts_seamHolds_canonical line 12

   Source documentation

   The evaluated framed flag equation depends only on the ports and ranks, not on the boundary enumeration.

   lemma valuesFromPorts_seamHolds_canonical
       {F S V K R : Type} {arity : S → ℕ} [Field K] [CommRing R] [Finite S]
       (D : Diagram F S V arity) (frames : D.PortFrames (R:=K))
   …

   Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram