OAI/RepresentationTheory/KazhdanLusztig/PositiveTransfer.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

Positive transfer inequalities, strict Hilbert-series detection including higher-codimension support, and reverse-filtration projective-to-free arguments.

  1. theorem OAI.KLInvariance.BruhatGraph.costalkEquivDual_pairing line 24
  2. theorem OAI.KLInvariance.BruhatGraph.costalkEquivDual_symmetric line 43
  3. theorem OAI.KLInvariance.BruhatGraph.costalkEquivDual_inverse_symmetric line 62
  4. abbrev OAI.KLInvariance.BruhatGraph.ActualBoundary line 94
  5. def OAI.KLInvariance.BruhatGraph.actualSymmetricPairing line 96
  6. def OAI.KLInvariance.BruhatGraph.actualSectionDuality line 100
  7. theorem OAI.KLInvariance.BruhatGraph.actualSectionDuality_symmetric line 113
  8. theorem OAI.KLInvariance.BruhatGraph.actualSectionDuality_homogeneous line 119
  9. theorem OAI.KLInvariance.BruhatGraph.costalkFreeObligation line 129
  10. def OAI.KLInvariance.BruhatGraph.localIntersection line 132
  11. theorem OAI.KLInvariance.BruhatGraph.localIntersection_injective line 140
  12. theorem OAI.KLInvariance.BruhatGraph.localIntersection_range line 146
  13. theorem OAI.KLInvariance.BruhatGraph.localIntersection_minimal line 160
  14. theorem OAI.KLInvariance.BruhatGraph.localIntersection_homogeneous line 167
  15. theorem OAI.KLInvariance.BruhatGraph.localIntersection_symmetric line 180
  16. theorem OAI.KLInvariance.BruhatGraph.localIntersection_diagonal_strict_degree line 186
  17. theorem OAI.KLInvariance.SchedulePaths.mem_suffix_iff_score_lt line 220
  18. theorem OAI.KLInvariance.SchedulePaths.mem_suffix_iff_score_lt_injective line 236
  19. theorem OAI.KLInvariance.Hilbert.shifted_map_homogeneous line 262
  20. def OAI.KLInvariance.Hilbert.shiftedImagePieceMap line 273
  21. theorem OAI.KLInvariance.Hilbert.shiftedImagePieceMap_surjective line 284
  22. def OAI.KLInvariance.Hilbert.shiftedImagePieceEquiv line 300
  23. theorem OAI.KLInvariance.Hilbert.shifted_image_value line 316

    Source documentation

    Hilbert series of the actual embedded image of a homogeneous injection.

     theorem shifted_image_value
    (๐“œ : โ„ค โ†’ Submodule k M) (๐“ : โ„ค โ†’ Submodule k N)
    [DirectSum.Decomposition ๐“œ] [DirectSum.Decomposition ๐“]
    (S : Submodule A M) (hS : โˆ€ n m, m โˆˆ S โ†’ component ๐“œ n m โˆˆ S)
    (f : M โ†’โ‚—[A] N) (d : โ„ค) (hf : โˆ€ n m, m โˆˆ ๐“œ n โ†’ f m โˆˆ ๐“ (n+d))
    (hinj : Function.Injective f) {q : โ„} (hq : q โ‰  0)
    (hs : Summable (term ๐“œ (S.restrictScalars k) q)) :
    value ๐“ ((S.map f).restrictScalars k) q =
      q^d * value ๐“œ (S.restrictScalars k) q := by
โ€ฆ

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

  24. def OAI.KLInvariance.MomentGraph.GradedSheaf.kernelHilbert line 359
  25. def OAI.KLInvariance.MomentGraph.GradedSheaf.lowerImage line 362
  26. def OAI.KLInvariance.MomentGraph.GradedSheaf.upperImage line 366
  27. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.upperImage_homogeneous line 371
  28. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.kernelHilbert_edge line 377
  29. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.shifted_upperImage_value line 388
  30. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.edge_increment_le line 410
  31. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.edge_increment_eq_iff line 433

    Source documentation

    Even a finite-length or higher-codimension embedded defect is detected by one positive numerical equality. This does not replace the image inclusion.

     theorem edge_increment_eq_iff (ฮฑ : E โ†’ MvPolynomial ฯƒ โ„) (hquot : B.UpperQuotient ฮฑ)
    (e : E) (F : Set (Sheaf.Outgoing (G := G) (G.source e)))
โ€ฆ

    Mentions: OAI.KLInvariance.MomentGraph.Sheaf.Outgoing

  32. theorem OAI.KLInvariance.BruhatGraph.actual_edge_increment_le line 479
  33. theorem OAI.KLInvariance.BruhatGraph.actual_edge_increment_eq_iff line 500
  34. theorem OAI.KLInvariance.Comparison.edge_scalar_identity line 535

    Source documentation

    Degree-one labels, q=tยฒ, and exactly the source degree 2*k = length(y)-length(x)-1 give the same coefficient at every edge.

     theorem edge_scalar_identity {t : โ„} (ht : t โ‰  0) (m n k : โ„ค)
    (h : m + 2*k = n-1) :
    t^m * (t^2)^k * (1-t^2) = (tโปยน-t) * t^n := by
โ€ฆ
  35. theorem OAI.KLInvariance.Comparison.transferCoefficient_pos line 550
  36. theorem OAI.KLInvariance.Comparison.stateScale_pos line 555
  37. theorem OAI.KLInvariance.Comparison.scaled_increment_eq_iff line 562

    Source documentation

    Cancellation of a positive state scale converts an additive normalized edge identity back to its raw Hilbert-series increment.

     theorem scaled_increment_eq_iff (a x y k z : โ„) (ha : a โ‰  0) :
    a*x = a*y+(a*k)*z โ†” x-y=k*z := by
โ€ฆ
  38. def OAI.KLInvariance.BruhatGraph.stateScale line 591
  39. theorem OAI.KLInvariance.BruhatGraph.stateScale_positive line 595
  40. def OAI.KLInvariance.BruhatGraph.normalizedKernel line 599
  41. theorem OAI.KLInvariance.BruhatGraph.edge_stateScale line 603
  42. theorem OAI.KLInvariance.BruhatGraph.normalized_edge_increment_le line 621

    Source documentation

    A single removal of a later-edge kernel condition has the exact uniform transfer coefficient tโปยน-t used by the Dyer path matrix.

     theorem normalized_edge_increment_le (e : Edge cs u b)
    (F : Set (Sheaf.Outgoing (G := graph cs u b) ((graph cs u b).source e)))
โ€ฆ

    Mentions: OAI.KLInvariance.BruhatGraph.Edge, OAI.KLInvariance.BruhatGraph.graph, OAI.KLInvariance.BruhatGraph.source

  43. theorem OAI.KLInvariance.BruhatGraph.normalized_edge_increment_eq_iff line 637
  44. theorem OAI.KLInvariance.BruhatGraph.emptyKernel_hilbert line 677
  45. theorem OAI.KLInvariance.BruhatGraph.normalized_emptyKernel_of_character line 693
  46. theorem OAI.KLInvariance.BruhatGraph.normalized_fullKernel_of_duality_character line 708
  47. theorem OAI.KLInvariance.BruhatGraph.restrictBoundary_kernel line 776
  48. theorem OAI.KLInvariance.BruhatGraph.normalizedKernel_restrictBoundary line 784
  49. theorem OAI.KLInvariance.BruhatGraph.normalized_emptyKernel_restrictBoundary line 793
  50. theorem OAI.KLInvariance.BruhatGraph.normalized_fullKernel_restrictBoundary line 800
  51. theorem OAI.KLInvariance.SchedulePaths.step_monotone line 822
  52. theorem OAI.KLInvariance.SchedulePaths.step_injective line 830
  53. theorem OAI.KLInvariance.SchedulePaths.dispatch_monotone line 843
  54. theorem OAI.KLInvariance.SchedulePaths.dispatch_injective line 849
  55. theorem OAI.KLInvariance.SchedulePaths.dispatch_append' line 858
  56. theorem OAI.KLInvariance.SchedulePaths.remaining_state_le line 866

    Source documentation

    A concrete state indexed by the remaining chronological edge list.

     theorem remaining_state_le (T : โ„) (hT : 0 โ‰ค T)
    (D : List E โ†’ V โ†’ โ„) (p : List E)
    (hstep : โˆ€ e q, e::q <:+ p โ†’ D q โ‰ค step source target T e (D (e::q))) :
    D [] โ‰ค dispatch source target T (D p) p.reverse := by
โ€ฆ

    Mentions: OAI.KLInvariance.SchedulePaths.step, OAI.KLInvariance.SchedulePaths.dispatch

  57. theorem OAI.KLInvariance.SchedulePaths.remaining_steps_eq line 880

    Source documentation

    If the endpoint bound is equality, every embedded one-edge Hilbert bound is equality. Injectivity must be used together with the one-sided bounds.

     theorem remaining_steps_eq (T : โ„) (hT : 0 โ‰ค T)
    (D : List E โ†’ V โ†’ โ„) (p : List E)
    (hne : โˆ€ e โˆˆ p, source e โ‰  target e)
    (hstep : โˆ€ e q, e::q <:+ p โ†’ D q โ‰ค step source target T e (D (e::q)))
    (hend : D [] = dispatch source target T (D p) p.reverse) :
    โˆ€ e q, e::q <:+ p โ†’ D q = step source target T e (D (e::q)) := by
โ€ฆ

    Mentions: OAI.KLInvariance.SchedulePaths.step, OAI.KLInvariance.SchedulePaths.dispatch

  58. def OAI.KLInvariance.ReverseFiltration.scalarKernelEquiv line 931

    Source documentation

    A kernel which is exactly a regular scalar multiple of its domain is integrally isomorphic to that domain, not just to its fraction-field span.

    noncomputable def scalarKernelEquiv (g : M โ†’โ‚—[A] N) (a : A)
    (hk : โˆ€ v, g v = 0 โ†” โˆƒ w, v = a โ€ข w)
    (ha : Function.Injective (fun v : M => a โ€ข v)) :
    M โ‰ƒโ‚—[A] LinearMap.ker g := by
โ€ฆ
  59. theorem OAI.KLInvariance.ReverseFiltration.projective_kernel_of_scalar_presentation line 947
  60. def OAI.KLInvariance.ReverseFiltration.imageMapKernelEquiv line 958
  61. theorem OAI.KLInvariance.ReverseFiltration.inf_kernel_projective_of_image_eq line 970

    Source documentation

    Scaled equality of two embedded images constructs a presentation with regular scalar kernel. This is the pure module-algebra form of the reverse freeness step, allowing arbitrary image codimension.

     theorem inf_kernel_projective_of_image_eq
    (S : Submodule A M) (T : Submodule A P)
    [Module.Projective A S] [Module.Projective A T]
    (f : M โ†’โ‚—[A] N) (g : P โ†’โ‚—[A] N) (ฯ† : N โ†’โ‚—[A] N)
    (hฯ† : Function.Injective ฯ†) (himage : S.map f = (T.map g).map ฯ†)
    (a : A) (hk : โˆ€ v, g v = 0 โ†” โˆƒ w, v = a โ€ข w)
    (hsat : โˆ€ v, a โ€ข v โˆˆ T โ†’ v โˆˆ T)
    (ha : Function.Injective (fun v : P => a โ€ข v)) :
    Module.Projective A โ†ฅ(S โŠ“ LinearMap.ker f) := by
โ€ฆ
  62. theorem OAI.KLInvariance.BruhatGraph.partial_kernel_projective_of_image_eq line 1029

    Source documentation

    The reverse-freeness step uses precisely the already free upper kernel and the preceding lower kernel, plus the actual embedded image equality.

     theorem partial_kernel_projective_of_image_eq (e : Edge cs u b)
    (F : Set (Sheaf.Outgoing (G := graph cs u b) ((graph cs u b).source e)))
โ€ฆ

    Mentions: OAI.KLInvariance.BruhatGraph.Edge, OAI.KLInvariance.BruhatGraph.graph, OAI.KLInvariance.BruhatGraph.source

  63. theorem OAI.KLInvariance.BruhatGraph.partial_kernel_free_of_image_eq line 1052
  64. def OAI.KLInvariance.BruhatGraph.remainingConditions line 1089
  65. theorem OAI.KLInvariance.BruhatGraph.remainingConditions_nil line 1093
  66. theorem OAI.KLInvariance.BruhatGraph.remainingConditions_cons_source line 1097
  67. theorem OAI.KLInvariance.BruhatGraph.remainingConditions_cons_other line 1105
  68. def OAI.KLInvariance.BruhatGraph.scheduleState line 1114
  69. theorem OAI.KLInvariance.BruhatGraph.scheduleState_step line 1117
  70. theorem OAI.KLInvariance.BruhatGraph.scheduleState_le line 1148
  71. theorem OAI.KLInvariance.BruhatGraph.edgeImages_eq_of_scheduleState_eq line 1161
  72. def OAI.KLInvariance.BruhatGraph.transportedSlope line 1222
  73. def OAI.KLInvariance.BruhatGraph.chronologicalSchedule line 1225
  74. theorem OAI.KLInvariance.BruhatGraph.transportedScore_eq line 1228
  75. theorem OAI.KLInvariance.BruhatGraph.chronologicalSchedule_pairwise line 1234
  76. theorem OAI.KLInvariance.BruhatGraph.chronologicalSchedule_nodup line 1244
  77. theorem OAI.KLInvariance.BruhatGraph.chronologicalSchedule_full line 1248
  78. theorem OAI.KLInvariance.BruhatGraph.transportedSlope_source_unique line 1252
  79. theorem OAI.KLInvariance.BruhatGraph.transportedSlope_path_ne line 1264
  80. theorem OAI.KLInvariance.BruhatGraph.suffix_source_iff line 1272
  81. theorem OAI.KLInvariance.BruhatGraph.suffix_target_iff line 1280
  82. theorem OAI.KLInvariance.BruhatGraph.ambientLater_upperInclusion line 1287
  83. theorem OAI.KLInvariance.BruhatGraph.remainingConditions_source_ambient line 1306
  84. theorem OAI.KLInvariance.BruhatGraph.remainingConditions_target_ambient line 1315