OAI/RepresentationTheory/KazhdanLusztig/CharacterReciprocity.lean

GitHub source file

140 declarations, 0 contain sorry, 0 declared as axioms

Conditional boundary-sheaf duality and stalk-character propositions, free sheaves, actual R-reciprocity and lower convolution. StalkCharacterObligation remains a Prop, not an unconditional character theorem or a premise of the R-first route.

  1. def OAI.KLInvariance.BruhatGraph.SectionDualityObligation line 20
  2. theorem OAI.BalancedCuts.balanced_two line 49
  3. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.PerfectPairing.cut_balanced line 76
  4. theorem OAI.KLInvariance.BruhatGraph.sectionDualityObligation_of_perfectPairing line 106
  5. structure OAI.KLInvariance.BruhatGraph.FreeSheaf line 140
  6. def OAI.KLInvariance.BruhatGraph.FreeSheaf.kernelEquivSingleSupport line 150
  7. structure OAI.KLInvariance.BruhatGraph.FreeSheaf.SectionDuality line 170
  8. def OAI.KLInvariance.BruhatGraph.FreeSheaf.costalkEquivDual line 185
  9. theorem OAI.KLInvariance.BruhatGraph.FreeSheaf.costalk_free_of_duality line 197
  10. theorem OAI.KLInvariance.BruhatGraph.FreeSheaf.kernelEquivSingleSupport_apply line 206
  11. theorem OAI.KLInvariance.BruhatGraph.FreeSheaf.costalkEquivDual_inverse_homogeneous line 215
  12. def OAI.KLInvariance.BruhatGraph.FreeSheaf.fullSubmodule line 258
  13. theorem OAI.KLInvariance.BruhatGraph.FreeSheaf.fullKernel_eq line 263
  14. def OAI.KLInvariance.BruhatGraph.FreeSheaf.fullKernel line 270
  15. theorem OAI.KLInvariance.BruhatGraph.FreeSheaf.costalk_hilbert_of_duality line 275
  16. def OAI.KLInvariance.BruhatGraph.FreeSheaf.dualityOfPairing line 318
  17. instance OAI.KLInvariance.MomentGraph.Sheaf.zeroVertex_subsingleton line 346
  18. instance OAI.KLInvariance.MomentGraph.Sheaf.zeroEdge_subsingleton line 349
  19. structure OAI.KLInvariance.MomentGraph.Sheaf.LocalModels line 352
  20. inductive OAI.KLInvariance.MomentGraph.Sheaf.ModelSum line 364
  21. lemma OAI.KLInvariance.MomentGraph.Sheaf.ModelSum.mono line 375
  22. lemma OAI.KLInvariance.MomentGraph.Sheaf.ModelSum.free line 381
  23. lemma OAI.KLInvariance.MomentGraph.Sheaf.ModelSum.finite line 390
  24. lemma OAI.KLInvariance.MomentGraph.Sheaf.ModelSum.quotient line 399
  25. lemma OAI.KLInvariance.MomentGraph.Sheaf.ModelSum.generated line 406
  26. lemma OAI.KLInvariance.MomentGraph.Sheaf.ModelSum.flabby line 411
  27. lemma OAI.KLInvariance.MomentGraph.Sheaf.ModelSum.minimal line 416
  28. def OAI.KLInvariance.MomentGraph.Sheaf.ScaledImages line 443

    Source documentation

    Equality of embedded images with a scalar on the upper image.

    def ScaledImages (B : Sheaf.{ur,uv,ue,uz} (R := R) G) (e : E)
…
  29. theorem OAI.KLInvariance.MomentGraph.Sheaf.scaledImages_iff line 450
  30. theorem OAI.KLInvariance.MomentGraph.Sheaf.prod_upwardKernel_iff line 480
  31. theorem OAI.KLInvariance.MomentGraph.Sheaf.pi_upwardKernel_iff line 497
  32. theorem OAI.KLInvariance.MomentGraph.Sheaf.prod_scaledImages line 508
  33. theorem OAI.KLInvariance.MomentGraph.Sheaf.pi_scaledImages line 526
  34. theorem OAI.KLInvariance.MomentGraph.Sheaf.zero_scaledImages line 542
  35. theorem OAI.KLInvariance.MomentGraph.Sheaf.ModelSum.scaledImages line 548
  36. abbrev OAI.KLInvariance.MomentGraph.GradedSheaf.kernelData line 576
  37. def OAI.KLInvariance.MomentGraph.GradedSheaf.kernelProdEquiv line 579
  38. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.kernelProdEquiv_graded line 590
  39. def OAI.KLInvariance.MomentGraph.GradedSheaf.kernelPiEquiv line 594
  40. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.kernelPiEquiv_graded line 604
  41. def OAI.KLInvariance.MomentGraph.GradedSheaf.kernelShiftEquiv line 608
  42. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.kernelShiftEquiv_graded line 611
  43. def OAI.KLInvariance.MomentGraph.GradedSheaf.Iso.kernelEquiv line 615
  44. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.Iso.kernelEquiv_graded line 624
  45. instance OAI.KLInvariance.MomentGraph.GradedSheaf.kernelShiftFree line 643
  46. instance OAI.KLInvariance.MomentGraph.GradedSheaf.kernelProdFree line 648
  47. instance OAI.KLInvariance.MomentGraph.GradedSheaf.kernelPiFree line 654
  48. instance OAI.KLInvariance.MomentGraph.GradedSheaf.kernelZeroFree line 660
  49. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.kernelChar_shift line 666
  50. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.kernelChar_prod line 673
  51. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.kernelChar_pi line 681
  52. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.kernelChar_zero line 688
  53. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.ModelSum.kernelFree line 694
  54. def OAI.KLInvariance.MomentGraph.GradedSheaf.freeKernelChar line 705
  55. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.ModelSum.character_both line 710
  56. def OAI.KLInvariance.MomentGraph.GradedSheaf.kernelEquivFull line 787
  57. def OAI.KLInvariance.BruhatGraph.FreeSheaf.kernelDual line 808
  58. theorem OAI.KLInvariance.BruhatGraph.FreeSheaf.kernel_free line 814
  59. theorem OAI.KLInvariance.BruhatGraph.FreeSheaf.kernelDual_homogeneous line 819
  60. theorem OAI.KLInvariance.BruhatGraph.FreeSheaf.kernel_character line 836
  61. theorem OAI.KLInvariance.TitsSpace.bottSection_left_orthogonal line 866
  62. theorem OAI.KLInvariance.TitsSpace.bottSection_right_orthogonal line 876
  63. def OAI.KLInvariance.TitsSpace.bottWordPerfectPairing line 884
  64. def OAI.KLInvariance.TitsSpace.bottPolynomialPerfectPairing line 892
  65. def OAI.KLInvariance.TitsSpace.bottFreeSheaf line 897
  66. def OAI.KLInvariance.TitsSpace.bottFreeDuality line 906
  67. theorem OAI.KLInvariance.TitsSpace.bottKernelFree line 910
  68. theorem OAI.KLInvariance.TitsSpace.bottKernelCharacter line 915
  69. theorem OAI.KLInvariance.HeckeQ.one_add_leftInv line 944
  70. theorem OAI.KLInvariance.HeckeQ.barLinear_positiveWord line 951
  71. theorem OAI.KLInvariance.HeckeQ.positiveWord_support line 963
  72. theorem OAI.KLInvariance.HeckeQ.positiveWord_rValue line 997
  73. theorem OAI.KLInvariance.HeckeQ.eval_positiveWord line 1027
  74. theorem OAI.KLInvariance.Graded.ModuleData.char_natDegree_le_of_dual_equiv line 1053
  75. theorem OAI.KLInvariance.TitsSpace.bottStalkCharacter_natDegree_le line 1088
  76. theorem OAI.KLInvariance.TitsSpace.bottStalkCharacter_reciprocity line 1105
  77. theorem OAI.KLInvariance.TitsSpace.bottKernelCharacter_rConvolution line 1134
  78. theorem OAI.KLInvariance.MomentGraph.BoundarySheaf.top_nontrivial line 1166
  79. theorem OAI.KLInvariance.MomentGraph.BoundarySheaf.iso_of_primitive_top_split line 1176
  80. def OAI.KLInvariance.TitsSpace.bottSplitAdjointSplit line 1213
  81. theorem OAI.KLInvariance.TitsSpace.bottSplitAdjoint_free line 1221
  82. def OAI.KLInvariance.TitsSpace.bottSplitAdjointTopInclusion line 1231
  83. def OAI.KLInvariance.TitsSpace.bottSplitAdjointTopProjection line 1238
  84. theorem OAI.KLInvariance.TitsSpace.bottSplitAdjointTop_split line 1245
  85. theorem OAI.KLInvariance.TitsSpace.bottBoundarySheaf_iso_adjoint line 1258
  86. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.imageSectionEquiv_symm_coordinates line 1294
  87. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.imageSectionEquiv_symm_inclusion line 1302
  88. def OAI.KLInvariance.TitsSpace.bottSplitRightWord line 1331
  89. def OAI.KLInvariance.TitsSpace.bottSplitLeftWord line 1336
  90. theorem OAI.KLInvariance.TitsSpace.bottSplitRightWord_coordinates line 1343
  91. theorem OAI.KLInvariance.TitsSpace.bottSplitLeftWord_coordinates line 1352
  92. theorem OAI.KLInvariance.TitsSpace.bottSplitAdjointWord_apply line 1361
  93. def OAI.KLInvariance.TitsSpace.bottRecognizedPerfectPairing line 1393
  94. theorem OAI.KLInvariance.TitsSpace.symmetric_scalar_mod_positive line 1443
  95. theorem OAI.KLInvariance.TitsSpace.symmetricLabel_homogeneous line 1457
  96. theorem OAI.KLInvariance.TitsSpace.exists_symmetricBoundarySheaf line 1461
  97. def OAI.KLInvariance.TitsSpace.symmetricBoundarySheaf line 1474
  98. theorem OAI.KLInvariance.TitsSpace.symmetricBoundarySheaf_perfectPairing_word line 1497
  99. theorem OAI.KLInvariance.TitsSpace.symmetricBoundarySheaf_perfectPairing line 1508
  100. def OAI.KLInvariance.Graded.ModuleData.changeUnitHom line 1533
  101. def OAI.KLInvariance.Graded.ModuleData.changeUnitInvHom line 1545
  102. theorem OAI.KLInvariance.Graded.ModuleData.changeUnitHom_inv line 1562
  103. theorem OAI.KLInvariance.Graded.ModuleData.changeUnitInvHom_hom line 1566
  104. def OAI.KLInvariance.Graded.ModuleData.unchangeHom line 1586
  105. def OAI.KLInvariance.MomentGraph.GradedSheaf.Hom.coefficientUnchange line 1612
  106. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.coefficientChange_primitive line 1619
  107. def OAI.KLInvariance.Graded.ModuleData.changeTopInclusion line 1675
  108. def OAI.KLInvariance.Graded.ModuleData.changeTopProjection line 1679
  109. theorem OAI.KLInvariance.Graded.ModuleData.changeTop_split line 1683
  110. theorem OAI.KLInvariance.MomentGraph.BoundarySheaf.iso_coefficientChange line 1709
  111. theorem OAI.KLInvariance.BruhatGraph.boundarySheaf_perfectPairing line 1740
  112. theorem OAI.KLInvariance.BruhatGraph.sectionDualityObligation line 1759
  113. def OAI.KLInvariance.BruhatGraph.boundaryFreeSheaf line 1786
  114. def OAI.KLInvariance.BruhatGraph.boundaryPerfectPairing line 1792
  115. def OAI.KLInvariance.BruhatGraph.boundaryFreeDuality line 1796
  116. theorem OAI.KLInvariance.BruhatGraph.boundaryKernelFree line 1799
  117. def OAI.KLInvariance.BruhatGraph.costalkCharacter line 1804
  118. theorem OAI.KLInvariance.BruhatGraph.costalkCharacter_reflect line 1807
  119. theorem OAI.KLInvariance.BruhatGraph.stalkBasis_degree_le line 1815
  120. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.lowerExtend_kernel_iff line 1847
  121. def OAI.KLInvariance.MomentGraph.GradedSheaf.lowerExtendKernelEquiv line 1867
  122. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.lowerExtendKernelEquiv_graded line 1877
  123. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.fullKernel_pullback line 1884
  124. def OAI.KLInvariance.MomentGraph.GradedSheaf.pullbackKernelEquiv line 1890
  125. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.pullbackKernelEquiv_graded line 1900
  126. def OAI.KLInvariance.BruhatGraph.lowerKernelEquiv line 1922
  127. theorem OAI.KLInvariance.BruhatGraph.lowerKernelEquiv_graded line 1929
  128. theorem OAI.KLInvariance.BruhatGraph.boundaryModels_kernelFree line 1936
  129. theorem OAI.KLInvariance.BruhatGraph.boundaryModels_kernelCharacter line 1947
  130. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.exists_character_decomposition line 1978
  131. theorem OAI.KLInvariance.TitsSpace.bottCharacter_decomposition_both line 2019
  132. def OAI.KLInvariance.Graded.ModuleData.unitPolynomialBasis line 2055
  133. theorem OAI.KLInvariance.Graded.ModuleData.char_unit line 2068
  134. theorem OAI.KLInvariance.BruhatGraph.stalkCharacter_top line 2091
  135. theorem OAI.KLInvariance.BruhatGraph.lowerCharacter_diagonal line 2099
  136. theorem OAI.KLInvariance.BruhatGraph.lowerCharacter_at_top line 2103
  137. def OAI.KLInvariance.BruhatGraph.lowerIntervalEquiv line 2134
  138. theorem OAI.KLInvariance.BruhatGraph.lowerCharacter_convolution line 2140
  139. theorem OAI.KLInvariance.BruhatGraph.lowerCharacter_convolution_zero line 2166
  140. theorem OAI.KLInvariance.BruhatGraph.lowerCharacter_reciprocity_lift line 2174