OAI/RepresentationTheory/KazhdanLusztig/Support.lean

GitHub source file

119 declarations, 0 contain sorry, 0 declared as axioms

Graded unit splittings, integral support and balanced cuts, and boundary-sheaf support and recognition.

  1. theorem OAI.KLInvariance.Graded.ModuleData.unit_endomorphisms_commute line 18
  2. theorem OAI.KLInvariance.Graded.ModuleData.unit_split_reverse line 39
  3. theorem OAI.KLInvariance.Graded.ModuleData.split_reverse_of_unit line 44
  4. theorem OAI.KLInvariance.TitsSpace.bottBoundarySplit_top_fixed line 85
  5. theorem OAI.KLInvariance.TitsSpace.bottBoundarySplitAdjoint_top_fixed line 94
  6. theorem OAI.KLInvariance.TitsSpace.symmetricGrading_zero line 117
  7. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.flabby line 144
  8. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.generated line 155
  9. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.upperQuotient line 164
  10. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.vertex_projective line 194
  11. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.vertex_free line 200
  12. theorem OAI.KLInvariance.Graded.ModuleData.equivOfEq_inverse line 225
  13. def OAI.KLInvariance.Graded.ModuleData.homOfEq line 230
  14. def OAI.KLInvariance.TitsSpace.symmetricLabel line 250
  15. theorem OAI.KLInvariance.TitsSpace.symmetricLabel_represents line 253
  16. theorem OAI.KLInvariance.TitsSpace.bottGradedProjectionSheaf_upperQuotient line 257
  17. def OAI.KLInvariance.TitsSpace.bottBoundarySheafTopInclusion line 263
  18. def OAI.KLInvariance.TitsSpace.bottBoundarySheafTopProjection line 272
  19. theorem OAI.KLInvariance.TitsSpace.bottBoundarySheafTop_split line 281
  20. theorem OAI.KLInvariance.TitsSpace.bottBoundarySheaf_splitIn line 293
  21. def OAI.KLInvariance.MomentGraph.GradedSheaf.coefficientChange line 329
  22. def OAI.KLInvariance.MomentGraph.GradedSheaf.Hom.coefficientChange line 335
  23. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.coefficientChange_free line 342
  24. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.coefficientChange_upperQuotient line 348
  25. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.coefficientChange_flabby line 368
  26. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.coefficientChange_generated line 380
  27. def OAI.KLInvariance.MomentGraph.GradedSheaf.coefficientChangeSections line 388
  28. def OAI.KLInvariance.TitsSpace.bottPolynomialSheaf line 417
  29. theorem OAI.KLInvariance.TitsSpace.bottPolynomialSheaf_free line 422
  30. theorem OAI.KLInvariance.TitsSpace.bottPolynomialSheaf_quotient line 426
  31. theorem OAI.KLInvariance.TitsSpace.bottPolynomialSheaf_flabby line 431
  32. theorem OAI.KLInvariance.TitsSpace.bottPolynomialSheaf_generated line 435
  33. theorem OAI.KLInvariance.TitsSpace.bottPolynomialSheaf_character line 439
  34. theorem OAI.KLInvariance.TitsSpace.bottStalkCharacter_decomposition line 443
  35. def OAI.KLInvariance.IntegralSupport.projection line 477
  36. def OAI.KLInvariance.IntegralSupport.supported line 479
  37. def OAI.KLInvariance.IntegralSupport.cut line 488
  38. theorem OAI.KLInvariance.IntegralSupport.cut_apply line 491
  39. theorem OAI.KLInvariance.IntegralSupport.cut_self line 493
  40. theorem OAI.KLInvariance.IntegralSupport.cut_other line 496
  41. theorem OAI.KLInvariance.IntegralSupport.cut_of_supported line 499
  42. theorem OAI.KLInvariance.IntegralSupport.cut_eq_zero line 509
  43. theorem OAI.KLInvariance.IntegralSupport.supported_iff_annihilates line 521

    Source documentation

    The exact integral annihilator, not merely its generic vector space.

     theorem supported_iff_annihilates (x : V) (m : M) :
    m ∈ supported M x ↔ ∀ n : M, projection M x n = 0 → d m n = 0 := by
…

    Mentions: OAI.KLInvariance.IntegralSupport.supported, OAI.KLInvariance.IntegralSupport.projection

  44. def OAI.KLInvariance.IntegralSupport.dualToSupport line 541

    Source documentation

    Precomposition with a surjective stalk projection gives the integral single-support module. No field extension was used anywhere in this map.

    noncomputable def dualToSupport (x : V) : Module.Dual R (A x) →ₗ[R] supported M x :=
…

    Mentions: OAI.KLInvariance.IntegralSupport.supported

  45. theorem OAI.KLInvariance.IntegralSupport.dualToSupport_bijective line 551
  46. def OAI.KLInvariance.IntegralSupport.supportEquivDual line 570
  47. theorem OAI.BalancedCuts.balanced line 594
  48. theorem OAI.KLInvariance.TitsSpace.bottSection_supported_annihilates line 619
  49. theorem OAI.KLInvariance.TitsSpace.bottSection_projector_balanced line 638
  50. theorem OAI.KLInvariance.TitsSpace.bottSupported_of_stalkSupport line 671
  51. theorem OAI.KLInvariance.TitsSpace.bottStalk_supported_annihilates line 681
  52. theorem OAI.KLInvariance.Graded.homogeneous_basis_repr line 709
  53. theorem OAI.KLInvariance.Graded.dualBasis_homogeneous line 724
  54. theorem OAI.KLInvariance.Graded.ModuleData.degree_le_of_dual_equiv line 747
  55. def OAI.KLInvariance.Graded.ModuleData.reflectedBasis line 763
  56. theorem OAI.KLInvariance.Graded.ModuleData.char_of_dual_equiv line 784
  57. theorem OAI.KLInvariance.MomentGraph.Sheaf.scaled_single_section line 820

    Source documentation

    A common edge annihilator makes all the scaled coordinate idempotents integral endomorphisms of the section module.

     theorem scaled_single_section [DecidableEq V] {p : R}
    (hp : ∀ e (v : B.edge e), p • v = 0) (x : V) (m : B.sections Set.univ) :
    p • Pi.single x (m.val x) ∈ B.sections Set.univ := by
…
  58. def OAI.KLInvariance.MomentGraph.Sheaf.labelProduct line 828
  59. theorem OAI.KLInvariance.MomentGraph.Sheaf.labelProduct_ne_zero line 830
  60. theorem OAI.KLInvariance.MomentGraph.Sheaf.labelProduct_annihilates line 833
  61. theorem OAI.KLInvariance.MomentGraph.Sheaf.projection_surjective line 840
  62. def OAI.KLInvariance.MomentGraph.Sheaf.singleSupportEquivDual line 856
  63. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.UpperQuotient.annihilates line 871
  64. theorem OAI.KLInvariance.MomentGraph.Sheaf.stalkMap_eq_zero_iff line 889
  65. theorem OAI.KLInvariance.MomentGraph.Sheaf.single_section_iff line 898
  66. def OAI.KLInvariance.MomentGraph.Sheaf.incoming line 926
  67. theorem OAI.KLInvariance.MomentGraph.Sheaf.mem_incoming line 928
  68. def OAI.KLInvariance.MomentGraph.Sheaf.incomingProduct line 931
  69. theorem OAI.KLInvariance.MomentGraph.Sheaf.incomingProduct_ne_zero line 940
  70. theorem OAI.KLInvariance.MomentGraph.Sheaf.outgoing_product_regular line 945
  71. theorem OAI.KLInvariance.MomentGraph.Sheaf.single_section_iff_prod line 959

    Source documentation

    The actual integral single-support conditions. Downward labels impose product divisibility, and they are regular at every upward edge.

     theorem single_section_iff_prod [DecompositionMonoid R] (x : V)
    (hrel : (incoming (G := G) x : Set E).Pairwise (Function.onFun IsRelPrime α))
…

    Mentions: OAI.KLInvariance.MomentGraph.Sheaf.incoming

  72. def OAI.KLInvariance.MomentGraph.Sheaf.singleStalk line 996

    Source documentation

    The single-support part as an actual submodule of its stalk.

    def singleStalk (x : V) : Submodule R (B.vertex x) :=
…
  73. def OAI.KLInvariance.MomentGraph.Sheaf.singleStalkEquivSupport line 999
  74. def OAI.KLInvariance.MomentGraph.Sheaf.kernelEquivSingleStalk line 1025
  75. theorem OAI.KLInvariance.BruhatGraph.root_injective_on_labels line 1061
  76. theorem OAI.KLInvariance.BruhatGraph.polynomialLabel_prime line 1065
  77. theorem OAI.KLInvariance.BruhatGraph.label_eq_of_polynomialLabel_dvd line 1071
  78. theorem OAI.KLInvariance.BruhatGraph.incoming_pairwise_relPrime line 1090
  79. theorem OAI.KLInvariance.BruhatGraph.outgoing_incoming_not_dvd line 1100
  80. def OAI.KLInvariance.Hilbert.scalarDegreeMap line 1124
  81. theorem OAI.KLInvariance.Hilbert.scalarDegreeMap_surjective line 1132
  82. theorem OAI.KLInvariance.Hilbert.scalarDegreeMap_injective line 1146
  83. def OAI.KLInvariance.Hilbert.scalarDegreeEquiv line 1153
  84. theorem OAI.KLInvariance.Hilbert.scalar_value line 1161
  85. theorem OAI.KLInvariance.Hilbert.scalarQuotient_value line 1186
  86. def OAI.KLInvariance.Hilbert.imageMap line 1216
  87. theorem OAI.KLInvariance.Hilbert.imageMap_surjective line 1221
  88. theorem OAI.KLInvariance.Hilbert.imageMap_ker line 1227
  89. theorem OAI.KLInvariance.Hilbert.map_homogeneous line 1243
  90. theorem OAI.KLInvariance.Hilbert.saturated_image_value line 1256

    Source documentation

    The actual upper image of a saturated graded submodule has precisely (1-q^d) times its Hilbert series. No choice of edge basis enters this identity.

    theorem saturated_image_value
    (𝓐 : ℤ → Submodule k A) (𝓜 : ℤ → Submodule k M) (𝓝 : ℤ → Submodule k N)
    [DirectSum.Decomposition 𝓜] [DirectSum.Decomposition 𝓝]
    [SetLike.GradedSMul 𝓐 𝓜] [∀ n, Module.Finite k (𝓜 n)]
    (S : Submodule A M) (hS : ∀ n m, m ∈ S → component 𝓜 n m ∈ S)
    (f : M →ₗ[A] N) (hf : ∀ n m, m ∈ 𝓜 n → f m ∈ 𝓝 n)
    (a : A) (d : ℤ) (ha : a ∈ 𝓐 d)
    (hk : ∀ v, f v = 0 ↔ ∃ w, v = a • w)
    (hsat : ∀ v, a • v ∈ S → v ∈ S)
    (hinj : Function.Injective (fun v : M => a • v))
    {q : ℝ} (hq : 0 < q) (hs : Summable (term 𝓜 (S.restrictScalars k) q)) :
    value 𝓝 ((S.map f).restrictScalars k) q =
…

    Mentions: OAI.KLInvariance.Hilbert.term, OAI.KLInvariance.Hilbert.value

  91. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.upwardSubmodule_saturated line 1302
  92. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.upper_image_value line 1315
  93. theorem OAI.KLInvariance.BruhatGraph.label_regular_stalk line 1353
  94. theorem OAI.KLInvariance.BruhatGraph.incoming_label_regular_outgoing line 1361
  95. theorem OAI.KLInvariance.BruhatGraph.upper_image_hilbert line 1372
  96. def OAI.KLInvariance.BruhatGraph.kernelEquivSingleSupport line 1412
  97. structure OAI.KLInvariance.BruhatGraph.SectionDuality line 1432
  98. def OAI.KLInvariance.BruhatGraph.costalkEquivDual line 1447
  99. theorem OAI.KLInvariance.BruhatGraph.costalk_free_of_duality line 1459
  100. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.dualToSupport_homogeneous line 1492
  101. theorem OAI.KLInvariance.Graded.mem_of_homogeneous_smul line 1523

    Source documentation

    Cancellation of an injective homogeneous scalar action includes the inverse grading shift. It does not require the scalar to be a unit.

     theorem mem_of_homogeneous_smul (d : ℤ) (a : A) (ha : a ∈ 𝓐 d)
    (hinj : Function.Injective (fun m : M => a • m))
    (n : ℤ) (m : M) (hm : a • m ∈ 𝓜 n) : m ∈ 𝓜 (n-d) := by
…
  102. theorem OAI.KLInvariance.BruhatGraph.incomingProduct_homogeneous line 1555
  103. theorem OAI.KLInvariance.BruhatGraph.kernelEquivSingleSupport_apply line 1565
  104. theorem OAI.KLInvariance.BruhatGraph.costalkEquivDual_inverse_homogeneous line 1574
  105. def OAI.KLInvariance.BruhatGraph.incomingEquivInversions line 1634
  106. theorem OAI.KLInvariance.BruhatGraph.incoming_card line 1663
  107. def OAI.KLInvariance.BruhatGraph.fullSubmodule line 1695
  108. theorem OAI.KLInvariance.BruhatGraph.fullKernel_eq line 1700
  109. def OAI.KLInvariance.BruhatGraph.fullKernel line 1707
  110. theorem OAI.KLInvariance.BruhatGraph.costalk_hilbert_of_duality line 1712
  111. def OAI.KLInvariance.CoefficientChange.mapEquiv line 1771
  112. def OAI.KLInvariance.CoefficientChange.dualTo line 1778
  113. def OAI.KLInvariance.CoefficientChange.dualFrom line 1787
  114. def OAI.KLInvariance.CoefficientChange.dualEquiv line 1802
  115. def OAI.KLInvariance.CoefficientChange.pairingEquiv line 1824
  116. theorem OAI.KLInvariance.CoefficientChange.pairingEquiv_apply line 1829
  117. structure OAI.KLInvariance.MomentGraph.GradedSheaf.PerfectPairing line 1850
  118. def OAI.KLInvariance.MomentGraph.GradedSheaf.PerfectPairing.pullback line 1860
  119. def OAI.KLInvariance.MomentGraph.GradedSheaf.PerfectPairing.coefficientChange line 1884