OAI/AlgebraicGeometry/CharacterVarieties/Foundation/FlagGalleries.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.equivalence_chain line 14
2. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.matrix_list line 21
3. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.gridTranspose line 38

   Source documentation

   The row/column enumeration of the same intersection blocks.

   def gridTranspose (m n : ℕ) : Fin (m*n) ≃ Fin (n*m) :=
   …

4. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.gridTranspose_colors line 41
5. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.rectangular_permutation line 53

   Source documentation

   Row-by-row to column-by-column uses only adjacent vertices.

   theorem rectangular_permutation (parent : F) {m n : ℕ} (f : Fin m → Fin n → F) :
       Nonempty (OrderedChain parent ((List.ofFn fun i => List.ofFn (f i)).flatten)
         ((List.ofFn fun j => List.ofFn fun i => f i j).flatten)) := by
   …

   Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedChain

6. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.two_flag_gallery line 63

   Source documentation

   The finite band recipe for the band reduction: split every old left grade into its common intersection pieces, interchange adjacent pieces, then coarsen into all right grades. Every split/merge branch is retained by OrderedStep.kind.

   theorem two_flag_gallery (parent : F) {m n : ℕ} (row : Fin m → F) (col : Fin n → F)
       (grid : Fin m → Fin n → F) :
       Nonempty (OrderedChain parent (List.ofFn row) (List.ofFn col)) := by
   …

   Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedChain

7. structure OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedWalk line 80

   Source documentation

   Finite sequence of states and vertex tables. States do not impose extra conditions on solutions: they are the ordered facet names computed by the split/permutation/merge recipe.

   structure OrderedWalk (parent : F) (a b : List F) where
   …

8. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedWalk.refl line 89
9. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedWalk.cons line 96
10. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedChain.walk line 109
11. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.children_ext line 114
12. structure OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand line 129

    Source documentation

    Entire finite band, including all split branch ports. The exposed ports are the complement of the internal sewing, not chosen subsets.

    structure RealizedBand (parent : F) (a b : List F) where
    …

13. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.patch line 143
14. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedWalk.headIdentity line 150

    Source documentation

    An identity vertex is retained even for an empty walk, so the resulting band always has two exposed main ports and loses no branch occurrence.

    def headIdentity (w : OrderedWalk parent a b) : OrderedWalk parent a b :=
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedWalk

15. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedWalk.realize line 159
16. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.produced_two_flag_band line 181

    Source documentation

    Finite two-flag band producer: every row branch, column branch, and every intersection-block passage occurs in an allowed finite port patch.

    theorem produced_two_flag_band (parent : F) {m n : ℕ} (row : Fin m → F)
        (col : Fin n → F) (grid : Fin m → Fin n → F) :
        Nonempty (RealizedBand parent (List.ofFn row) (List.ofFn col)) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand

17. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.listRank line 191
18. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.listRank_nil line 192
19. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.listRank_cons line 193
20. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.listRank_append line 194
21. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.listRank_ofFn line 196
22. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration.Conservative line 200

    Source documentation

    Rank conservation on every ordered port (including side branches).

    def Decoration.Conservative {k : Kind} (d : Decoration k F) : Prop :=
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration

23. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration.conservative_iff line 203
24. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.splitLists_conservative line 214
25. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.passage_conservative line 228
26. inductive OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain line 238

    Source documentation

    A finite ranked gallery. The constructor stores a verified vertex, not a geometric bundle hypothesis; lengths and unused ports remain explicit.

    inductive RankedChain (parent : F) : List F → List F → Type
      | refl (a : List F) : RankedChain parent a a
      | step {a b c : List F} (s : OrderedStep parent a b)
          (hs : s.decoration.Conservative r) (p : RankedChain parent b c) : RankedChain parent a c
    
    namespace RankedChain
    variable {r} {parent : F}

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedStep

27. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain.forget line 245
28. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain.trans line 249
29. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain.single line 253
30. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain.split line 256
31. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain.merge line 262
32. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain.passage line 268
33. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.row_rank_sum line 278
34. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.ranked_refine_rows line 288

    Source documentation

    Rank conservation is verified on every refinement branch, not merely on the parent at the ends of a band.

    theorem ranked_refine_rows (parent : F) (rows : List (F × List F)) (left right : List F)
        (hp : r parent=listRank r (left++(rows.map Prod.fst++right)))
        (hr : ∀ x∈rows, r x.1=listRank r x.2) :
        Nonempty (RankedChain r parent (left++(rows.map Prod.fst++right))
          (left++(rows.flatMap Prod.snd++right))) ∧
        Nonempty (RankedChain r parent (left++(rows.flatMap Prod.snd++right))
          (left++(rows.map Prod.fst++right))) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.listRank, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain

35. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.ranked_permutation_chain line 312

    Source documentation

    Adjacent interchanges preserve the numerical rank of the parent, including zero blocks; this is the ranked version of the permutation producer.

    theorem ranked_permutation_chain (parent : F) {m : ℕ} (σ : Equiv.Perm (Fin m)) :
        ∀ (f : Fin m → F), r parent=listRank r (List.ofFn f) →
        Nonempty (RankedChain r parent (List.ofFn f) (List.ofFn (f ∘ σ.symm))) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.listRank, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain

36. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.ranked_equivalence_chain line 338
37. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.ranked_rectangular_permutation line 345
38. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.listRank_flatten line 356
39. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.ranked_two_flag_gallery line 363

    Source documentation

    Finite ranked two-flag band under the exact intersection-rank identities. No properness or positivity is required until later zero-block normalization.

    theorem ranked_two_flag_gallery (parent : F) {m n : ℕ} (row : Fin m → F) (col : Fin n → F)
        (grid : Fin m → Fin n → F) (hp : r parent=∑ i,r (row i))
        (hr : ∀ i,r (row i)=∑ j,r (grid i j)) (hc : ∀ j,r (col j)=∑ i,r (grid i j)) :
        Nonempty (RankedChain r parent (List.ofFn row) (List.ofFn col)) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain

40. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedWalk.Conservative line 397
41. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedWalk.conservative_cons line 399
42. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedWalk.conservative_headIdentity line 409
43. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedWalk.realize_conservative line 416
44. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain.walk_conservative line 423
45. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.produced_ranked_two_flag_band line 431

    Source documentation

    The finite band is an allowed incidence patch with the full rank identity at every port. Rank conservation is produced, not an extra interface.

    theorem produced_ranked_two_flag_band {m n : ℕ} (row : Fin m → F) (col : Fin n → F)
        (grid : Fin m → Fin n → F) (hp : r parent=∑ i,r (row i))
        (hr : ∀ i,r (row i)=∑ j,r (grid i j)) (hc : ∀ j,r (col j)=∑ i,r (grid i j)) :
        ∃ B : RealizedBand parent (List.ofFn row) (List.ofFn col),
          ∀ v,(B.decoration v).Conservative r := by
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand

46. def OAI.IntegralCharacterVarieties.flagGridSum line 445

    Source documentation

    All blocks in a rectangular lower-left prefix.

    def flagGridSum {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
        (W : ℕ → ℕ → Submodule K V) (i j : ℕ) : Submodule K V :=
    …

47. lemma OAI.IntegralCharacterVarieties.fin_iSup_castSucc line 450
48. lemma OAI.IntegralCharacterVarieties.flagGridSum_corner line 462
49. lemma OAI.IntegralCharacterVarieties.twoFlagGrid_choose line 469
50. lemma OAI.IntegralCharacterVarieties.twoFlagGrid_spans line 482
51. lemma OAI.IntegralCharacterVarieties.twoFlagGrid_dim_corner line 497
52. lemma OAI.IntegralCharacterVarieties.grid_sum_corner line 516
53. lemma OAI.IntegralCharacterVarieties.grid_sum_unique line 524
54. def OAI.IntegralCharacterVarieties.finiteSubmoduleSum line 540
55. lemma OAI.IntegralCharacterVarieties.finiteSubmoduleSum_surjective line 546
56. theorem OAI.IntegralCharacterVarieties.two_flag_common_splitting line 565

    Source documentation

    Every pair of finite flags has one simultaneous free splitting, including flags with repeated terms/zero blocks.

    theorem two_flag_common_splitting
        {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
        [FiniteDimensional K V]
        (F H : ℕ → Submodule K V) (hF : Monotone F) (hH : Monotone H)
        (hF0 : F 0=⊥) (hH0 : H 0=⊥) (n m : ℕ) (hFn : F n=⊤) (hHm : H m=⊤) :
        ∃ W : ℕ → ℕ → Submodule K V,
          (∀ i j, F i ⊓ H j=flagGridSum W i j) ∧
          Function.Bijective (fun v : (p : Fin n × Fin m) → W p.1.val p.2.val =>
            ∑ p, (v p : V)) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.flagGridSum