OAI/RepresentationTheory/KazhdanLusztig/ReflectionOrders.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KLInvariance.SchedulePaths.dispatch_append line 19
2. theorem OAI.KLInvariance.SchedulePaths.dispatch_add line 26
3. theorem OAI.KLInvariance.SchedulePaths.dispatch_mul_right line 37
4. theorem OAI.KLInvariance.SchedulePaths.dispatch_zero line 48
5. theorem OAI.KLInvariance.SchedulePaths.dispatch_sum line 56
6. theorem OAI.KLInvariance.SchedulePaths.dispatch_eq_sum_entries line 63
7. theorem OAI.KLInvariance.SchedulePaths.dispatch_eq_of_entries line 73
8. theorem OAI.KLInvariance.SchedulePaths.dispatch_congr_on line 84

   Source documentation

   A finite lower region is closed under every target occurring in its edge schedule, so values outside that region never enter its product.

   theorem dispatch_congr_on (T : R) (S : Set V) (p : List E)
       (htarget : ∀ e ∈ p, target e ∈ S) (v w : V → R)
       (hvw : ∀ x ∈ S, v x=w x) :
       ∀ x ∈ S, dispatch source target T v p x = dispatch source target T w p x := by
   …

   Mentions: OAI.KLInvariance.SchedulePaths.dispatch

9. theorem OAI.KLInvariance.SchedulePaths.dispatch_eq_finite_entries line 95
10. theorem OAI.KLInvariance.SchedulePaths.dispatch_eq_of_entries_on line 108
11. theorem OAI.KLInvariance.SchedulePaths.subpaths_eq_of_sorted line 124

    Source documentation

    A genuine path in a sorted schedule is determined by its edge set and strict label order. Arbitrary permutations of repeated reflection labels therefore have no effect.

    theorem subpaths_eq_of_sorted (label : E → Λ)
        (hties : ∀ e f, label e = label f → target e ≠ source f)
        (p q : List E)
        (hp : p.Pairwise (fun e f => label f ≤ label e))
        (hq : q.Pairwise (fun e f => label f ≤ label e))
        (hmem : ∀ e, e ∈ p ↔ e ∈ q) (x y : V) :
        subpaths source target p x y = subpaths source target q x y := by
    …

    Mentions: OAI.KLInvariance.SchedulePaths.subpaths

12. theorem OAI.KLInvariance.SchedulePaths.dispatch_eq_of_sorted line 145
13. theorem OAI.KLInvariance.SchedulePaths.dispatch_flatMap_eq line 159

    Source documentation

    Replacing each block by an equal actual operator replaces the product.

    theorem dispatch_flatMap_eq {A : Type*} (T : R) (blocks : List A) (p q : A → List E)
        (h : ∀ a ∈ blocks, ∀ v, dispatch source target T v (p a) =
          dispatch source target T v (q a)) (v : V → R) :
        dispatch source target T v (blocks.flatMap p) =
          dispatch source target T v (blocks.flatMap q) := by
    …

    Mentions: OAI.KLInvariance.SchedulePaths.dispatch

14. theorem OAI.KLInvariance.SchedulePaths.IsPath.map_iff line 173
15. theorem OAI.KLInvariance.SchedulePaths.exists_list_lift line 184
16. theorem OAI.KLInvariance.SchedulePaths.dispatch_entry_graph_embedding line 195

    Source documentation

    If all actual paths between the specified endpoints lie in a full embedded subgraph, its full sorted product computes the same entry.

    theorem dispatch_entry_graph_embedding (T : R) (label : E → Λ)
        (hties : ∀ e f, label e=label f → target e ≠ source f)
        (j : V' → V) (hj : Function.Injective j) (J : E' → E) (hJ : Function.Injective J)
        (hs : ∀ e, source (J e)=j (source' e))
        (ht : ∀ e, target (J e)=j (target' e))
        (p : List E) (q : List E') (hpnd : p.Nodup) (hqnd : q.Nodup)
        (hp : p.Pairwise (fun e f => label f ≤ label e))
        (hq : q.Pairwise (fun e f => label (J f) ≤ label (J e)))
        (hqfull : ∀ e, e ∈ q) (hJmem : ∀ e, J e ∈ p)
        (x y : V')
        (hpath : ∀ r ∈ subpaths source target p (j x) (j y), ∀ e ∈ r, ∃ e', J e'=e) :
        dispatch source target T (fun z => if z=j y then 1 else 0) p (j x) =
    …

    Mentions: OAI.KLInvariance.SchedulePaths.subpaths, OAI.KLInvariance.SchedulePaths.dispatch

17. theorem OAI.KLInvariance.TitsSpace.normalizedRoot_height line 265
18. theorem OAI.KLInvariance.TitsSpace.dual_normalizedRoot line 269
19. theorem OAI.KLInvariance.TitsSpace.geometricFunctional_normalizedRoot line 273
20. theorem OAI.KLInvariance.TitsSpace.normalizedRoot_mem_iff line 277
21. theorem OAI.KLInvariance.TitsSpace.rootPlane_eq_normalized_span line 285
22. theorem OAI.KLInvariance.TitsSpace.normalizedRoot_affine line 303

    Source documentation

    The intersection of a root-plane with the height-one hyperplane is the actual affine line through the two normalized roots.

    theorem normalizedRoot_affine {a b c : PositiveRoot M cs}
        (hc : c.val ∈ rootPlane a b) :
        ∃ t : ℝ, normalizedRoot c = t • normalizedRoot a + (1-t) • normalizedRoot b := by
    …

    Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.TitsSpace.rootPlane, OAI.KLInvariance.TitsSpace.normalizedRoot

23. theorem OAI.KLInvariance.TitsSpace.exists_affine_rootPlane line 318

    Source documentation

    On each genuine root plane, every height-normalized linear functional is an affine function of the fixed angular slope.

    theorem exists_affine_rootPlane (f : Module.Dual ℝ (I → ℝ))
        (a b : PositiveRoot M cs) (hab : a ≠ b) :
        ∃ c d : ℝ, ∀ r : PositiveRoot M cs, r.val ∈ rootPlane a b →
          f (normalizedRoot r) = c * geometricSlope r + d := by
    …

    Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.TitsSpace.rootPlane, OAI.KLInvariance.TitsSpace.normalizedRoot, OAI.KLInvariance.TitsSpace.geometricSlope

24. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.exists_affine line 351
25. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.path_coordinates line 379

    Source documentation

    All edges of a plane-labelled path lie in the full induced relative interval between its endpoints, with the original ambient labels.

    theorem path_coordinates {a₀ : W}
        (hmin : ∀ z ∈ planeSubgroup M cs P, cs.length a₀ ≤ cs.length (z*a₀))
        (g : planeSubgroup M cs P) {y : W} {p : List (AdaptedDyer.Edge cs)}
        (hp : IsPath (source cs) (target cs) ((g:W)*a₀) y p)
        (hP : ∀ e ∈ p, (rootLabel cs e).val ∈ P) :
        ∃ k : planeSubgroup M cs P, y=(k:W)*a₀ ∧ BruhatLE B.system g k ∧
          ∀ e ∈ p, ∃ l r : planeSubgroup M cs P,
            source cs e=(l:W)*a₀ ∧ target cs e=(r:W)*a₀ ∧
            BruhatLE B.system g l ∧ BruhatStep B.system l r ∧ BruhatLE B.system r k := by
    …

    Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup, OAI.KLInvariance.AdaptedDyer.Edge, OAI.KLInvariance.BruhatLE, OAI.KLInvariance.BruhatStep

26. def OAI.KLInvariance.TitsSpace.PlaneBasis.intervalToAmbient line 410
27. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.intervalToAmbient_injective line 413
28. def OAI.KLInvariance.TitsSpace.PlaneBasis.edgeToAmbient line 418
29. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.edgeToAmbient_source line 424
30. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.edgeToAmbient_target line 429
31. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.edgeToAmbient_injective line 434
32. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.edgeToAmbient_root line 444
33. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.path_edges_lift line 462

    Source documentation

    Edge-by-edge lifting of every plane path into the full relative interval. It is obtained from actual path connectivity, not from ambient comparability alone (which would not suffice).

    theorem path_edges_lift {a₀ : W}
        (hmin : ∀ z ∈ planeSubgroup M cs P, cs.length a₀ ≤ cs.length (z*a₀))
        {g k : planeSubgroup M cs P} {p : List (AdaptedDyer.Edge cs)}
        (hp : IsPath (source cs) (target cs) ((g:W)*a₀) ((k:W)*a₀) p)
        (hP : ∀ e ∈ p, (rootLabel cs e).val ∈ P) :
        ∀ e ∈ p, ∃ e' : BruhatGraph.Edge B.system g k, B.edgeToAmbient hmin e'=e := by
    …

    Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup, OAI.KLInvariance.AdaptedDyer.Edge, OAI.KLInvariance.BruhatGraph.Edge

34. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.dispatch_plane_reverse line 484

    Source documentation

    Reversal of a complete angular block of genuine ambient edges preserves all its endpoint entries. Fullness is with respect to the actual root plane, not to a rank-two subgroup chosen merely to contain two arbitrary reflections.

    theorem dispatch_plane_reverse {R : Type*} [Semiring R] (T : R) (b : W)
        (p : List (AdaptedDyer.Edge cs)) (hnd : p.Nodup)
        (hfull : ∀ e, e ∈ p ↔ (rootLabel cs e).val ∈ P ∧ BruhatLE cs (target cs e) b)
        (hs : p.Pairwise (fun e f => geometricSlope (rootLabel cs f) ≤ geometricSlope (rootLabel cs e)))
        (x y : W) (hy : BruhatLE cs y b) :
        dispatch (source cs) (target cs) T (fun z => if z=y then 1 else 0) p x =
          dispatch (source cs) (target cs) T (fun z => if z=y then 1 else 0) p.reverse x := by
    …

    Mentions: OAI.KLInvariance.AdaptedDyer.Edge, OAI.KLInvariance.BruhatLE, OAI.KLInvariance.TitsSpace.geometricSlope

35. def OAI.KLInvariance.SchedulePaths.sortedSchedule line 582
36. theorem OAI.KLInvariance.SchedulePaths.mem_sortedSchedule line 585
37. theorem OAI.KLInvariance.SchedulePaths.sortedSchedule_nodup line 588
38. theorem OAI.KLInvariance.SchedulePaths.sortedSchedule_pairwise line 592
39. def OAI.KLInvariance.SchedulePaths.blockValues line 596
40. def OAI.KLInvariance.SchedulePaths.scheduleBlock line 599
41. def OAI.KLInvariance.SchedulePaths.groupedSchedule line 602
42. theorem OAI.KLInvariance.SchedulePaths.mem_blockValues line 605
43. theorem OAI.KLInvariance.SchedulePaths.mem_scheduleBlock line 610
44. theorem OAI.KLInvariance.SchedulePaths.mem_groupedSchedule line 614
45. theorem OAI.KLInvariance.SchedulePaths.blockValues_strict line 625
46. theorem OAI.KLInvariance.SchedulePaths.groupedSchedule_nodup line 631
47. theorem OAI.KLInvariance.SchedulePaths.groupedSchedule_pairwise line 645
48. theorem OAI.KLInvariance.SchedulePaths.dispatch_entries_eq_of_sorted line 660
49. theorem OAI.KLInvariance.SchedulePaths.dispatch_flatMap_eq_on line 675

    Source documentation

    Replacement on a finite lower region requires no artificial finiteness assumption on the ambient Coxeter group.

    theorem dispatch_flatMap_eq_on (T : R) (S : Set V) (blocks : List A) (p q : A → List E)
        (htarget : ∀ a ∈ blocks, ∀ e ∈ p a, target e ∈ S)
        (h : ∀ a ∈ blocks, ∀ v, ∀ x ∈ S,
          dispatch source target T v (p a) x = dispatch source target T v (q a) x)
        (v : V → R) : ∀ x ∈ S,
        dispatch source target T v (blocks.flatMap p) x =
          dispatch source target T v (blocks.flatMap q) x := by
    …

    Mentions: OAI.KLInvariance.SchedulePaths.dispatch

50. def OAI.KLInvariance.TitsSpace.lexRootScore line 710
51. theorem OAI.KLInvariance.TitsSpace.lexRootScore_injective line 713
52. def OAI.KLInvariance.TitsSpace.lexEdgeScore line 719
53. theorem OAI.KLInvariance.TitsSpace.lexEdgeScore_ties line 722
54. theorem OAI.KLInvariance.TitsSpace.lex_affine_nonneg line 728
55. theorem OAI.KLInvariance.TitsSpace.lex_affine_neg line 737
56. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.lex_block_orientation line 753

    Source documentation

    Any linearly sorted full plane block is either angularly sorted or reverse-angularly sorted. This includes tied primary labels refined by the fixed genuine geometric functional.

    theorem lex_block_orientation (f : Module.Dual ℝ (I → ℝ))
        (p : List (AdaptedDyer.Edge cs))
        (hP : ∀ e ∈ p, (rootLabel cs e).val ∈ P)
        (hs : p.Pairwise (fun e e' => lexEdgeScore f e' ≤ lexEdgeScore f e)) :
        p.Pairwise (fun e e' => geometricSlope (rootLabel cs e') ≤ geometricSlope (rootLabel cs e)) ∨
        p.Pairwise (fun e e' => geometricSlope (rootLabel cs e) ≤ geometricSlope (rootLabel cs e')) := by
    …

    Mentions: OAI.KLInvariance.AdaptedDyer.Edge, OAI.KLInvariance.TitsSpace.lexEdgeScore, OAI.KLInvariance.TitsSpace.geometricSlope

57. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.dispatch_plane_functional line 779

    Source documentation

    A complete plane block, sorted by any functional, has precisely the same actual path product as its angularly sorted version.

    theorem dispatch_plane_functional {R : Type*} [Semiring R] (T : R) (b : W)
        (f : Module.Dual ℝ (I → ℝ)) (p q : List (AdaptedDyer.Edge cs))
        (hpnd : p.Nodup) (hqnd : q.Nodup)
        (hpfull : ∀ e, e ∈ p ↔ (rootLabel cs e).val ∈ P ∧ BruhatLE cs (target cs e) b)
        (hqfull : ∀ e, e ∈ q ↔ (rootLabel cs e).val ∈ P ∧ BruhatLE cs (target cs e) b)
        (hp : p.Pairwise (fun e e' => lexEdgeScore f e' ≤ lexEdgeScore f e))
        (hq : q.Pairwise (fun e e' => geometricSlope (rootLabel cs e') ≤ geometricSlope (rootLabel cs e)))
        (x y : W) (hy : BruhatLE cs y b) :
        dispatch (source cs) (target cs) T (fun z => if z=y then 1 else 0) p x =
          dispatch (source cs) (target cs) T (fun z => if z=y then 1 else 0) q x := by
    …

    Mentions: OAI.KLInvariance.AdaptedDyer.Edge, OAI.KLInvariance.BruhatLE, OAI.KLInvariance.TitsSpace.lexEdgeScore, OAI.KLInvariance.TitsSpace.geometricSlope

58. theorem OAI.KLInvariance.ReflectionSchedules.exists_avoiding_functional line 822

    Source documentation

    A countable family of nonzero vectors can be simultaneously avoided.

    theorem exists_avoiding_functional {A : Type v} [Countable A] (v : A → (I → ℝ)) :
        ∃ f : Module.Dual ℝ (I → ℝ), ∀ a, v a ≠ 0 → f (v a) ≠ 0 := by
    …

59. def OAI.KLInvariance.TitsSpace.pencil line 856
60. theorem OAI.KLInvariance.TitsSpace.pencil_zero line 860
61. theorem OAI.KLInvariance.TitsSpace.pencil_one line 863
62. theorem OAI.KLInvariance.TitsSpace.pencil_apply line 867
63. def OAI.KLInvariance.TitsSpace.rootDifference line 870
64. def OAI.KLInvariance.TitsSpace.wallVector line 872
65. def OAI.KLInvariance.TitsSpace.Transverse line 878

    Source documentation

    This is an actual genericity condition on linear functionals, not an assumed path or Hecke identity.

    def Transverse (f g : Module.Dual ℝ (I → ℝ)) : Prop :=
    …

66. theorem OAI.KLInvariance.TitsSpace.pencil_tie_plane line 881
67. theorem OAI.KLInvariance.TitsSpace.exists_common_transverse line 938

    Source documentation

    One intermediate functional is simultaneously transverse to any two specified generic endpoints, even with infinitely many positive roots.

    theorem exists_common_transverse (f h : Module.Dual ℝ (I → ℝ)) :
        ∃ g : Module.Dual ℝ (I → ℝ),
          Function.Injective (fun a : PositiveRoot M cs => g (normalizedRoot a)) ∧
          Transverse (M := M) (cs := cs) f g ∧ Transverse (M := M) (cs := cs) h g := by
    …

    Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.TitsSpace.normalizedRoot, OAI.KLInvariance.TitsSpace.Transverse

68. def OAI.KLInvariance.WallDyer.rootValue line 983
69. def OAI.KLInvariance.WallDyer.rootPlaneTies line 986
70. def OAI.KLInvariance.WallDyer.schedule line 991
71. def OAI.KLInvariance.WallDyer.entry line 994
72. theorem OAI.KLInvariance.WallDyer.block_entry_independent line 1000

    Source documentation

    The complete tied block at any genuine simple wall has an actual operator independent of the linear tie-breaking functional.

    theorem block_entry_independent {R : Type*} [Semiring R] (T : R) (b : W)
        (f : Module.Dual ℝ (I → ℝ)) (hf : rootPlaneTies (M := M) (cs := cs) f)
    …

    Mentions: OAI.KLInvariance.WallDyer.rootPlaneTies

73. theorem OAI.KLInvariance.WallDyer.grouped_entry_independent line 1054

    Source documentation

    All blocks may be replaced simultaneously on the finite lower region.

    theorem grouped_entry_independent {R : Type*} [Semiring R] (T : R) (b : W)
        (f : Module.Dual ℝ (I → ℝ)) (hf : rootPlaneTies (M := M) (cs := cs) f)
    …

    Mentions: OAI.KLInvariance.WallDyer.rootPlaneTies

74. theorem OAI.KLInvariance.WallDyer.entry_eq_grouped line 1079

    Source documentation

    Stable strict primary comparisons identify the genuine sorted schedule with the corresponding product of tied blocks.

    theorem entry_eq_grouped {R : Type*} [Semiring R] (T : R) (b : W)
        (f g : Module.Dual ℝ (I → ℝ))
        (h : ∀ e ∈ edgeFinset cs b, ∀ e' ∈ edgeFinset cs b,
          rootValue f e' < rootValue f e → rootValue g e' < rootValue g e)
        (x y : W) :
        entry (cs := cs) T g b x y =
    …

    Mentions: OAI.KLInvariance.WallDyer.rootValue, OAI.KLInvariance.WallDyer.entry

75. theorem OAI.KLInvariance.WallDyer.pencil_strict_stable line 1096
76. theorem OAI.KLInvariance.WallDyer.locally_constant_pencil line 1115

    Source documentation

    Crossing all actual root-plane walls leaves the full path matrix fixed, not merely a single adapted endpoint column.

    theorem locally_constant_pencil {R : Type*} [Semiring R] (T : R) (b : W)
        (f g : Module.Dual ℝ (I → ℝ))
        (hf : Function.Injective (fun a : PositiveRoot M cs => f (normalizedRoot a)))
        (hg : Transverse (M := M) (cs := cs) f g) (x y : W) (hx : BruhatLE cs x b) :
    …

    Mentions: OAI.KLInvariance.BruhatLE

77. theorem OAI.KLInvariance.WallDyer.entry_independent line 1131

    Source documentation

    Full matrix order independence for genuine finite geometric orders.

    theorem entry_independent {R : Type*} [Semiring R] (T : R) (b : W)
        (f h : Module.Dual ℝ (I → ℝ))
        (hf : Function.Injective (fun a : PositiveRoot M cs => f (normalizedRoot a)))
        (hh : Function.Injective (fun a : PositiveRoot M cs => h (normalizedRoot a)))
        (x y : W) (hx : BruhatLE cs x b) : entry (cs := cs) T f b x y=entry (cs := cs) T h b x y := by
    …

    Mentions: OAI.KLInvariance.BruhatLE, OAI.KLInvariance.WallDyer.entry

78. theorem OAI.KLInvariance.WallDyer.neg_numerator_normalized line 1160
79. theorem OAI.KLInvariance.WallDyer.subpaths_neg_numerator line 1167

    Source documentation

    An upper bound larger than the path endpoint creates no extra paths: every actual directed path stays inside its endpoint interval.

    theorem subpaths_neg_numerator (O : RatioOrder (M := M) (cs := cs))
    …

80. theorem OAI.KLInvariance.WallDyer.entry_neg_numerator line 1204
81. theorem OAI.KLInvariance.WallDyer.entry_eq_rTilde line 1214
82. theorem OAI.KLInvariance.WallDyer.geometric_entry_eq_rTilde line 1229

    Source documentation

    The manuscript's fixed geometric functional provides such a genuine full Dyer schedule for every finite lower Bruhat region.

    theorem geometric_entry_eq_rTilde (b x y : W) (hx : BruhatLE cs x b) (hy : BruhatLE cs y b) :
        entry (cs := cs) (Polynomial.X : Polynomial ℤ) (geometricFunctional (M := M) (cs := cs)) b x y =
    …

    Mentions: OAI.KLInvariance.BruhatLE, OAI.KLInvariance.WallDyer.entry