OAI/AlgebraicGeometry/CharacterVarieties/Frames/CutFrames.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutFromOldFrames line 14

   Source documentation

   Connected-strip incidence constructed from a pair of seam frames.

   def cutFromOldFrames [Finite V]
       (f h : (Matrix (Fin (D.seamDim q)) (Fin (D.seamDim q)) K)ˣ) :=
   …

2. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.colored_local_color line 27
3. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.transportFrames line 36
4. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.transportFrames_holds line 39
5. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCut_vertex_rank line 57
6. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCut_old_vertexRanks line 63
7. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCut_orig_ranks line 68
8. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCut_mirror_ranks line 73
9. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedOldFrames line 81
10. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedOrigFrames line 88
11. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMirrorFrames line 95
12. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCutVertexFrames line 104

    Source documentation

    The original and atomic frames satisfy the local vertex equations before the global gauge changes.

    def refinedCutVertexFrames (f : D.PortFrames (R:=R)) (v : V ⊕ (Fin (d.atomicBand.length+1) ⊕ Fin (d.atomicBand.length+1))) :
    …

13. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCutPortFrames line 112
14. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCutPortFrames_holds line 115