OAI/RepresentationTheory/KazhdanLusztig/BalancedPairings.lean

GitHub source file

158 declarations, 0 contain sorry, 0 declared as axioms

Graded stalk duality, integral perfect balanced all-sections pairings, recognition and top grading.

  1. theorem OAI.KLInvariance.TitsSpace.bottPairing_dualToSupport line 19
  2. theorem OAI.KLInvariance.TitsSpace.bottStalkDuality_apply_projection line 29
  3. theorem OAI.KLInvariance.TitsSpace.bottStalkDuality_homogeneous line 42
  4. theorem OAI.KLInvariance.TitsSpace.bottDualToSupport_homogeneous line 50
  5. theorem OAI.KLInvariance.TitsSpace.bottStalkDuality_homogeneous_iff line 63
  6. theorem OAI.KLInvariance.TitsSpace.bott_projection_zero_iff_annihilates_support line 101
  7. def OAI.KLInvariance.TitsSpace.bottAdjoint line 118
  8. theorem OAI.KLInvariance.TitsSpace.bottAdjoint_preserves_kernel line 121
  9. theorem OAI.KLInvariance.TitsSpace.bottAdjoint_preserves_support line 133
  10. theorem OAI.KLInvariance.TitsSpace.bottAdjoint_homogeneous line 146
  11. def OAI.KLInvariance.TitsSpace.bottVertexProjection line 174
  12. theorem OAI.KLInvariance.TitsSpace.bottVertexProjection_injective line 179
  13. theorem OAI.KLInvariance.TitsSpace.bottVertexProjection_stable line 185
  14. theorem OAI.KLInvariance.TitsSpace.bottVertexProjection_scaled line 194
  15. theorem OAI.KLInvariance.TitsSpace.bottSection_pair_lift line 212
  16. theorem OAI.KLInvariance.TitsSpace.bottSection_prime_lift line 231
  17. theorem OAI.KLInvariance.TitsSpace.bottSection_local_denominator line 262
  18. theorem OAI.KLInvariance.TitsSpace.bottSection_surjective line 277
  19. def OAI.KLInvariance.TitsSpace.bottSectionEquiv line 292
  20. theorem OAI.TransportPerfectPairing.balanced line 311
  21. theorem OAI.TransportPerfectPairing.symmetric line 322
  22. def OAI.KLInvariance.TitsSpace.bottSectionDuality line 346
  23. theorem OAI.KLInvariance.TitsSpace.bottSectionDuality_apply line 354
  24. def OAI.KLInvariance.TitsSpace.bottSectionRight line 363
  25. theorem OAI.KLInvariance.TitsSpace.bottSectionRight_apply line 370
  26. theorem OAI.KLInvariance.TitsSpace.bottSectionRight_coordinates line 379
  27. theorem OAI.KLInvariance.TitsSpace.bottSection_balanced line 388
  28. theorem OAI.KLInvariance.TitsSpace.bottSection_symmetric line 397
  29. theorem OAI.KLInvariance.TitsSpace.bottPiece_iff_stalks line 422
  30. theorem OAI.KLInvariance.TitsSpace.bottSectionDuality_homogeneous line 443
  31. def OAI.KLInvariance.MomentGraph.GradedSheaf.Hom.assignmentMap line 474
  32. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.Hom.assignmentMap_compatible line 479
  33. def OAI.KLInvariance.MomentGraph.GradedSheaf.Hom.sectionMap line 488
  34. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.Hom.sectionMap_apply line 493
  35. def OAI.KLInvariance.MomentGraph.GradedSheaf.Hom.gradedSectionMap line 499
  36. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.sections_split line 507
  37. def OAI.KLInvariance.TitsSpace.bottEndOfSheaf line 533
  38. theorem OAI.KLInvariance.TitsSpace.bottEndOfSheaf_coordinates line 540
  39. theorem OAI.KLInvariance.TitsSpace.bottEndOfSheaf_homogeneous line 551
  40. theorem OAI.KLInvariance.TitsSpace.bottEndOfSheaf_preserves_kernel line 561
  41. theorem OAI.KLInvariance.TitsSpace.bottEndOfSheaf_preserves_support line 570
  42. def OAI.LinearDescent.descend line 603
  43. theorem OAI.LinearDescent.descend_apply line 607
  44. theorem OAI.LinearDescent.descend_idempotent line 613
  45. def OAI.KLInvariance.Graded.ModuleData.descended line 637
  46. theorem OAI.KLInvariance.Graded.ModuleData.lower_kernel_preserved line 646
  47. def OAI.KLInvariance.Graded.ModuleData.descendedEdge line 654
  48. theorem OAI.KLInvariance.Graded.ModuleData.descendedEdge_lower line 664
  49. theorem OAI.KLInvariance.Graded.ModuleData.descendedEdge_upper line 669
  50. def OAI.KLInvariance.TitsSpace.bottAdjointWordHom line 700
  51. theorem OAI.KLInvariance.TitsSpace.bottAdjointWordHom_kernel line 708
  52. def OAI.KLInvariance.TitsSpace.bottAdjointSheaf line 717
  53. theorem OAI.KLInvariance.TitsSpace.bottAdjointSheaf_vertex line 735
  54. theorem OAI.KLInvariance.TitsSpace.bottEndOfAdjointSheaf line 743
  55. theorem OAI.KLInvariance.TitsSpace.bottEndOfSheaf_idempotent line 778
  56. theorem OAI.KLInvariance.TitsSpace.bottAdjointSheaf_vertex_idempotent line 789
  57. theorem OAI.KLInvariance.TitsSpace.bottAdjointSheaf_edge_idempotent line 802
  58. theorem OAI.KLInvariance.TitsSpace.bottAdjointSheaf_twice_vertex line 817
  59. def OAI.KLInvariance.Graded.ModuleData.rangeMap line 846
  60. def OAI.KLInvariance.Graded.ModuleData.rangeInclusion line 853
  61. def OAI.KLInvariance.Graded.ModuleData.rangeProjection line 857
  62. def OAI.KLInvariance.MomentGraph.GradedSheaf.Hom.image line 873
  63. def OAI.KLInvariance.MomentGraph.GradedSheaf.Hom.imageInclusion line 879
  64. def OAI.KLInvariance.MomentGraph.GradedSheaf.Hom.imageProjection line 885
  65. def OAI.KLInvariance.MomentGraph.GradedSheaf.Hom.imageSplit line 891
  66. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.Hom.imageSection_fixed line 927
  67. def OAI.KLInvariance.MomentGraph.GradedSheaf.Hom.imageSectionMap line 937
  68. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.Hom.imageSectionMap_bijective line 943
  69. def OAI.KLInvariance.MomentGraph.GradedSheaf.Hom.imageSectionEquiv line 958
  70. def OAI.ConjugateRange.conjugate line 980
  71. def OAI.ConjugateRange.map line 982
  72. theorem OAI.ConjugateRange.map_bijective line 989
  73. def OAI.ConjugateRange.equiv line 999
  74. theorem OAI.ConjugateRange.equiv_apply line 1002
  75. def OAI.AdjointSummandDuality.dualSection line 1025
  76. def OAI.AdjointSummandDuality.dualProjection line 1028
  77. theorem OAI.AdjointSummandDuality.projection_section line 1031
  78. def OAI.AdjointSummandDuality.adjointProjector line 1040
  79. theorem OAI.AdjointSummandDuality.adjointProjector_idempotent line 1043
  80. def OAI.AdjointSummandDuality.adjointSummand line 1049
  81. theorem OAI.AdjointSummandDuality.dualProjection_injective_on_adjoint line 1052
  82. theorem OAI.AdjointSummandDuality.dualProjection_surjective_on_adjoint line 1062
  83. def OAI.AdjointSummandDuality.adjointEquivDual line 1067
  84. theorem OAI.AdjointSummandDuality.adjointEquivDual_apply line 1071
  85. theorem OAI.AdjointSummandDuality.adjointProjector_range line 1075
  86. theorem OAI.AdjointSummandDuality.projection_intertwines line 1090
  87. theorem OAI.AdjointSummandDuality.section_intertwines line 1098
  88. theorem OAI.AdjointSummandDuality.adjointProjector_commutes line 1110
  89. theorem OAI.PerfectAdjoint.adjoint_projector_eq line 1136
  90. def OAI.PerfectAdjoint.rangeAdjointEquivDual line 1142
  91. theorem OAI.PerfectAdjoint.rangeAdjointEquivDual_apply line 1147
  92. theorem OAI.PerfectAdjoint.range_projector_split line 1167
  93. def OAI.PerfectAdjoint.rangeAdjointEquivDualRange line 1173
  94. theorem OAI.PerfectAdjoint.rangeAdjointEquivDualRange_apply line 1176
  95. theorem OAI.KLInvariance.TitsSpace.symmetricCoefficientNoetherian line 1194
  96. def OAI.KLInvariance.TitsSpace.bottImageSheaf line 1221
  97. def OAI.KLInvariance.TitsSpace.bottImageSectionWordEquiv line 1226
  98. def OAI.KLInvariance.TitsSpace.bottAdjointImageEquivDual line 1234
  99. theorem OAI.KLInvariance.TitsSpace.bottImageSectionWordEquiv_coordinates line 1249
  100. theorem OAI.KLInvariance.TitsSpace.bottImageSectionWordEquiv_homogeneous line 1260
  101. theorem OAI.KLInvariance.TitsSpace.bottAdjointImageEquivDual_apply line 1270
  102. theorem OAI.KLInvariance.TitsSpace.bottAdjointImagePairing_homogeneous line 1279
  103. def OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.projector line 1314
  104. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.projector_vertex line 1317
  105. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.projector_edge line 1325
  106. def OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.imageTo line 1332
  107. def OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.toImage line 1333
  108. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.imageTo_toImage_vertex line 1335
  109. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.toImage_imageTo_vertex line 1341
  110. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.imageTo_toImage_edge line 1348
  111. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.toImage_imageTo_edge line 1354
  112. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.imageSection_bijective line 1361
  113. def OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.imageSectionEquiv line 1377
  114. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.imageSectionEquiv_symm_apply line 1381
  115. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.imageSectionEquiv_symm_homogeneous line 1389
  116. def OAI.KLInvariance.TitsSpace.bottSplitAdjointSheaf line 1417
  117. def OAI.KLInvariance.TitsSpace.bottSplitAdjointEquivDual line 1421
  118. theorem OAI.KLInvariance.TitsSpace.bottSplitAdjointPairing_homogeneous line 1429
  119. theorem OAI.KLInvariance.TitsSpace.bottEndOfSheaf_fixed_support line 1466
  120. theorem OAI.KLInvariance.TitsSpace.bottAdjointSheaf_fixed_stalk line 1478
  121. theorem OAI.KLInvariance.TitsSpace.bottAdjointSheaf_fixed_stalk_iff line 1495
  122. theorem OAI.KLInvariance.Graded.ModuleData.Hom.eq_of_map_eq line 1517
  123. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.Hom.eq_of_maps line 1531
  124. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.Hom.eq_of_vertex line 1544
  125. theorem OAI.KLInvariance.TitsSpace.bottEndOfSheaf_comp line 1571
  126. theorem OAI.KLInvariance.TitsSpace.bottAdjointSheaf_comp line 1585
  127. theorem OAI.KLInvariance.TitsSpace.bottAdjointSheaf_involutive line 1610
  128. theorem OAI.KLInvariance.TitsSpace.bottAdjointSheaf_injective line 1616
  129. def OAI.KLInvariance.MomentGraph.GradedSheaf.Hom.zero line 1636
  130. def OAI.KLInvariance.MomentGraph.GradedSheaf.Hom.id line 1642
  131. def OAI.KLInvariance.MomentGraph.GradedSheaf.Hom.PrimitiveProjector line 1648
  132. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.Hom.primitive_of_antiInvolution line 1652
  133. theorem OAI.PerfectAdjoint.adjoint_zero line 1691
  134. theorem OAI.KLInvariance.TitsSpace.bottEndOfSheaf_zero line 1710
  135. theorem OAI.KLInvariance.TitsSpace.bottAdjointSheaf_zero line 1720
  136. theorem OAI.KLInvariance.TitsSpace.bottAdjointSheaf_primitive line 1736
  137. theorem OAI.KLInvariance.TitsSpace.bottAdjointSheaf_primitive_iff line 1747
  138. def OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.liftEnd line 1778
  139. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.liftEnd_injective line 1781
  140. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.liftEnd_comp line 1801
  141. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.liftEnd_zero line 1817
  142. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.primitive_id_of_projector line 1826
  143. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.projector_eq_id_of_primitive line 1845
  144. def OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.isoOfProjectorEqId line 1868
  145. def OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.isoOfPrimitive line 1884
  146. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.Hom.primitive_image line 1891
  147. def OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.downEnd line 1925
  148. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.lift_down line 1928
  149. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.downEnd_idempotent line 1935
  150. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.primitive_projector_of_id line 1942
  151. theorem OAI.KLInvariance.MomentGraph.BoundarySheaf.primitive_identity line 1974
  152. theorem OAI.KLInvariance.MomentGraph.BoundarySheaf.split_projector_primitive line 1996
  153. theorem OAI.KLInvariance.TitsSpace.bottBoundarySplitAdjoint_primitive line 2025
  154. theorem OAI.KLInvariance.TitsSpace.bottTopStalkEquiv_homogeneous_iff line 2053
  155. def OAI.KLInvariance.TitsSpace.bottTopHom line 2066
  156. def OAI.KLInvariance.TitsSpace.bottTopInvHom line 2075
  157. theorem OAI.KLInvariance.TitsSpace.bottTopHom_inv line 2087
  158. theorem OAI.KLInvariance.TitsSpace.bottTopInvHom_top line 2093