OAI/RepresentationTheory/KazhdanLusztig/IntegralPairings.lean

GitHub source file

169 declarations, 0 contain sorry, 0 declared as axioms

Hilbert recurrences, projective section ranges, integral lattices and graded perfect adjoints.

  1. theorem OAI.KLInvariance.Hilbert.hasSum_shift_coeff line 14
  2. theorem OAI.KLInvariance.Hilbert.numerator_unique line 24
  3. theorem OAI.KLInvariance.Hilbert.numerator_add_shift line 38
  4. theorem OAI.KLInvariance.TitsSpace.bottStalk_finrank_descent line 86
  5. theorem OAI.KLInvariance.TitsSpace.bottStalkCharacter_ascent line 104
  6. theorem OAI.KLInvariance.TitsSpace.bottStalkCharacter_descent line 120
  7. theorem OAI.KLInvariance.HeckeQ.left_coeff line 152
  8. theorem OAI.KLInvariance.HeckeQ.left_plus_coeff line 197
  9. def OAI.KLInvariance.HeckeQ.positiveWord line 204
  10. theorem OAI.KLInvariance.HeckeQ.positiveWord_nil line 208
  11. theorem OAI.KLInvariance.HeckeQ.positiveWord_cons_coeff line 211
  12. theorem OAI.KLInvariance.TitsSpace.bottStalkCharacter_zero line 237
  13. def OAI.KLInvariance.TitsSpace.bottTopPolynomialEquiv line 248
  14. theorem OAI.KLInvariance.TitsSpace.bottTopPolynomialEquiv_homogeneous line 254
  15. theorem OAI.KLInvariance.TitsSpace.bottStalkCharacter_top line 260
  16. theorem OAI.KLInvariance.TitsSpace.bottStalkCharacter_nil line 279
  17. theorem OAI.KLInvariance.TitsSpace.bottStalkCharacter_eq_heckeWord line 289
  18. def OAI.KLInvariance.CoordinateProjection.eval line 321
  19. def OAI.KLInvariance.CoordinateProjection.image line 322
  20. def OAI.KLInvariance.CoordinateProjection.project line 323
  21. theorem OAI.KLInvariance.CoordinateProjection.project_surjective line 325
  22. theorem OAI.KLInvariance.CoordinateProjection.project_apply line 330
  23. theorem OAI.KLInvariance.CoordinateProjection.project_zero_iff line 332
  24. def OAI.KLInvariance.CoordinateProjection.restrict line 341
  25. theorem OAI.KLInvariance.CoordinateProjection.restrict_project line 350
  26. theorem OAI.KLInvariance.CoordinateProjection.restrict_surjective line 353
  27. theorem OAI.KLInvariance.CoordinateProjection.restrict_zero_iff line 358
  28. def OAI.KLInvariance.TitsSpace.BruhatUpper line 384
  29. def OAI.KLInvariance.TitsSpace.simpleUnion line 387
  30. def OAI.KLInvariance.TitsSpace.simpleInter line 388
  31. theorem OAI.KLInvariance.TitsSpace.BruhatUpper.mem_simpleUnion line 391
  32. theorem OAI.KLInvariance.TitsSpace.BruhatUpper.mem_simpleInter line 406
  33. theorem OAI.KLInvariance.TitsSpace.BruhatUpper.simpleUnion line 419
  34. theorem OAI.KLInvariance.TitsSpace.BruhatUpper.simpleInter line 427
  35. theorem OAI.KLInvariance.TitsSpace.simpleUnion_stable line 435
  36. theorem OAI.KLInvariance.TitsSpace.simpleInter_stable line 441
  37. theorem OAI.KLInvariance.TitsSpace.cross_edge_is_simple line 447
  38. def OAI.KLInvariance.TitsSpace.bottSetImage line 453
  39. instance OAI.KLInvariance.TitsSpace.bottSetImageAddCommGroup line 454
  40. instance OAI.KLInvariance.TitsSpace.bottSetImageModule line 456
  41. def OAI.KLInvariance.TitsSpace.bottSetProjection line 459
  42. def OAI.KLInvariance.TitsSpace.BottCompatible line 462
  43. def OAI.KLInvariance.TitsSpace.BottFlabby line 467
  44. def OAI.KLInvariance.TitsSpace.BottProjectiveUpper line 470
  45. def OAI.KLInvariance.ProjectiveRange.descend line 490
  46. theorem OAI.KLInvariance.ProjectiveRange.descend_apply line 494
  47. theorem OAI.KLInvariance.ProjectiveRange.projective_of_end line 500
  48. def OAI.KLInvariance.ProjectiveRange.kernelRetraction line 509
  49. theorem OAI.KLInvariance.ProjectiveRange.kernel_projective line 515
  50. def OAI.KLInvariance.ProjectiveRange.splitEquiv line 526
  51. theorem OAI.KLInvariance.ProjectiveRange.projective_of_kernel line 541
  52. theorem OAI.KLInvariance.ReflectionPairTranslation.tensorFirst_map line 562
  53. theorem OAI.KLInvariance.ReflectionPairTranslation.tensorSecond_map line 570
  54. theorem OAI.KLInvariance.injective_of_zero_lift line 595
  55. theorem OAI.KLInvariance.maps_eq_iff_of_zero_iff line 602
  56. theorem OAI.KLInvariance.functions_eq_of_surjective line 606
  57. def OAI.KLInvariance.TitsSpace.simplePull line 630
  58. theorem OAI.KLInvariance.TitsSpace.bottSetProjection_zero_iff line 632
  59. theorem OAI.KLInvariance.TitsSpace.bottSetProjection_surjective line 636
  60. theorem OAI.KLInvariance.TitsSpace.bottStalkProjection_zero_of_eq line 639
  61. theorem OAI.KLInvariance.TitsSpace.bottHeadSet_zero_iff line 645
  62. def OAI.KLInvariance.TitsSpace.bottSetFirst line 673
  63. def OAI.KLInvariance.TitsSpace.bottSetSecond line 679
  64. theorem OAI.KLInvariance.TitsSpace.bottSetFirst_project line 687
  65. theorem OAI.KLInvariance.TitsSpace.bottSetSecond_project line 691
  66. theorem OAI.KLInvariance.TitsSpace.bottSetComponents_injective line 696
  67. def OAI.KLInvariance.TitsSpace.bottTensorEnd line 707
  68. theorem OAI.KLInvariance.TitsSpace.bottTensorEnd_seed line 713
  69. theorem OAI.KLInvariance.TitsSpace.bottTensorEnd_first line 719
  70. theorem OAI.KLInvariance.TitsSpace.bottTensorEnd_second line 725
  71. theorem OAI.KLInvariance.TitsSpace.bottHead_components_injective line 732
  72. theorem OAI.KLInvariance.ReflectionPairTranslation.tensor_difference line 761
  73. theorem OAI.KLInvariance.PairProjection.cross_lift line 794
  74. theorem OAI.KLInvariance.TitsSpace.bottHead_difference line 821
  75. def OAI.KLInvariance.TitsSpace.bottHeadPatch line 827
  76. theorem OAI.KLInvariance.TitsSpace.bottHeadPatch_compatible line 833
  77. theorem OAI.KLInvariance.TitsSpace.bottHeadPatch_lift line 857
  78. def OAI.KLInvariance.TitsSpace.bottSetRestrict line 898
  79. theorem OAI.KLInvariance.TitsSpace.bottSetRestrict_project line 902
  80. theorem OAI.KLInvariance.TitsSpace.bottSetRestrict_surjective line 906
  81. theorem OAI.KLInvariance.TitsSpace.bottSetRestrict_zero_iff line 909
  82. def OAI.KLInvariance.TitsSpace.bottSeed line 913
  83. theorem OAI.KLInvariance.TitsSpace.bottSeed_first line 916
  84. theorem OAI.KLInvariance.TitsSpace.bottSeed_second line 919
  85. theorem OAI.KLInvariance.TitsSpace.bottSetFirst_seed line 922
  86. theorem OAI.KLInvariance.TitsSpace.bottSetSecond_seed line 928
  87. theorem OAI.KLInvariance.TitsSpace.bottSeed_zero_stable line 935
  88. theorem OAI.KLInvariance.TitsSpace.bottSetFirst_restrict line 948
  89. theorem OAI.KLInvariance.TitsSpace.bottSeed_zero_inter line 960
  90. theorem OAI.KLInvariance.projective_of_same_range line 992
  91. theorem OAI.KLInvariance.ReflectionPairTranslation.Twist.projective line 1001
  92. theorem OAI.KLInvariance.kernel_coordinate_injective line 1022
  93. theorem OAI.KLInvariance.common_kernel_coordinate_injective line 1030
  94. theorem OAI.KLInvariance.projective_of_coordinates line 1038
  95. theorem OAI.KLInvariance.ReflectionPairTranslation.twistMap_injective line 1052
  96. theorem OAI.KLInvariance.CoordinateProjection.restrict_joint_injective line 1062
  97. def OAI.KLInvariance.TitsSpace.bottInterRestriction line 1086
  98. def OAI.KLInvariance.TitsSpace.bottUnionRestriction line 1090
  99. def OAI.KLInvariance.TitsSpace.bottUnionPullRestriction line 1094
  100. def OAI.KLInvariance.TitsSpace.bottCommonKernel line 1099
  101. def OAI.KLInvariance.TitsSpace.bottCommonSecond line 1103
  102. theorem OAI.KLInvariance.TitsSpace.bottCommonSecond_injective line 1108
  103. def OAI.KLInvariance.TitsSpace.bottUnionKernelSecond line 1112
  104. theorem OAI.KLInvariance.TitsSpace.bottUnionKernelSecond_injective line 1117
  105. theorem OAI.KLInvariance.TitsSpace.bottHeadPatch_lift_of_zero_inter line 1123
  106. theorem OAI.KLInvariance.TitsSpace.bottCommon_lift line 1152
  107. theorem OAI.KLInvariance.TitsSpace.bottCommon_patch_lift line 1167
  108. theorem OAI.KLInvariance.TitsSpace.bottCommon_range_of_patch line 1182
  109. theorem OAI.KLInvariance.TitsSpace.bottCommon_range_of_lift line 1199
  110. theorem OAI.KLInvariance.TitsSpace.bottCommon_range_forward line 1212
  111. theorem OAI.KLInvariance.TitsSpace.bottCommon_range_backward line 1222
  112. theorem OAI.KLInvariance.TitsSpace.bottHeadLocalPair_eq_iff line 1258
  113. theorem OAI.KLInvariance.TitsSpace.bottTensorEnd_set_preserve line 1264
  114. theorem OAI.KLInvariance.TitsSpace.bottTensorEnd_set_kills line 1283
  115. theorem OAI.KLInvariance.TitsSpace.bottStableUpper_projective line 1299
  116. def OAI.KLInvariance.ProjectiveRange.onKernel line 1337
  117. def OAI.KLInvariance.ProjectiveRange.kernelOnKernelEquiv line 1340
  118. theorem OAI.KLInvariance.ProjectiveRange.projective_of_two_stage line 1349
  119. theorem OAI.KLInvariance.TitsSpace.bottInter_first_zero line 1373
  120. theorem OAI.KLInvariance.TitsSpace.bottInterKernelFirst_surjective line 1379
  121. theorem OAI.KLInvariance.TitsSpace.bottCommon_projective line 1392
  122. theorem OAI.KLInvariance.TitsSpace.bottProjectiveUpper_cons line 1408
  123. theorem OAI.KLInvariance.Realization.orthogonal_eq_id_or_rootReflection line 1439
  124. theorem OAI.KLInvariance.TitsSpace.reflection_character_congruence_iff line 1491
  125. theorem OAI.KLInvariance.TitsSpace.reflection_character_separates line 1547
  126. theorem OAI.KLInvariance.TitsSpace.isReflection_of_prime_character_congruence line 1572
  127. theorem OAI.KLInvariance.TitsSpace.prime_character_class line 1620
  128. def OAI.KLInvariance.FiniteCharacterLocalization.diagonal line 1664
  129. def OAI.KLInvariance.FiniteCharacterLocalization.stabilizer line 1669
  130. theorem OAI.KLInvariance.FiniteCharacterLocalization.diagonal_mem line 1694
  131. theorem OAI.KLInvariance.FiniteCharacterLocalization.uniform_projector line 1700

    Source documentation

    A polynomial in stable diagonal weights which kills the complement of C and is a common scalar on C. Its scalar is a product, not a quotient.

     theorem uniform_projector (L : Submodule R (∀ x, E x)) (C : Finset X)
    (f : X → R) (hf : f ∈ stabilizer L) (hz : ∀ x ∉ C, f x=0) :
    ∃ g ∈ stabilizer L,
      (∀ x ∈ C, g x=∏ y ∈ C, f y) ∧ (∀ x ∉ C, g x=0) := by
…

    Mentions: OAI.KLInvariance.FiniteCharacterLocalization.stabilizer

  132. theorem OAI.KLInvariance.FiniteCharacterLocalization.class_projector line 1730

    Source documentation

    Separate one residue-character class from its complement without inverting any element of the coefficient domain.

     theorem class_projector [Fintype X] (L : Submodule R (∀ x, E x)) (p : R) (hp : Prime p)
    (C : Finset X) (x : X)
    (test : X → X → R) (htest : ∀ y, test y ∈ stabilizer L)
    (hzero : ∀ y ∉ C, test y y=0)
    (hunit : ∀ y ∉ C, ¬ p ∣ test y x)
    (hcongr : ∀ z ∈ C, ∀ y, p ∣ test y z-test y x) :
    ∃ d : R, ¬ p ∣ d ∧ ∃ g ∈ stabilizer L,
      (∀ z ∈ C, g z=d) ∧ (∀ z ∉ C, g z=0) := by
…

    Mentions: OAI.KLInvariance.FiniteCharacterLocalization.stabilizer

  133. theorem OAI.KLInvariance.FiniteCharacterLocalization.partition_local_denominator line 1761

    Source documentation

    Local lifts on each finite character block assemble after a single scalar denominator away from the prime.

     theorem partition_local_denominator {Q : Type*} [Fintype Q]
    (L : Submodule R (∀ x, E x)) (p : R) (hp : Prime p) (q : X → Q)
    (z : ∀ x, E x) (d : Q → R) (hd : ∀ j, ¬ p ∣ d j)
    (g : Q → X → R) (hg : ∀ j, g j ∈ stabilizer L)
    (hgin : ∀ j x, q x=j → g j x=d j)
    (hgout : ∀ j x, q x≠j → g j x=0)
    (m : Q → ∀ x, E x) (hm : ∀ j, m j ∈ L)
    (hmatch : ∀ j x, q x=j → m j x=z x) :
    ∃ a : R, ¬ p ∣ a ∧ a • z ∈ L := by
…

    Mentions: OAI.KLInvariance.FiniteCharacterLocalization.stabilizer

  134. def OAI.KLInvariance.FiniteCharacterLocalization.residueSetoid line 1788
  135. theorem OAI.KLInvariance.FiniteCharacterLocalization.character_class_projector line 1794
  136. theorem OAI.KLInvariance.FiniteCharacterLocalization.character_local_denominator line 1833

    Source documentation

    Pair/blockwise liftability at a prime suffices for integral local membership in a finite character-stable lattice.

     theorem character_local_denominator [Fintype X] {A : Type*}
    (L : Submodule R (∀ x, E x)) (p : R) (hp : Prime p)
    (χ : A → X → R) (hχ : ∀ a, χ a ∈ stabilizer L) (z : ∀ x, E x)
    (hlift : ∀ x, ∃ m ∈ L, ∀ y, (residueSetoid p χ).r x y → m y=z y) :
    ∃ a : R, ¬ p ∣ a ∧ a • z ∈ L := by
…

    Mentions: OAI.KLInvariance.FiniteCharacterLocalization.stabilizer, OAI.KLInvariance.FiniteCharacterLocalization.residueSetoid

  137. theorem OAI.KLInvariance.ProjectiveLattice.finsupp_divide line 1870
  138. theorem OAI.KLInvariance.ProjectiveLattice.prime_divide_of_relation line 1886
  139. theorem OAI.KLInvariance.ProjectiveLattice.mem_of_prime_local_membership line 1904
  140. theorem OAI.KLInvariance.TitsSpace.bottSet_scaled line 1950
  141. theorem OAI.KLInvariance.TitsSpace.BottCompatible.reflection_lift line 1968
  142. theorem OAI.KLInvariance.TitsSpace.BottCompatible.prime_lift line 1982
  143. def OAI.KLInvariance.TitsSpace.BottUpperIndex line 2013
  144. def OAI.KLInvariance.TitsSpace.bottIndexSetEval line 2015
  145. theorem OAI.KLInvariance.TitsSpace.bottIndexSetEval_stable line 2020
  146. theorem OAI.KLInvariance.TitsSpace.BottCompatible.local_denominator line 2029
  147. theorem OAI.KLInvariance.TitsSpace.bottFlabby_of_projective line 2057
  148. theorem OAI.KLInvariance.TitsSpace.bottSetProjection_nil_injective line 2084
  149. theorem OAI.KLInvariance.TitsSpace.bottSetImage_nil_subsingleton line 2091
  150. theorem OAI.KLInvariance.TitsSpace.bottSetImage_nil_projective line 2101
  151. theorem OAI.KLInvariance.TitsSpace.bottProjectiveUpper line 2109
  152. theorem OAI.KLInvariance.TitsSpace.bottFlabby line 2114
  153. theorem OAI.KLInvariance.TitsSpace.bottStalk_subsingleton_of_not_bruhat line 2134
  154. def OAI.KLInvariance.TitsSpace.intervalUpperClosure line 2142
  155. theorem OAI.KLInvariance.TitsSpace.intervalUpperClosure_upper line 2146
  156. theorem OAI.KLInvariance.TitsSpace.intervalUpperClosure_member line 2152
  157. def OAI.KLInvariance.TitsSpace.bottIntervalExtension line 2158
  158. theorem OAI.KLInvariance.TitsSpace.bottIntervalExtension_apply line 2164
  159. theorem OAI.KLInvariance.TitsSpace.bottIntervalExtension_compatible line 2172
  160. theorem OAI.KLInvariance.TitsSpace.bottProjectionSheaf_flabby line 2192
  161. def OAI.PerfectAdjoint.adjoint line 2220
  162. theorem OAI.PerfectAdjoint.pairing line 2223
  163. theorem OAI.PerfectAdjoint.adjoint_comp line 2228
  164. theorem OAI.PerfectAdjoint.adjoint_idempotent line 2238
  165. theorem OAI.PerfectAdjoint.commutes_of_balanced line 2245
  166. theorem OAI.PerfectAdjoint.symmetric_pairing line 2253
  167. theorem OAI.PerfectAdjoint.adjoint_adjoint line 2257
  168. theorem OAI.KLInvariance.Graded.perfect_inverse_of_homogeneous_functional line 2285
  169. theorem OAI.KLInvariance.Graded.adjoint_homogeneous line 2340