OAI/AlgebraicGeometry/CharacterVarieties/Foundation/SplitFlags.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.IntegralCharacterVarieties.MatrixIso.linearEquiv_congr_apply line 13
2. lemma OAI.IntegralCharacterVarieties.MatrixIso.linearEquiv_congr_symm_apply line 22
3. lemma OAI.IntegralCharacterVarieties.MatrixIso.linearEquiv_trans_apply line 27
4. lemma OAI.IntegralCharacterVarieties.MatrixIso.linearEquiv_diagonal_apply line 32
5. lemma OAI.IntegralCharacterVarieties.MatrixIso.linearEquiv_trans_symm_apply line 37
6. lemma OAI.IntegralCharacterVarieties.MatrixIso.linearEquiv_diagonal_symm_apply line 43
7. theorem OAI.IntegralCharacterVarieties.MatrixIso.linearEquiv_reindex line 55
8. theorem OAI.IntegralCharacterVarieties.MatrixIso.linearEquiv_sum_inl line 62
9. theorem OAI.IntegralCharacterVarieties.MatrixIso.linearEquiv_sum_inr line 69
10. lemma OAI.IntegralCharacterVarieties.mem_framedPrefix line 79
11. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.coarseW line 92
12. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.fineW line 95
13. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.refinement_coarseW line 100
14. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.refinement_prefix line 108
15. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.refinement_suffix line 115
16. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.beforeGrade line 123

    Source documentation

    Source-order grades, not an arbitrary enumeration.

    def beforeGrade (z : d.Columns .before) : ℕ :=
    …

17. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.afterGrade line 125
18. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.branchGrade line 127
19. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.beforeGrade_prefix line 129
20. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.beforeGrade_middle line 131
21. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.beforeGrade_suffix line 135
22. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.afterGrade_prefix line 139
23. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.afterGrade_middle line 141
24. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.afterGrade_suffix line 143
25. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.current_iff line 149
26. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.afterPrefix_iff line 167
27. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.refinement_current_iff line 196
28. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.refinement_flag_iff line 211

    Source documentation

    At the split matrix, the refined interval flag is the inverse image of the additional seam flag INSIDE the old coarse W interval.

    theorem refinement_flag_iff (v : d.Columns .after → R) (j : ℕ) (hj : j≤b) :
        v∈coordinatePrefix R d.afterGrade (a+j) ↔
          (d.splitRefinement w).linearEquiv v∈coordinatePrefix R d.beforeGrade (a+1) ∧
          d.coarseW ((d.splitRefinement w).linearEquiv v)∈
            framedPrefix d.branchGrade w.linearEquiv j := by
    …

    Mentions: OAI.IntegralCharacterVarieties.coordinatePrefix, OAI.IntegralCharacterVarieties.framedPrefix

29. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.beforeParentFrame line 224
30. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.rightFrame_eq line 227
31. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.rightFrame_formula line 232
32. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.old_refined_flag line 242

    Source documentation

    The equality below is derived from the source comparison itself.

    theorem old_refined_flag (v : d.Parent .after → R) (j : ℕ) (hj : j≤b) :
        v∈framedPrefix d.afterGrade (f .after).linearEquiv (a+j) ↔
          v∈framedPrefix d.beforeGrade (d.beforeParentFrame f).linearEquiv (a+1) ∧
          d.coarseW ((d.beforeParentFrame f).linearEquiv.symm v)∈
            framedPrefix d.branchGrade (f .branch).linearEquiv j := by
    …

    Mentions: OAI.IntegralCharacterVarieties.framedPrefix

33. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.branchProjection line 269
34. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.right_branch_coordinates line 275
35. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.old_branch_grade line 293

    Source documentation

    Every named fine quotient coordinate agrees with the old branch frame. This uses the GRADED clause of the old vertex equation.

    theorem old_branch_grade (z : d.Columns .branch) (v : d.Parent .after → R)
        (hv : v∈framedPrefix d.afterGrade (f .after).linearEquiv (a+z.1.val+1)) :
        d.fineW ((f .after).linearEquiv.symm v) z=
          (f .branch).linearEquiv.symm (d.branchProjection f v) z := by
    …

    Mentions: OAI.IntegralCharacterVarieties.framedPrefix

36. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.branchSubsystem line 304
37. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.old_branch_intersections line 312

    Source documentation

    The branch subsystem's entire fine flag is obtained from the old U intersection flag, in the named additional-seam module.

    theorem old_branch_intersections (U : Submodule R (d.Parent .after → R))
        (j : ℕ) (hj : j≤b) :
        (U ⊓ framedPrefix d.afterGrade (f .after).linearEquiv (a+j)).map
            (d.branchProjection f)=
          d.branchSubsystem f U ⊓ framedPrefix d.branchGrade (f .branch).linearEquiv j := by
    …

    Mentions: OAI.IntegralCharacterVarieties.framedPrefix

38. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.HasOldSplit line 327

    Source documentation

    The output records the exact source prefix criterion together with all U intersection images, rather than only relative-position dimensions.

    def HasOldSplit : Prop :=
    …

39. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.old_split_flags line 342
40. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.OldSplitExtracted line 345
41. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.comparison_oldSplit line 351
42. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.oldSplit_extraction line 369

    Source documentation

    The split/merge extraction follows from the entire old solution.

    theorem oldSplit_extraction (v : V) :
        LocalRanks.OldSplitExtracted A (D.ports.kind v) (D.vertexRanks v)
          (fun p => D.portFrame g.val.val ⟨v,p⟩) :=
    …