OAI/AlgebraicGeometry/CharacterVarieties/Foundation/ReorderedSolutions.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.IntegralCharacterVarieties.MatrixIso.unit_injective line 11
2. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.reorderPunctures line 26

   Source documentation

   Puncture scalars and genus are not changed by the re-basing.

   def reorderPunctures (P : D.Punctures R) : (D.reorderBoundary σ).Punctures R :=
   …

   Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.Punctures

3. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.reorder_boundaryEdge_eval line 29
4. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.reorder_boundaryWord_eval line 37
5. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.reorder_parentWord_eval line 45
6. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.reorder_seamLeft_eval line 54
7. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.reorder_seamRight_eval line 60
8. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.reorder_surfaceTarget_eval line 64
9. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.reorder_surfaceWord_eval line 68
10. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.reorderPathWords line 81

    Source documentation

    The choices depend only on the finite permutation, not on a solution or on a coefficient field. They are based path words.

    def reorderPathWords (f : F) : Fin (D.boundaryCount f) → FreeGroup (Fin (D.boundaryCount f)) :=
    …

11. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.reorderPathWords_spec line 84
12. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.reorderCircleBases line 91

    Source documentation

    Evaluate those same paths over an arbitrary coefficient ring.

    def reorderCircleBases : D.CircleBases (R:=A) := fun ⟨f,b⟩ =>
    …

13. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.basedReorderGenerators line 95
14. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.basedReorder_surfaceWord line 98
15. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.basedReorderSolution line 109

    Source documentation

    Full sewn-diagram solution after arbitrary reordering of boundary circles.

    def basedReorderSolution (P : D.Punctures R) (x : D.Solution P A) :
        (D.reorderBoundary σ).Solution (D.reorderPunctures σ P) A := by
    …

    Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.Solution