OAI/RepresentationTheory/KazhdanLusztig/DihedralIntervals.lean

GitHub source file

137 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KLInvariance.Dihedral.wordProd_alt_odd line 15
2. def OAI.KLInvariance.Dihedral.rotation line 24
3. theorem OAI.KLInvariance.Dihedral.simple_rotation line 26
4. theorem OAI.KLInvariance.Dihedral.simple_rotation_zpow line 31
5. def OAI.KLInvariance.Dihedral.indexWord line 41

   Source documentation

   The signed coordinate evaluates both alternating rays in the same group. The Euclidean quotient also gives the correct odd negative coordinates.

    def indexWord (cs : CoxeterSystem M W) (i : ℤ) : W :=
   …

6. theorem OAI.KLInvariance.Dihedral.indexWord_even line 45
7. theorem OAI.KLInvariance.Dihedral.indexWord_odd line 48
8. theorem OAI.KLInvariance.Dihedral.indexWord_nat line 53
9. theorem OAI.KLInvariance.Dihedral.indexWord_neg_nat line 63
10. theorem OAI.KLInvariance.Dihedral.exists_indexWord line 80
11. theorem OAI.KLInvariance.Dihedral.indexWord_reflection_mul line 90

    Source documentation

    A reflection acts on the signed index line by reflection in its midpoint. Finite dihedral groups are handled by equality in the group, without choosing residue representatives here.

     theorem indexWord_reflection_mul (cs : CoxeterSystem M W) {a : ℤ} (ha : Odd a)
        (i : ℤ) : indexWord cs a * indexWord cs i = indexWord cs (a-i) := by
    …

    Mentions: OAI.KLInvariance.Dihedral.indexWord

12. theorem OAI.KLInvariance.Dihedral.indexWord_label line 112
13. def OAI.KLInvariance.TitsSpace.linearPolynomial line 137
14. def OAI.KLInvariance.TitsSpace.orbitSpline line 141
15. theorem OAI.KLInvariance.TitsSpace.orbitSpline_self line 144
16. theorem OAI.KLInvariance.TitsSpace.orbitSpline_reflection line 147
17. theorem OAI.KLInvariance.TitsSpace.exists_pair_vector line 162
18. theorem OAI.KLInvariance.TitsSpace.orbitSpline_pair_factor line 176
19. theorem OAI.KLInvariance.TitsSpace.orbitSpline_single_factor line 193
20. theorem OAI.KLInvariance.Dihedral.reflection_of_parity line 228
21. def OAI.KLInvariance.Dihedral.oppositeExternal line 235
22. def OAI.KLInvariance.Dihedral.sameExternal line 239
23. theorem OAI.KLInvariance.Dihedral.oppositeExternal_reflection line 243
24. def OAI.KLInvariance.Dihedral.interpolationRoot line 248
25. theorem OAI.KLInvariance.Dihedral.interpolation_exists line 251
26. def OAI.KLInvariance.MomentGraph.Sheaf.modelOutgoing line 341
27. theorem OAI.KLInvariance.MomentGraph.Sheaf.mem_modelOutgoing line 345
28. def OAI.KLInvariance.MomentGraph.Sheaf.modelProduct line 350
29. def OAI.KLInvariance.MomentGraph.Sheaf.HasFlowDown line 352
30. theorem OAI.KLInvariance.MomentGraph.Sheaf.structureCompatible_iff line 359
31. theorem OAI.KLInvariance.MomentGraph.Sheaf.flowDown_flabby line 372
32. def OAI.KLInvariance.Dihedral.inducedRoot line 464
33. def OAI.KLInvariance.Dihedral.inducedLabel line 467
34. theorem OAI.KLInvariance.Dihedral.external_step line 470
35. theorem OAI.KLInvariance.Dihedral.step_external line 480
36. def OAI.KLInvariance.Dihedral.externalEdge line 491
37. theorem OAI.KLInvariance.Dihedral.externalEdge_mem line 496
38. def OAI.KLInvariance.Dihedral.outgoingEquiv line 503
39. theorem OAI.KLInvariance.Dihedral.interpolation_product line 521
40. theorem OAI.KLInvariance.Dihedral.hasFlowDown line 531
41. theorem OAI.KLInvariance.Dihedral.inducedLabel_prime line 554
42. theorem OAI.KLInvariance.Dihedral.label_eq_of_induced_dvd line 561
43. theorem OAI.KLInvariance.Dihedral.model_flabby line 580
44. def OAI.KLInvariance.TitsSpace.PlaneBasis.modelLabel line 612
45. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.model_flabby line 616
46. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.model_generated line 622
47. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.model_quotient line 626
48. theorem OAI.KLInvariance.bruhat_top_of_all_descents line 644
49. theorem OAI.KLInvariance.Dihedral.exists_common_upper line 667
50. theorem OAI.KLInvariance.Dihedral.map_not_alt line 700
51. theorem OAI.KLInvariance.Dihedral.swap_alt line 705
52. theorem OAI.KLInvariance.Dihedral.length_alt_le_length line 709
53. theorem OAI.KLInvariance.Dihedral.length_indexWord_nat line 722
54. theorem OAI.KLInvariance.Dihedral.length_indexWord_neg_nat line 727
55. theorem OAI.KLInvariance.Dihedral.length_indexWord line 732
56. theorem OAI.KLInvariance.Dihedral.leftDescent_alt line 742
57. theorem OAI.KLInvariance.Dihedral.indexWord_add_even line 752
58. theorem OAI.KLInvariance.Dihedral.rotation_pow_max line 763

    Source documentation

    The maximal-length case supplies the precise signed period, without an extra finiteness hypothesis or a numerical cosine restriction.

     theorem rotation_pow_max (cs : CoxeterSystem M W) (w : W)
        (hmax : ∀ z, cs.length z ≤ cs.length w) : rotation cs ^ cs.length w = 1 := by
    …

    Mentions: OAI.KLInvariance.Dihedral.rotation

59. theorem OAI.KLInvariance.Dihedral.indexWord_period line 779
60. theorem OAI.KLInvariance.Dihedral.indexWord_mod_period line 785
61. theorem OAI.KLInvariance.Dihedral.indexWord_step line 803
62. theorem OAI.KLInvariance.Dihedral.neg_indexWord_step line 809
63. def OAI.KLInvariance.TitsSpace.PlaneBasis.prefixRoot line 826
64. def OAI.KLInvariance.TitsSpace.PlaneBasis.negPrefixRoot line 829
65. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.prefixRoot_strictMono line 832
66. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.negPrefixRoot_strictAnti line 844
67. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.edgeRoot_eq_of_label line 874
68. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.prefixRoot_eq_edgeRoot line 882
69. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.negPrefixRoot_eq_edgeRoot line 893
70. def OAI.KLInvariance.SignedDihedral.Before line 917
71. theorem OAI.KLInvariance.SignedDihedral.before_same_source_pos line 920
72. theorem OAI.KLInvariance.SignedDihedral.before_same_source_neg line 932
73. theorem OAI.KLInvariance.SignedDihedral.before_next_source line 944
74. theorem OAI.KLInvariance.SignedDihedral.midpoint_mod line 965
75. theorem OAI.KLInvariance.SignedDihedral.finite_before_same line 975

    Source documentation

    For two outgoing edges at the same vertex, reduction modulo the period has no wrap-around exception in the midpoint comparison table.

     theorem finite_before_same {m i j z : ℤ} (hm : 0 < m)
        (hi : |i| < |j|) (hz : |i| < |z|)
        (hjM : -m < j ∧ j ≤ m) (hzM : -m < z ∧ z ≤ m) :
        (i+j) % (2*m) < (i+z) % (2*m) ↔ Before (i+j) (i+z) := by
    …

    Mentions: OAI.KLInvariance.SignedDihedral.Before

76. theorem OAI.KLInvariance.SignedDihedral.finite_before_next line 1001
77. theorem OAI.KLInvariance.SignedDihedral.eligible_ranks_card line 1027
78. def OAI.KLInvariance.SignedDihedral.arrowAfter line 1046
79. def OAI.KLInvariance.SignedDihedral.countAfter line 1051

    Source documentation

    Double internal ranks and the singleton top, with no singleton bottom term because upward arrows never end at the bottom.

     noncomputable def countAfter (a label c : ℤ) : ℕ :=
    …

80. theorem OAI.KLInvariance.SignedDihedral.arrowAfter_of_not_lt line 1055
81. theorem OAI.KLInvariance.SignedDihedral.arrowAfter_self line 1058
82. theorem OAI.KLInvariance.Dihedral.length_indexWord_unbounded line 1075
83. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.edgeRoot_inverted_iff line 1091
84. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.edgeRoot_positive_lt_negative line 1101
85. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.edgeRoot_infinite_order line 1143

    Source documentation

    The two angular rays of an infinite canonical dihedral subsystem, with actual ambient labels, have precisely the source's signed-midpoint order.

     theorem edgeRoot_infinite_order
        (hu : ∀ n : ℕ, ∃ w, n ≤ B.system.length w)
        {x y z t : planeSubgroup M cs P}
        (hxy : BruhatStep B.system x y) (hzt : BruhatStep B.system z t)
        {a b : ℤ} (ha : Odd a) (hb : Odd b)
        (hx : y*x⁻¹=indexWord B.system a) (hz : t*z⁻¹=indexWord B.system b) :
        geometricSlope (B.edgeRoot hxy) < geometricSlope (B.edgeRoot hzt) ↔
          SignedDihedral.Before a b := by
    …

    Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup, OAI.KLInvariance.BruhatStep, OAI.KLInvariance.TitsSpace.geometricSlope, OAI.KLInvariance.SignedDihedral.Before

86. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.max_length_pos line 1234
87. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.odd_residue_repr line 1240
88. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.edgeRoot_finite_order line 1251

    Source documentation

    The actual ambient angular order in a finite canonical plane subsystem is the increasing residue order on odd doubled midpoints.

     theorem edgeRoot_finite_order
        (w : planeSubgroup M cs P) (hmax : ∀ z, B.system.length z ≤ B.system.length w)
        {x y z t : planeSubgroup M cs P}
        (hxy : BruhatStep B.system x y) (hzt : BruhatStep B.system z t)
        {a b : ℤ} (ha : Odd a) (hb : Odd b)
        (hx : y*x⁻¹=indexWord B.system a) (hz : t*z⁻¹=indexWord B.system b) :
        geometricSlope (B.edgeRoot hxy) < geometricSlope (B.edgeRoot hzt) ↔
          a % (2*(B.system.length w:ℤ)) < b % (2*(B.system.length w:ℤ)) := by
    …

    Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup, OAI.KLInvariance.BruhatStep, OAI.KLInvariance.TitsSpace.geometricSlope

89. theorem OAI.KLInvariance.Dihedral.indexWord_pos_ne_neg line 1281
90. theorem OAI.KLInvariance.Dihedral.lower_length_fiber line 1296
91. theorem OAI.KLInvariance.Dihedral.lower_zero_fiber line 1316
92. theorem OAI.KLInvariance.Dihedral.lower_top_fiber line 1326
93. theorem OAI.KLInvariance.Dihedral.sum_lower_signed line 1341

    Source documentation

    Actual finite dihedral lower ideals have two internal alternating rays and a singleton top. The doubled identity contributes zero.

     theorem sum_lower_signed (cs : CoxeterSystem M W) (c : W)
        {A : Type*} [AddCommMonoid A] (f : W → A) (h1 : f 1=0) :
        ∑ z ∈ lowerFinset cs c, f z =
          (∑ n ∈ Finset.range (cs.length c),
            (f (indexWord cs n)+f (indexWord cs (-(n:ℤ))))) + f c := by
    …

    Mentions: OAI.KLInvariance.lowerFinset, OAI.KLInvariance.Dihedral.indexWord

94. def OAI.KLInvariance.Dihedral.GoodIndex line 1378
95. theorem OAI.KLInvariance.Dihedral.maximal_or_unbounded line 1381
96. theorem OAI.KLInvariance.Dihedral.max_length_positive line 1396
97. theorem OAI.KLInvariance.Dihedral.maximal_eq line 1402
98. theorem OAI.KLInvariance.Dihedral.goodIndex_nat line 1412
99. theorem OAI.KLInvariance.Dihedral.goodIndex_neg_nat line 1419
100. theorem OAI.KLInvariance.Dihedral.exists_good_index line 1425
101. theorem OAI.KLInvariance.SignedDihedral.odd_add_natAbs line 1455
102. theorem OAI.KLInvariance.SignedDihedral.odd_sub_natAbs line 1464
103. theorem OAI.KLInvariance.SignedDihedral.arrowAfter_pos line 1468
104. theorem OAI.KLInvariance.SignedDihedral.arrowAfter_neg line 1488
105. theorem OAI.KLInvariance.SignedDihedral.arrowAfter_next line 1510
106. theorem OAI.KLInvariance.SignedDihedral.countAfter_base line 1537
107. theorem OAI.KLInvariance.SignedDihedral.total_outgoing_count line 1563

     Source documentation

     A double internal level together with the singleton top contributes one outgoing arrow per rank, independently of top parity.

      theorem total_outgoing_count (L C : ℕ) (h : L ≤ C) :
         (∑ r ∈ Finset.range C, if L < r ∧ Odd (L+r) then 2 else 0) +
           (if L < C ∧ Odd (L+C) then 1 else 0) = C-L := by
     …

108. theorem OAI.KLInvariance.SignedDihedral.odd_add_abs line 1610
109. theorem OAI.KLInvariance.SignedDihedral.arrowAfter_far line 1628
110. def OAI.KLInvariance.SignedDihedral.positiveCount line 1646
111. theorem OAI.KLInvariance.SignedDihedral.positiveCount_formula line 1650
112. theorem OAI.KLInvariance.SignedDihedral.countAfter_pos_formula line 1688
113. theorem OAI.KLInvariance.SignedDihedral.countAfter_neg_formula line 1718
114. theorem OAI.KLInvariance.SignedDihedral.countAfter_next_formula line 1741
115. theorem OAI.KLInvariance.SignedDihedral.countAfter_difference line 1765

     Source documentation

     The signed-index cardinality identity for the source's forward angular order. Its identification with actual Coxeter angular roots is separate.

      theorem countAfter_difference {i j c : ℤ} (hij : |i| < |j|)
         (ho : Odd (i.natAbs+j.natAbs)) (h : c=j ∨ |j| < |c|) :
         countAfter i (i+j) c = countAfter j (i+j) c + (j.natAbs-i.natAbs-1)/2 := by
     …

     Mentions: OAI.KLInvariance.SignedDihedral.countAfter

116. theorem OAI.KLInvariance.Dihedral.natAbs_lt_iff line 1788
117. theorem OAI.KLInvariance.Dihedral.index_step_iff line 1792
118. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.edgeRoot_same_table line 1814
119. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.edgeRoot_next_table line 1833
120. def OAI.KLInvariance.TitsSpace.PlaneBasis.afterIndicator line 1852
121. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.afterIndicator_one line 1858
122. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.afterIndicator_same line 1867
123. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.afterIndicator_next line 1885
124. def OAI.KLInvariance.TitsSpace.PlaneBasis.laterCount line 1919
125. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.laterCount_same line 1923
126. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.laterCount_next line 1948
127. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.laterCount_difference line 1974
128. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.afterIndicator_eq_zero line 2022
129. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.interval_laterCount line 2030

     Source documentation

     Counting only the relative interval above a lower bound does not alter an outgoing count based at a vertex above that bound.

      theorem interval_laterCount {a x c : planeSubgroup M cs P}
         (hax : BruhatLE B.system a x) (α : PositiveRoot M cs) :
         (∑ᶠ z : Interval B.system a c, B.afterIndicator x α z.val) =
           B.laterCount x α c := by
     …

     Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup, OAI.KLInvariance.BruhatLE, OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.Interval

130. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.edgeRoot_coset line 2048
131. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.interval_map_count line 2064

     Source documentation

     A full relative interval transport carries the actual angular later-edge count. An arbitrary graph embedding would not suffice here.

      theorem interval_map_count {a c : planeSubgroup M cs P}
         (hac : BruhatLE B.system a c)
         (F : Interval B.system a c → planeSubgroup M' cs' P')
         (hinj : Function.Injective F)
         (hrange : Set.range F = {z | BruhatLE B'.system (F ⟨a,bruhat_refl B.system a,hac⟩) z ∧
           BruhatLE B'.system z (F ⟨c,hac,bruhat_refl B.system c⟩)})
         (x : Interval B.system a c) (α : PositiveRoot M' cs') :
         (∑ᶠ z : Interval B.system a c, B'.afterIndicator (F x) α (F z)) =
           B'.laterCount (F x) α (F ⟨c,hac,bruhat_refl B.system c⟩) := by
     …

     Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup, OAI.KLInvariance.BruhatLE, OAI.KLInvariance.Interval, OAI.KLInvariance.bruhat_refl, OAI.KLInvariance.TitsSpace.PositiveRoot

132. def OAI.KLInvariance.TitsSpace.ambientAfterIndicator line 2107
133. theorem OAI.KLInvariance.TitsSpace.ambientAfterIndicator_of_le line 2113
134. theorem OAI.KLInvariance.TitsSpace.ambientAfterIndicator_edge_self line 2120
135. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.ambientAfterIndicator_coset line 2128
136. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.transported_count_difference line 2145
137. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.transported_count_difference_all line 2200

     Source documentation

     The same scheduled count with no restriction on the relative rank.

      theorem transported_count_difference_all {a₀ u b : W} {u' b' : W'}
         (hmin : ∀ z ∈ planeSubgroup M cs P, cs.length a₀ ≤ cs.length (z*a₀))
         {a c : planeSubgroup M cs P} (hac : BruhatLE B.system a c)
         (hlo : BruhatLE cs u ((a:W)*a₀)) (hhi : BruhatLE cs ((c:W)*a₀) b)
         (e : Interval cs u b ≃o Interval cs' u' b')
         (y : Interval B.system a c) (hxy : BruhatStep B.system a y.val) :
         let inc := B.cosetIntervalMap hmin hlo hhi
     …

     Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup, OAI.KLInvariance.BruhatLE, OAI.KLInvariance.Interval, OAI.KLInvariance.BruhatStep