OAI/AlgebraicGeometry/CharacterVarieties/Cutting/AtomicGallery.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.atomWeight line 18

   Source documentation

   The occupancy of a specified old simultaneous basis atom in a facet.

   def atomWeight (s : F → Set A) (t : A) (f : F) : ℕ := if t∈s f then 1 else 0
   …

2. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration.AtomConservative line 24

   Source documentation

   Occurrence-sensitive atom conservation, stronger than dimension conservation.

   def AtomConservative : Prop := ∀ t, d.Conservative (atomWeight s t)

   Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.atomWeight

3. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration.atom_sum line 26
4. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration.atomicData line 34

   Source documentation

   A checked literal partition, derived from atom conservation at all ports. No coverage hypothesis about solution varieties is introduced here.

   def atomicData (h : d.AtomConservative s) : AtomicData k A where
   …

   Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData

5. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain.ForRank line 56

   Source documentation

   Additional conservation on the same concrete ranked program.

   def ForRank (q : F → ℕ) : {a b : List F} → RankedChain r parent a b → Prop
     | _,_,.refl _ => True
     | _,_,.step s _ p => s.decoration.Conservative q ∧ p.ForRank q

   Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain

6. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain.forRank_trans line 60
7. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain.forRank_single line 67
8. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain.forRank_walk line 71
9. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain.forRank_reindex line 77
10. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.WeightedCleanGallery line 94

    Source documentation

    The same fresh, crossing-free gallery conserves every labeled weight. Weights are instantiated below by atom occupancies; hence this records actual partitions and not only the numerical rank equation.

    def WeightedCleanGallery (N : ℕ) (r : F → ℕ) (M : I → ℕ) (w : I → F → ℕ)
        (a b : List F) : Prop :=
    …

11. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.WeightedCleanGallery.refl line 105
12. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.WeightedCleanGallery.trans line 106
13. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.WeightedCleanGallery.split line 113
14. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.WeightedCleanGallery.merge line 142
15. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.WeightedCleanGallery.refine_rows line 179
16. lemma OAI.IntegralCharacterVarieties.DirectedSort.Program.ranked_forRank line 220

    Source documentation

    The original no-recrossing program conserves each atom on the very same literal passage, not on a separately chosen permutation word.

    lemma ranked_forRank (f : α → F) (p : Program a b) (hp : N=listRank r (a.map f))
        (M : ℕ) (w : F → ℕ) (hw : M=listRank w (a.map f)) :
        (p.ranked f hp).ForRank (freshRank M w) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.DirectedSort.Program

17. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.WeightedReducedGallery line 241

    Source documentation

    A fresh, directed/no-recrossing family-conserving gallery.

    def WeightedReducedGallery (N : ℕ) (r : F → ℕ) (M : I → ℕ) (w : I → F → ℕ)
        (a b : List F) : Prop :=
    …

18. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.WeightedReducedGallery.clean_left line 247
19. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.WeightedReducedGallery.clean_right line 255
20. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.WeightedReducedGallery.rectangular line 270
21. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.WeightedReducedGallery.two_flag_gallery line 324

    Source documentation

    The lower gallery is produced with both ordinary ranks and every atom occupancy conserved, while retaining the literal fresh/no-recrossing program.

    theorem two_flag_gallery {m n : ℕ} (row : Fin m → F) (col : Fin n → F)
        (grid : Fin m → Fin n → F)
        (hinj : Function.Injective (fun p : Fin m × Fin n => grid p.1 p.2))
        (hp : N=∑ i,r (row i))
        (hr : ∀ i,r (row i)=∑ j,r (grid i j))
        (hc : ∀ j,r (col j)=∑ i,r (grid i j))
        (hwp : ∀ t,M t=∑ i,w t (row i))
        (hwr : ∀ t i,w t (row i)=∑ j,w t (grid i j))
        (hwc : ∀ t j,w t (col j)=∑ i,w t (grid i j)) :
        WeightedReducedGallery N r M w (List.ofFn row) (List.ofFn col) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.WeightedReducedGallery

22. inductive OAI.IntegralCharacterVarieties.TwoFlagBand.Secondary line 394

    Source documentation

    Occurrence labels for the lower strips; the maximal parent is deliberately not a constructor. Equal ranks or isomorphic modules do not identify labels.

    inductive Secondary (n m : ℕ)
      | row : Fin n → Secondary n m
      | col : Fin m → Secondary n m
      | cell : Fin n → Fin m → Secondary n m
      deriving DecidableEq, Fintype
    
    namespace RankShape
    variable {n m r : ℕ} (d : RankShape n m r)

    Mentions: OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape

23. def OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.secondaryRank line 402
24. lemma OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.fresh_parent_row_rank line 407
25. abbrev OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.Atom line 412

    Source documentation

    Actual names of the common-graded basis vectors, including empty cells.

    abbrev Atom := (p : Fin n × Fin m) × Fin (d.val p).val

26. def OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.secondaryAtoms line 414
27. def OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.facetAtoms line 419
28. lemma OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.atom_parent_sum line 432
29. lemma OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.atom_row_sum line 436
30. lemma OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.atom_col_sum line 442
31. lemma OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.cell_injective line 448
32. lemma OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.weighted_band line 452
33. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedWalk.crossings line 467
34. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedWalk.crossings_cons line 469
35. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedWalk.crossings_refl line 475
36. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedWalk.crossings_headIdentity line 476
37. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RankedChain.walk_crossings line 482
38. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.crossings line 493
39. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.realize_crossings line 495
40. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.exists_reduced_congr line 500
41. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.reduced_ranked_two_flag_band line 514

    Source documentation

    A finite band with rank conservation, exhaustion of the fresh parent germs, and no repeated crossing.

    theorem reduced_ranked_two_flag_band {m n : ℕ} (row : Fin m → F) (col : Fin n → F)
        (grid : Fin m → Fin n → F)
        (hinj : Function.Injective (fun p : Fin m × Fin n => grid p.1 p.2))
        (hp : N = ∑ i, rank (row i))
        (hr : ∀ i, rank (row i) = ∑ j, rank (grid i j))
        (hc : ∀ j, rank (col j) = ∑ i, rank (grid i j)) :
        ∃ B : RealizedBand none (List.ofFn (some ∘ row)) (List.ofFn (some ∘ col)),
          (∀ v, (B.decoration v).Conservative (freshRank N rank)) ∧
          (∀ v, ∃ d : (B.kind v).SecondaryNames F,
            B.decoration v = (B.kind v).freshDecoration d) ∧ B.crossings.Nodup := by
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.freshRank

42. def OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.atomicChain line 544
43. def OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.atomicBand line 548
44. lemma OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.atomicBand_conservative line 551
45. lemma OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.atomicBand_fresh line 556
46. lemma OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.atomicBand_nodup line 561
47. lemma OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.facet_atomWeight line 565
48. lemma OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.atomicBand_atoms line 571
49. def OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.vertexAtoms line 578
50. lemma OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.atomicBand_comparison line 581
51. def OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.rowAtomsEquiv line 596
52. def OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.colAtomsEquiv line 612
53. def OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.cellAtomsEquiv line 628
54. lemma OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.card_secondaryAtoms line 639
55. lemma OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.card_atoms line 649
56. lemma OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.card_facetAtoms line 652
57. lemma OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.vertexAtoms_rank line 658