OAI/AlgebraicGeometry/CharacterVarieties/Foundation/BandCutTopology.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutParent line 13
2. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutExtra line 15
3. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutBoundaryCount line 17
4. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutBoundaryLength line 19
5. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutExtra_eq line 23
6. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutExtraPositions line 29

   Source documentation

   There is exactly one additional boundary, at the selected parent facet.

   def bandCutExtraPositions :
       ((f : F) × (_ : Fin (D.bandCutExtra q f)) × Fin 2) ≃ Fin 2 where
   …

7. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutTriplePositions line 47

   Source documentation

   Divide each old boundary index into its old side and its phase.

   def bandCutTriplePositions :
       ((f : F) × (b : Fin (D.boundaryCount f)) × Fin (D.boundaryLength f b*3)) ≃
         ((f : F) × (b : Fin (D.boundaryCount f)) × Fin (D.boundaryLength f b)) × Fin 3 where
   …

8. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutBoundaryPositions line 63
9. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutBoundarySide line 74
10. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutBoundaryLength_old line 85
11. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutBoundaryLength_new line 89
12. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutBoundarySide_old line 93
13. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutBoundarySide_new line 111
14. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutBoundaryPositive line 128
15. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutBoundaryFacet line 137
16. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.tripled_next_zero line 153
17. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.tripled_next_one line 161
18. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.tripled_next_two line 169
19. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutLong_pair line 179
20. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutLong_next line 188
21. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutBoundaryNext line 206
22. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutDiagram line 238

    Source documentation

    The topological inverse handle cut, with complete boundary cycles. The identity seam is an intermediate awaiting proper lower-gallery replacement.

    def bandCutDiagram : Diagram F (BandCutSeam S) (BandCutVertex V S q) (bandCutArity arity) where
    …

    Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram

23. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutDiagram_genus_drop line 256
24. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutDiagram_boundary_add line 261