OAI/AlgebraicGeometry/CharacterVarieties/Foundation/SurfacePresentation.lean

GitHub source file

106 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram line 13

   Source documentation

   The finite oriented boundary cycles contain each side occurrence exactly once. Their successor is the one constructed from the allowed vertices. No cycle is discarded if a facet or a seam appears repeatedly.

   structure Diagram (F S V : Type) (arity : S → ℕ) where
   …

2. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.seamDim line 29
3. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.childDim line 30
4. inductive OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.Generator line 33

   Source documentation

   Every frame and every transport has its own occurrence index. Handle generators are retained even on closed or multiply incident facets.

   inductive Generator where
   …

5. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.generatorRank line 38
6. instance OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.finiteGenerator line 43
7. abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.Word line 59
8. structure OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.Punctures line 62

   Source documentation

   Scalar punctures, as prescribed full-ring units. Quasi-unipotence will be imposed at the density stage; the representing scheme itself needs only units.

   structure Punctures (D : Diagram F S V arity) (R : Type*) [CommRing R] where
   …

   Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram

9. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.frameWord line 67
10. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.sideWord line 68
11. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.parentWord line 70
12. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.childWord line 71
13. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.wordProduct line 73
14. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.commutatorWord line 76
15. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundaryEdgeWord line 81
16. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundaryWord line 86

    Source documentation

    Matrix transport reads a positive boundary path from right to left.

    def boundaryWord (f : F) (b : Fin (D.boundaryCount f)) : D.Word R (D.rank f) :=
    …

17. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.surfaceWord line 89
18. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.scalarUnit line 93
19. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.surfaceTarget line 96
20. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.seamLeft line 100

    Source documentation

    Seam-parallel transport from false to true uses the inverse CHILD transport, since each child's boundary orientation is opposite to the parent's.

    def seamLeft (s : S) : D.Word R (D.seamDim s) := .mul (D.parentWord s) (D.frameWord s false)

21. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.seamRight line 101
22. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.seamGrade line 105

    Source documentation

    Ordered flag grade for the direct sum of the child fibers.

    def seamGrade (s : S) (i : Fin (D.seamDim s)) : ℕ := ((blockIndex (D.childDim s)) i).1.val

23. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.edgeCircuit line 108

    Source documentation

    The surface and regular seam part of the diagram equations.

    def edgeCircuit (P : D.Punctures R) : FlagCircuit.Data R D.Generator D.generatorRank (F ⊕ S) where
    …

    Mentions: OAI.IntegralCharacterVarieties.FlagCircuit.Data

24. abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.EdgeCoordinate line 115

    Source documentation

    The finite matrix presentation of this portion of the local-system scheme, including inverses and all oriented boundary/facet equations.

    abbrev EdgeCoordinate (P : D.Punctures R) := (D.edgeCircuit P).Coordinate
    …

    Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.Coordinate

25. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.edgePointsEquiv line 119
26. structure OAI.IntegralCharacterVarieties.MatrixIso line 130

    Source documentation

    A genuinely invertible rectangular coordinate matrix; source and target fiber labels can differ, even if both occur on a single facet.

    structure MatrixIso (R : Type*) [CommRing R] (α β : Type*) [Fintype α] [Fintype β] where
    …

27. def OAI.IntegralCharacterVarieties.MatrixIso.linearEquiv line 140
28. def OAI.IntegralCharacterVarieties.MatrixIso.refl line 146
29. def OAI.IntegralCharacterVarieties.MatrixIso.symm line 147
30. def OAI.IntegralCharacterVarieties.MatrixIso.trans line 148
31. def OAI.IntegralCharacterVarieties.MatrixIso.unit line 154
32. def OAI.IntegralCharacterVarieties.MatrixIso.reindex line 164
33. def OAI.IntegralCharacterVarieties.MatrixIso.congr line 171
34. def OAI.IntegralCharacterVarieties.MatrixIso.block line 173
35. def OAI.IntegralCharacterVarieties.MatrixIso.sum line 192
36. def OAI.IntegralCharacterVarieties.MatrixIso.map line 205
37. theorem OAI.IntegralCharacterVarieties.MatrixIso.sameFramedFlag_iff line 212

    Source documentation

    Identified-flag equality, in matrix coordinates without equating or forgetting any of its named fibers.

    theorem sameFramedFlag_iff (a : α → ℕ) (x y : MatrixIso R α β) :
        SameFramedFlag a x.linearEquiv y.linearEquiv ↔
          ∀ i j, a j ≤ a i → (y.inv*x.val) i j=(1 : Matrix α α R) i j := by
    …

    Mentions: OAI.IntegralCharacterVarieties.MatrixIso, OAI.IntegralCharacterVarieties.SameFramedFlag

38. instance OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.fintypePort line 234
39. instance OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.fintypeChild line 235
40. structure OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks line 238

    Source documentation

    Ranks are attached to local occurrences. Their only identification is the corner pairing from the source vertex table.

    structure LocalRanks (k : Kind) where
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind

41. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.Parent line 245
42. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.Child line 246
43. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.Columns line 247
44. instance OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.fintypeColumns line 248
45. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.cornerEquiv line 252
46. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.portSide line 266

    Source documentation

    Each local port remembers its entire parent/child list at that precise endpoint. Facet labels may repeat without identifying any side coordinates.

    def portSide (p : LocalPort V D.ports.kind) (c : Option ((D.ports.kind p.1).table.Child p.2)) : Side S arity :=
    …

47. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.portSide_eq line 269
48. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.portFacet_corner line 272
49. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.vertexRanks line 278

    Source documentation

    Local vertex ranks are derived from the diagram, NOT additional rank hypotheses that might exclude one of its solutions.

    def vertexRanks (v : V) : VertexTable.LocalRanks (D.ports.kind v) where
    …

50. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.portColumnIndex line 287
51. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.portRowIndex line 292
52. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.portFrame line 299

    Source documentation

    The rectangular seam frame. Both child and parent bases come from named occurrences; all reindexings are fixed by the source incidence data.

    def portFrame (g : (e : D.Generator) → (Matrix (Fin (D.generatorRank e)) (Fin (D.generatorRank e)) R)ˣ)
        (p : LocalPort V D.ports.kind) :
        MatrixIso R ((D.vertexRanks p.1).Columns p.2) ((D.vertexRanks p.1).Parent p.2) :=
    …

    Mentions: OAI.IntegralCharacterVarieties.MatrixIso

53. structure OAI.IntegralCharacterVarieties.FlagComparison line 312

    Source documentation

    One comparison of flags carrying their named graded fibers.

    structure FlagComparison (R : Type*) [CommRing R] where
    …

54. abbrev OAI.IntegralCharacterVarieties.FlagComparison.Entry line 324
55. def OAI.IntegralCharacterVarieties.FlagComparison.equation line 325
56. def OAI.IntegralCharacterVarieties.FlagComparison.Holds line 326
57. theorem OAI.IntegralCharacterVarieties.FlagComparison.holds_iff_equations line 328
58. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.passageGrade line 342

    Source documentation

    Fine list positions, with exactly the prescribed pair merged for an adjacent interchange. This retains the entire A⊕B identified quotient.

    def passageGrade {m : ℕ} (t : Passage m) (j : Fin m) : ℕ :=
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Passage

59. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.passageColumns line 347
60. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.passageParent line 352
61. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.passageComparison line 357
62. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.forwardRanks line 372

    Source documentation

    Reversal changes germ endpoint directions, not any fiber/refinement data.

    def forwardRanks (d : LocalRanks (.splitting a b c true)) : LocalRanks (.splitting a b c false) :=
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks

63. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.prefixRank line 375
64. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.suffixRank line 378
65. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.SplitA line 381
66. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.SplitC line 383
67. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.SplitB line 385
68. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.SplitW line 387
69. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.splitBefore line 391

    Source documentation

    Ordered source decomposition of before and after lists.

    def splitBefore (d : LocalRanks (.splitting a b c false)) :
        d.Columns .before ≃ (d.SplitA false ⊕ (d.SplitW ⊕ d.SplitC false)) where
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks

70. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.splitAfter line 407
71. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.splitPrefix line 418
72. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.splitSuffix line 420
73. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.splitBranchChildren line 422
74. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.splitBranchParent line 424
75. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.splitParent line 426
76. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.splitRefinement line 430

    Source documentation

    Refinement: leave every old prefix/suffix fiber unchanged, and in exactly the old W-block insert its named third-seam frame.

    def splitRefinement (d : LocalRanks (.splitting a b c false))
        (w : @MatrixIso R _ (d.Columns .branch) (d.Parent .branch) (d.fintypeColumns .branch) inferInstance) :
        @MatrixIso R _ (d.Columns .after) (d.Columns .before) (d.fintypeColumns .after) (d.fintypeColumns .before) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks, OAI.IntegralCharacterVarieties.MatrixIso

77. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.splitComparison line 440
78. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.comparison line 455

    Source documentation

    All and only the permitted source vertex comparisons, including complement and quotient maps at a swap, and reverse refinement at a merge.

    def comparison : (k : Kind) → (d : LocalRanks k) →
        (∀ p, MatrixIso R (d.Columns p) (d.Parent p)) → FlagComparison R
      | .passage _ _,d,f => d.passageComparison f
      | .splitting _ _ _ false,d,f => d.splitComparison f
      | .splitting _ _ _ true,d,f => d.forwardRanks.splitComparison f
    
    end LocalRanks
    end OccurrenceIncidence.VertexTable
    end IntegralCharacterVarieties
    namespace IntegralCharacterVarieties
    open scoped Classical Matrix
    namespace MatrixIso
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks, OAI.IntegralCharacterVarieties.MatrixIso, OAI.IntegralCharacterVarieties.FlagComparison, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.passage, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable

79. theorem OAI.IntegralCharacterVarieties.MatrixIso.ext line 470
80. lemma OAI.IntegralCharacterVarieties.MatrixIso.map_refl line 473
81. lemma OAI.IntegralCharacterVarieties.MatrixIso.map_trans line 476
82. lemma OAI.IntegralCharacterVarieties.MatrixIso.map_reindex line 480
83. lemma OAI.IntegralCharacterVarieties.MatrixIso.map_congr line 484
84. lemma OAI.IntegralCharacterVarieties.MatrixIso.map_sum line 487
85. lemma OAI.IntegralCharacterVarieties.MatrixIso.map_unit line 492
86. def OAI.IntegralCharacterVarieties.FlagComparison.map line 498
87. theorem OAI.IntegralCharacterVarieties.FlagComparison.equation_map line 507
88. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.splitComparison_map line 523
89. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.comparison_map line 535
90. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.portFrame_map line 551
91. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.vertexComparison line 558

    Source documentation

    Comparison at this vertex, with the occurrence transports already expressed in the shared facet frames.

    def vertexComparison
        (g : (e : D.Generator) → (Matrix (Fin (D.generatorRank e)) (Fin (D.generatorRank e)) R)ˣ)
        (v : V) : FlagComparison R :=
    …

    Mentions: OAI.IntegralCharacterVarieties.FlagComparison

92. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.vertexComparison_map line 564
93. def OAI.IntegralCharacterVarieties.EquationQuotient.ideal line 574
94. abbrev OAI.IntegralCharacterVarieties.EquationQuotient.Coordinate line 575
95. lemma OAI.IntegralCharacterVarieties.EquationQuotient.ideal_le_ker line 577
96. def OAI.IntegralCharacterVarieties.EquationQuotient.pointsEquiv line 584

    Source documentation

    Exact equation quotient over any full coefficient ring.

    def pointsEquiv : {φ : B →ₐ[R] A // ∀ j, φ (e j)=0} ≃ (Coordinate e →ₐ[R] A) where
    …

    Mentions: OAI.IntegralCharacterVarieties.EquationQuotient.Coordinate

97. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.universalEdge line 608
98. abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.VertexEntry line 612
99. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.vertexEquation line 614
100. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.VertexHolds line 618

     Source documentation

     All permitted vertex conditions on the matrix system.

     def VertexHolds
         (g : (e : D.Generator) → (Matrix (Fin (D.generatorRank e)) (Fin (D.generatorRank e)) A)ˣ) : Prop :=
     …

101. abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.Coordinate line 623

     Source documentation

     The finite coordinate algebra, retaining all surface relations, all regular seam identifications and all vertex refinements/complements.

     abbrev Coordinate := EquationQuotient.Coordinate (D.vertexEquation P)

     Mentions: OAI.IntegralCharacterVarieties.EquationQuotient.Coordinate

102. abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.Solution line 626

     Source documentation

     The split-frame solution functor of the incidence diagram.

     abbrev Solution (A : Type*) [CommRing A] [Algebra R A] :=
     …

103. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.vertex_equations_iff line 630

     Source documentation

     Specialization of the universal vertex equations is precisely the stated geometric vertex condition, including the natural maps at a swap.

     theorem vertex_equations_iff (φ : D.EdgeCoordinate P →ₐ[R] A) :
         (∀ j, φ (D.vertexEquation P j)=0) ↔
           D.VertexHolds ((D.edgePointsEquiv P).symm φ).val := by
     …

104. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.pointsEquiv line 652

     Source documentation

     The equivalence works over an arbitrary commutative algebra, in particular the full ring of integers, and retains forward AND inverse entries.

     def pointsEquiv : D.Solution P A ≃ (D.Coordinate P →ₐ[R] A) :=
     …

105. instance OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.finiteVertexEntry line 658
106. instance OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.finiteType line 659