OAI/AlgebraicGeometry/CharacterVarieties/Frames/MarkedFrames.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. opaque OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutGeneratorWitness line 18

   Source documentation

   A simultaneous splitting for arbitrary original generator coordinates, including the circle- gauged coordinates of the surface equation.

   opaque cutGeneratorWitness : IdentifiedBand (D.childDim q)
       (D.namedSeamFrame q (g (.frame q false)))
       (((D.namedSeamFrame q (g (.frame q false))).trans (D.namedParentLinear q g)).trans
         (MatrixIso.unit J).linearEquiv.symm) :=
   …

   Mentions: OAI.IntegralCharacterVarieties.MatrixIso.unit

2. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedCutFrames line 42
3. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedCutFrames_holds line 45
4. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.marked_values_vertexHolds line 54