OAI/RepresentationTheory/KazhdanLusztig/SheafMorphisms.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

Graded sheaf morphisms, exact section constructions and character sums.

  1. structure OAI.KLInvariance.Graded.NonnegativeBasis line 20
  2. theorem OAI.KLInvariance.Graded.exists_nonnegativeBasis line 29
  3. def OAI.KLInvariance.Graded.NonnegativeBasis.polynomial line 47
  4. lemma OAI.KLInvariance.Graded.NonnegativeBasis.coeff_nonneg line 51
  5. lemma OAI.KLInvariance.Graded.NonnegativeBasis.eval₂_eq line 58
  6. lemma OAI.KLInvariance.Graded.NonnegativeBasis.hasSum line 64
  7. lemma OAI.KLInvariance.Graded.NonnegativeBasis.polynomial_eq line 72
  8. def OAI.KLInvariance.Graded.character line 89
  9. lemma OAI.KLInvariance.Graded.character_coeff_nonneg line 93
  10. lemma OAI.KLInvariance.Graded.character_eq line 98
  11. theorem OAI.KLInvariance.Graded.polynomial_scalar_mod_positive line 114
  12. abbrev OAI.KLInvariance.BruhatGraph.Coefficient line 139
  13. def OAI.KLInvariance.BruhatGraph.root line 141
  14. def OAI.KLInvariance.BruhatGraph.polynomialLabel line 144
  15. theorem OAI.KLInvariance.BruhatGraph.polynomialLabel_homogeneous line 148
  16. theorem OAI.KLInvariance.BruhatGraph.polynomialLabel_ne_zero line 160
  17. theorem OAI.KLInvariance.BruhatGraph.exists_boundarySheaf line 172
  18. def OAI.KLInvariance.BruhatGraph.boundarySheaf line 202
  19. def OAI.KLInvariance.BruhatGraph.stalkCharacter line 206
  20. theorem OAI.KLInvariance.BruhatGraph.stalkCharacter_coeff_nonneg line 211
  21. def OAI.KLInvariance.BruhatGraph.StalkCharacterObligation line 219
  22. def OAI.KLInvariance.BruhatGraph.CostalkFreeObligation line 223
  23. theorem OAI.KLInvariance.simple_mul_bruhat_of_descent line 243
  24. theorem OAI.KLInvariance.lower_parity_balance line 252
  25. def OAI.KLInvariance.externalLower line 275
  26. theorem OAI.KLInvariance.mem_externalLower line 279
  27. theorem OAI.KLInvariance.one_bruhat line 284
  28. theorem OAI.KLInvariance.external_parity_card_le line 288
  29. abbrev OAI.KLInvariance.BruhatGraph.lowerIdealGraph line 345
  30. def OAI.KLInvariance.BruhatGraph.lowerIntervalMap line 348
  31. theorem OAI.KLInvariance.BruhatGraph.lowerIntervalMap_injective line 358
  32. theorem OAI.KLInvariance.BruhatGraph.lowerIntervalMap_outgoing line 365
  33. def OAI.KLInvariance.BruhatGraph.lowerIntervalBoundary line 378
  34. def OAI.KLInvariance.BruhatGraph.boundaryModels line 385
  35. theorem OAI.KLInvariance.Graded.basis_coordinates_graded line 422
  36. theorem OAI.KLInvariance.Graded.ModuleData.exists_equiv_shiftedUnits line 457
  37. def OAI.KLInvariance.QuotientEdge.descend line 509
  38. theorem OAI.KLInvariance.QuotientEdge.descend_apply line 514
  39. theorem OAI.KLInvariance.QuotientEdge.kernel_scalar_le line 520
  40. def OAI.KLInvariance.Graded.ModuleData.quotientHom line 539
  41. theorem OAI.KLInvariance.Graded.ModuleData.quotientHom_apply line 549
  42. structure OAI.KLInvariance.MomentGraph.GradedSheaf.Hom line 570
  43. structure OAI.KLInvariance.MomentGraph.GradedSheaf.OnHom line 578
  44. def OAI.KLInvariance.MomentGraph.GradedSheaf.Hom.comp line 591
  45. def OAI.KLInvariance.MomentGraph.GradedSheaf.OnHom.ofUniv line 607
  46. def OAI.KLInvariance.MomentGraph.GradedSheaf.OnHom.mapAssignment line 613
  47. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.OnHom.mapAssignment_at line 618
  48. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.OnHom.compatible line 625
  49. def OAI.KLInvariance.MomentGraph.GradedSheaf.OnHom.boundary line 639
  50. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.OnHom.boundaryMap line 648
  51. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.OnHom.map_stalk_image_le line 658
  52. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.OnHom.extend_stalk line 675
  53. def OAI.KLInvariance.MomentGraph.GradedSheaf.castVertexHom line 715
  54. def OAI.KLInvariance.MomentGraph.GradedSheaf.OnHom.extend line 723
  55. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.OnHom.extend_vertex_old line 770
  56. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.OnHom.extend_vertex_new line 784
  57. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.OnHom.cast_vertex line 827
  58. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.OnHom.exists_extension line 834
  59. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.exists_hom_top line 917
  60. theorem OAI.KLInvariance.Graded.ModuleData.idempotent_eq_zero line 961
  61. structure OAI.KLInvariance.MomentGraph.GradedSheaf.Endomorphism line 996
  62. def OAI.KLInvariance.MomentGraph.GradedSheaf.Endomorphism.complement line 1007
  63. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.Endomorphism.complement_idempotent line 1023
  64. theorem OAI.KLInvariance.Graded.ModuleData.unit_idempotent_trivial line 1040
  65. theorem OAI.KLInvariance.MomentGraph.BoundarySheaf.idempotent_zero_of_top_zero line 1087
  66. theorem OAI.KLInvariance.MomentGraph.BoundarySheaf.idempotent_trivial line 1124

    Source documentation

    Actual indecomposability in the idempotent formulation. A direct sum splitting supplies such a homogeneous idempotent, hence one summand vanishes.

     theorem idempotent_trivial [Finite V] [IsDomain A]
    (f : B.sheaf.Endomorphism)
    (hi : ∀ x v, (f.vertex x).map ((f.vertex x).map v) = (f.vertex x).map v) :
    ((∀ x, (f.vertex x).map = 0) ∧ (∀ e, (f.edge e).map = 0)) ∨
      ((∀ x, (f.vertex x).map = LinearMap.id) ∧
        (∀ e, (f.edge e).map = LinearMap.id)) := by
…
  67. theorem OAI.KLInvariance.Graded.ModuleData.MinimalCover.bijective_of_boundaryIso line 1171
  68. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.Endomorphism.edge_bijective_of_vertex line 1220
  69. theorem OAI.KLInvariance.MomentGraph.BoundarySheaf.endomorphism_bijective_of_top line 1252
  70. def OAI.KLInvariance.Graded.ModuleData.Hom.inverse line 1312
  71. theorem OAI.KLInvariance.Graded.ModuleData.Hom.map_inverse line 1320
  72. theorem OAI.KLInvariance.Graded.ModuleData.Hom.inverse_map line 1323
  73. def OAI.KLInvariance.MomentGraph.GradedSheaf.Hom.toEndomorphism line 1337
  74. def OAI.KLInvariance.MomentGraph.GradedSheaf.Hom.inverse line 1340
  75. structure OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn line 1354
  76. theorem OAI.KLInvariance.MomentGraph.BoundarySheaf.splitIn_of_top_split line 1380
  77. theorem OAI.KLInvariance.Graded.ModuleData.exists_minimalCover_split line 1427
  78. def OAI.KLInvariance.Graded.ModuleData.Hom.splitEquiv line 1445
  79. theorem OAI.KLInvariance.Graded.ModuleData.Hom.splitEquiv_graded line 1450
  80. theorem OAI.KLInvariance.Graded.ModuleData.Hom.kernel_free_of_split line 1459
  81. theorem OAI.KLInvariance.MomentGraph.Sheaf.AboveIso.split_stalk_graded line 1496
  82. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.extend_modelSum line 1567
  83. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.exists_modelSumIso line 1642

    Source documentation

    Finite graded decomposition with actual nonnegative shifts.

    theorem exists_modelSumIso [Finite V]
    (hBfree : ∀ x, Module.Free A (B.vertex x))
    (hBq : B.UpperQuotient α) (hBf : B.forget.Flabby) (hBg : B.forget.Generated) :
    ∃ C : GradedSheaf (𝓐 := 𝓐) G,
…

    Mentions: OAI.KLInvariance.MomentGraph.GradedSheaf

  84. def OAI.KLInvariance.Graded.ModuleData.mapNonnegativeBasis line 1708
  85. theorem OAI.KLInvariance.Graded.ModuleData.character_eq_of_gradedEquiv line 1717
  86. abbrev OAI.KLInvariance.Graded.ModuleData.char line 1742
  87. def OAI.KLInvariance.Graded.ModuleData.shiftedBasis line 1745
  88. instance OAI.KLInvariance.Graded.ModuleData.shift_free line 1755
  89. theorem OAI.KLInvariance.Graded.ModuleData.char_shift line 1758
  90. def OAI.KLInvariance.Graded.ModuleData.productBasis line 1765
  91. instance OAI.KLInvariance.Graded.ModuleData.prod_free line 1785
  92. theorem OAI.KLInvariance.Graded.ModuleData.char_prod line 1789
  93. def OAI.KLInvariance.Graded.ModuleData.piBasis line 1799
  94. instance OAI.KLInvariance.Graded.ModuleData.pi_free line 1817
  95. theorem OAI.KLInvariance.Graded.ModuleData.char_pi line 1823
  96. theorem OAI.KLInvariance.Graded.ModuleData.char_zero line 1835