OAI/RepresentationTheory/KazhdanLusztig/Hecke.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.KLInvariance.Hecke.Space line 24

   Source documentation

   The standard free module of the actual Coxeter group.

   abbrev Space (W C : Type*) [Zero C] := W →₀ C

2. def OAI.KLInvariance.Hecke.basis line 26
3. theorem OAI.KLInvariance.Hecke.end_ext line 29
4. def OAI.KLInvariance.Hecke.left line 39

   Source documentation

   Normalized Hecke multiplication: H_s² = 1 + a H_s.

   noncomputable def left (cs : CoxeterSystem M W) (a : C) (i : B) :
       Module.End C (Space W C) :=
   …

   Mentions: OAI.KLInvariance.Hecke.Space

5. def OAI.KLInvariance.Hecke.right line 44
6. theorem OAI.KLInvariance.Hecke.left_basis line 49
7. theorem OAI.KLInvariance.Hecke.right_basis line 54
8. theorem OAI.KLInvariance.Hecke.left_right_commute line 59
9. theorem OAI.KLInvariance.Hecke.left_quadratic line 83
10. def OAI.KLInvariance.Hecke.leftInv line 99

    Source documentation

    Inverse normalized Hecke generator, available without inverting any scalar.

    noncomputable def leftInv (cs : CoxeterSystem M W) (a : C) (i : B) :
        Module.End C (Space W C) := left cs a i - a • 1

    Mentions: OAI.KLInvariance.Hecke.Space, OAI.KLInvariance.Hecke.left

11. theorem OAI.KLInvariance.Hecke.left_mul_leftInv line 102
12. theorem OAI.KLInvariance.Hecke.leftInv_mul_left line 115
13. def OAI.KLInvariance.Hecke.leftWord line 128
14. theorem OAI.KLInvariance.Hecke.leftWord_nil line 131
15. theorem OAI.KLInvariance.Hecke.leftWord_cons line 134
16. theorem OAI.KLInvariance.Hecke.leftWord_one line 139

    Source documentation

    Acting on the identity along a reduced word gives exactly its standard basis element.

    theorem leftWord_one (cs : CoxeterSystem M W) (a : C) {ω : List B}
        (hω : cs.IsReduced ω) :
        leftWord cs a ω (basis 1) = basis (cs.wordProd ω) := by
    …

    Mentions: OAI.KLInvariance.Hecke.leftWord, OAI.KLInvariance.Hecke.basis

17. def OAI.KLInvariance.Hecke.rightWord line 152
18. theorem OAI.KLInvariance.Hecke.rightWord_nil line 155
19. theorem OAI.KLInvariance.Hecke.rightWord_cons line 158
20. theorem OAI.KLInvariance.Hecke.rightWord_one line 161
21. theorem OAI.KLInvariance.Hecke.commute_rightWord line 182
22. theorem OAI.KLInvariance.Hecke.commuting_ext line 191

    Source documentation

    The regular right action is cyclic, with cyclic vector the identity.

    theorem commuting_ext (cs : CoxeterSystem M W) (a : C)
        {f g : Module.End C (Space W C)}
        (hf : ∀ i, Commute f (right cs a i))
        (hg : ∀ i, Commute g (right cs a i))
        (h : f (basis 1) = g (basis 1)) : f = g := by
    …

    Mentions: OAI.KLInvariance.Hecke.Space, OAI.KLInvariance.Hecke.right, OAI.KLInvariance.Hecke.basis

23. theorem OAI.KLInvariance.Hecke.leftWord_commute_right line 210
24. theorem OAI.KLInvariance.Hecke.leftWord_independent line 218
25. def OAI.KLInvariance.Hecke.unit line 225
26. def OAI.KLInvariance.Hecke.wordUnit line 232
27. theorem OAI.KLInvariance.Hecke.wordUnit_val line 235
28. theorem OAI.KLInvariance.Hecke.wordUnit_independent line 244
29. def OAI.KLInvariance.Hecke.standardUnit line 252

    Source documentation

    The genuine normalized standard-basis action, a unit in the regular endomorphism algebra. No presentation relations are assumed.

    noncomputable def standardUnit (cs : CoxeterSystem M W) (a : C) (w : W) :
        (Module.End C (Space W C))ˣ :=
    …

    Mentions: OAI.KLInvariance.Hecke.Space

30. theorem OAI.KLInvariance.Hecke.standardUnit_word line 256
31. theorem OAI.KLInvariance.Hecke.standardUnit_one line 262
32. theorem OAI.KLInvariance.Hecke.standardUnit_basis_one line 267
33. theorem OAI.KLInvariance.Hecke.standardUnit_simple_mul line 272
34. theorem OAI.KLInvariance.Hecke.standardUnit_mul_simple line 286
35. def OAI.KLInvariance.Hecke.barBasis line 303

    Source documentation

    The bar image of an actual standard basis vector; inverse units give expression independence before any polynomial coefficients are extracted.

    noncomputable def barBasis (cs : CoxeterSystem M W) (a : C) (w : W) : Space W C :=
    …

    Mentions: OAI.KLInvariance.Hecke.Space

36. theorem OAI.KLInvariance.Hecke.barBasis_one line 306
37. theorem OAI.KLInvariance.Hecke.barBasis_simple_mul_ascent line 309
38. theorem OAI.KLInvariance.Hecke.leftInv_barBasis line 322
39. def OAI.KLInvariance.Hecke.barLinear line 339
40. theorem OAI.KLInvariance.Hecke.barLinear_basis line 342
41. theorem OAI.KLInvariance.Hecke.barLinear_left line 348

    Source documentation

    Intertwining with the opposite parameter. In Laurent coefficients this is the semilinear Hecke bar relation.

    theorem barLinear_left (cs : CoxeterSystem M W) (a : C) (i : B) :
        barLinear cs a * left cs (-a) i = leftInv cs a i * barLinear cs a := by
    …

    Mentions: OAI.KLInvariance.Hecke.barLinear, OAI.KLInvariance.Hecke.left, OAI.KLInvariance.Hecke.leftInv

42. theorem OAI.KLInvariance.Hecke.barLinear_leftInv line 358
43. theorem OAI.KLInvariance.Hecke.barLinear_barBasis line 367

    Source documentation

    The inverse-parameter bar transforms are mutually inverse.

    theorem barLinear_barBasis (cs : CoxeterSystem M W) (a : C) (w : W) :
        barLinear cs a (barBasis cs (-a) w) = basis w := by
    …

    Mentions: OAI.KLInvariance.Hecke.barLinear, OAI.KLInvariance.Hecke.barBasis, OAI.KLInvariance.Hecke.basis

44. theorem OAI.KLInvariance.Hecke.barLinear_inverse line 381
45. theorem OAI.KLInvariance.Hecke.leftInv_basis line 388
46. theorem OAI.KLInvariance.Hecke.left_coeff line 395
47. theorem OAI.KLInvariance.Hecke.leftInv_coeff line 424
48. theorem OAI.KLInvariance.Hecke.simple_mul_le_ascent line 431
49. theorem OAI.KLInvariance.Hecke.barBasis_zero line 441

    Source documentation

    Triangularity for the genuine reflection-generated order.

    theorem barBasis_zero (cs : CoxeterSystem M W) (a : C) (x y : W)
        (hxy : ¬BruhatLE cs x y) : barBasis cs a y x = 0 := by
    …

    Mentions: OAI.KLInvariance.BruhatLE, OAI.KLInvariance.Hecke.barBasis

50. theorem OAI.KLInvariance.Hecke.barBasis_diagonal line 466
51. def OAI.KLInvariance.Hecke.rTilde line 482

    Source documentation

    Normalized R-polynomials, obtained from the bar action rather than postulated with an inconsistent choice of descent.

    noncomputable def rTilde (cs : CoxeterSystem M W) (x y : W) : ℤ[X] :=
    …

52. theorem OAI.KLInvariance.Hecke.rTilde_diagonal line 485
53. theorem OAI.KLInvariance.Hecke.rTilde_zero line 488
54. theorem OAI.KLInvariance.Hecke.rTilde_recursion line 491
55. def OAI.KLInvariance.HeckeQ.left line 514

    Source documentation

    Unnormalized equal-parameter Hecke multiplication, T_s²=q+(q−1)T_s.

    noncomputable def left (cs : CoxeterSystem M W) (q : C) (i : B) :
        Module.End C (Space W C) :=
    …

56. def OAI.KLInvariance.HeckeQ.right line 521
57. theorem OAI.KLInvariance.HeckeQ.left_basis line 528
58. theorem OAI.KLInvariance.HeckeQ.right_basis line 534
59. theorem OAI.KLInvariance.HeckeQ.left_right_commute line 540
60. theorem OAI.KLInvariance.HeckeQ.left_quadratic line 569
61. def OAI.KLInvariance.HeckeQ.leftInv line 583
62. theorem OAI.KLInvariance.HeckeQ.leftInv_apply line 586
63. theorem OAI.KLInvariance.HeckeQ.left_mul_leftInv line 589
64. theorem OAI.KLInvariance.HeckeQ.leftInv_mul_left line 602
65. def OAI.KLInvariance.HeckeQ.leftWord line 615
66. theorem OAI.KLInvariance.HeckeQ.leftWord_nil line 618
67. theorem OAI.KLInvariance.HeckeQ.leftWord_cons line 621
68. theorem OAI.KLInvariance.HeckeQ.leftWord_one line 626

    Source documentation

    Acting on the identity along q reduced word gives exactly its standard basis element.

    theorem leftWord_one (cs : CoxeterSystem M W) (q : C) {ω : List B}
        (hω : cs.IsReduced ω) :
        leftWord cs q ω (basis 1) = basis (cs.wordProd ω) := by
    …

    Mentions: OAI.KLInvariance.HeckeQ.leftWord

69. def OAI.KLInvariance.HeckeQ.rightWord line 639
70. theorem OAI.KLInvariance.HeckeQ.rightWord_nil line 642
71. theorem OAI.KLInvariance.HeckeQ.rightWord_cons line 645
72. theorem OAI.KLInvariance.HeckeQ.rightWord_one line 648
73. theorem OAI.KLInvariance.HeckeQ.commute_rightWord line 669
74. theorem OAI.KLInvariance.HeckeQ.commuting_ext line 678

    Source documentation

    The regular right action is cyclic, with cyclic vector the identity.

    theorem commuting_ext (cs : CoxeterSystem M W) (q : C)
        {f g : Module.End C (Space W C)}
        (hf : ∀ i, Commute f (right cs q i))
        (hg : ∀ i, Commute g (right cs q i))
        (h : f (basis 1) = g (basis 1)) : f = g := by
    …

    Mentions: OAI.KLInvariance.HeckeQ.right

75. theorem OAI.KLInvariance.HeckeQ.leftWord_commute_right line 697
76. theorem OAI.KLInvariance.HeckeQ.leftWord_independent line 705
77. def OAI.KLInvariance.HeckeQ.unit line 712
78. def OAI.KLInvariance.HeckeQ.wordUnit line 719
79. theorem OAI.KLInvariance.HeckeQ.wordUnit_val line 722
80. theorem OAI.KLInvariance.HeckeQ.wordUnit_independent line 731
81. def OAI.KLInvariance.HeckeQ.standardUnit line 739

    Source documentation

    The genuine normalized standard-basis action, a unit in the regular endomorphism algebra. No presentation relations are assumed.

    noncomputable def standardUnit (cs : CoxeterSystem M W) (q : Cˣ) (w : W) :
        (Module.End C (Space W C))ˣ :=
    …

82. theorem OAI.KLInvariance.HeckeQ.standardUnit_word line 743
83. theorem OAI.KLInvariance.HeckeQ.standardUnit_one line 749
84. theorem OAI.KLInvariance.HeckeQ.standardUnit_basis_one line 754
85. theorem OAI.KLInvariance.HeckeQ.standardUnit_simple_mul line 759
86. theorem OAI.KLInvariance.HeckeQ.standardUnit_mul_simple line 773
87. def OAI.KLInvariance.HeckeQ.barBasis line 790

    Source documentation

    The bar image of an actual standard basis vector; inverse units give expression independence before any polynomial coefficients are extracted.

    noncomputable def barBasis (cs : CoxeterSystem M W) (q : Cˣ) (w : W) : Space W C :=
    …

88. theorem OAI.KLInvariance.HeckeQ.barBasis_one line 793
89. theorem OAI.KLInvariance.HeckeQ.barBasis_simple_mul_ascent line 796
90. theorem OAI.KLInvariance.HeckeQ.leftInv_barBasis line 810
91. def OAI.KLInvariance.HeckeQ.barLinear line 833
92. theorem OAI.KLInvariance.HeckeQ.barLinear_basis line 836
93. theorem OAI.KLInvariance.HeckeQ.barLinear_left line 841

    Source documentation

    Linear intertwining, before specializing coefficients to a Laurent ring.

    theorem barLinear_left (cs : CoxeterSystem M W) (q : Cˣ) (i : B) :
        barLinear cs q * left cs (↑q⁻¹ : C) i = leftInv cs q i * barLinear cs q := by
    …

    Mentions: OAI.KLInvariance.HeckeQ.barLinear, OAI.KLInvariance.HeckeQ.left, OAI.KLInvariance.HeckeQ.leftInv

94. theorem OAI.KLInvariance.HeckeQ.barLinear_leftInv line 848
95. theorem OAI.KLInvariance.HeckeQ.barLinear_barBasis line 862

    Source documentation

    Applying coefficient inversion and the Hecke bar twice is the identity.

    theorem barLinear_barBasis (cs : CoxeterSystem M W) (q : Cˣ) (w : W) :
        barLinear cs q (barBasis cs q⁻¹ w) = basis w := by
    …

    Mentions: OAI.KLInvariance.HeckeQ.barLinear, OAI.KLInvariance.HeckeQ.barBasis

96. theorem OAI.KLInvariance.HeckeQ.barLinear_inverse line 876
97. theorem OAI.KLInvariance.HeckeQ.leftInv_basis line 882
98. theorem OAI.KLInvariance.HeckeQ.leftInv_coeff line 895
99. theorem OAI.KLInvariance.HeckeQ.barBasis_zero line 941

    Source documentation

    Triangularity in the actual Bruhat order.

    theorem barBasis_zero (cs : CoxeterSystem M W) (q : Cˣ) (x y : W)
        (hxy : ¬BruhatLE cs x y) : barBasis cs q y x = 0 := by
    …

    Mentions: OAI.KLInvariance.BruhatLE, OAI.KLInvariance.HeckeQ.barBasis

100. theorem OAI.KLInvariance.HeckeQ.barBasis_diagonal line 966
101. def OAI.KLInvariance.HeckeQ.rValue line 986

     Source documentation

     R-value extracted from the genuine Hecke bar, with the classical sign and leading q-power. No recurrence is imposed in this definition.

     noncomputable def rValue (cs : CoxeterSystem M W) (q : Cˣ) (x y : W) : C :=
     …

102. theorem OAI.KLInvariance.HeckeQ.rValue_diagonal line 989
103. theorem OAI.KLInvariance.HeckeQ.rValue_zero line 994
104. theorem OAI.KLInvariance.HeckeQ.rValue_recursion line 1000

     Source documentation

     The classical R recursion holds for every left descent, by Hecke operator independence. This is the consistency obligation for actual R.

     theorem rValue_recursion (cs : CoxeterSystem M W) (q : Cˣ) (x y : W) (i : B)
         (hy : cs.length (cs.simple i * y) < cs.length y) :
         rValue cs q x y =
           if cs.length (cs.simple i * x) < cs.length x then
             rValue cs q (cs.simple i * x) (cs.simple i * y)
           else ((q : C) - 1) * rValue cs q x (cs.simple i * y) +
             (q : C) * rValue cs q (cs.simple i * x) (cs.simple i * y) := by
     …

     Mentions: OAI.KLInvariance.HeckeQ.rValue

105. def OAI.KLInvariance.lowerFinset line 1042

     Source documentation

     A concrete finite lower ideal of the genuine Bruhat order.

     noncomputable def lowerFinset (cs : CoxeterSystem M W) (y : W) : Finset W :=
     …

106. theorem OAI.KLInvariance.mem_lowerFinset line 1045
107. theorem OAI.KLInvariance.HeckeQ.bar_coeff_inverse line 1055
108. theorem OAI.KLInvariance.HeckeQ.rValue_inverse_factor line 1069
109. theorem OAI.KLInvariance.HeckeQ.rValue_inverse line 1085

     Source documentation

     The exact R-kernel identity, before specialization to polynomials.

     theorem rValue_inverse (cs : CoxeterSystem M W) (q : Cˣ) (x y : W) :
         ∑ z ∈ lowerFinset cs y,
           rValue cs q x z * (q : C) ^ cs.length y * (↑q⁻¹ : C) ^ cs.length z *
             rValue cs q⁻¹ z y = if x = y then 1 else 0 := by
     …

     Mentions: OAI.KLInvariance.lowerFinset, OAI.KLInvariance.HeckeQ.rValue

110. theorem OAI.KLInvariance.eval₂_reflect_unit line 1101

     Source documentation

     Reflection of a bounded-degree polynomial evaluated at an actual unit.

     theorem eval₂_reflect_unit {C : Type*} [CommRing C] (q : Cˣ)
         (p : ℤ[X]) (d : ℕ) (hp : p.natDegree ≤ d) :
         Polynomial.eval₂ (Int.castRingHom C) (q : C) (reflect d p) =
           (q : C) ^ d * Polynomial.eval₂ (Int.castRingHom C) (↑q⁻¹ : C) p := by
     …