OAI/RepresentationTheory/KazhdanLusztig/SimultaneousInvariance.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

R-first simultaneous invariance and transported-schedule terminal-kernel freeness: upper-interval freeness, lower-interval cancellation, reversal and endpoint bottom freeness; all-entry transport and KL degree rigidity.

  1. def OAI.KLInvariance.BruhatGraph.upperIntervalIso line 21
  2. def OAI.KLInvariance.BruhatGraph.upperGraphInclusion line 44
  3. theorem OAI.KLInvariance.BruhatGraph.upperGraphInclusion_outgoing line 54
  4. theorem OAI.KLInvariance.BruhatGraph.upperIntervalIso_val line 66
  5. theorem OAI.KLInvariance.BruhatGraph.upper_transportedSlope line 71
  6. theorem OAI.KLInvariance.BruhatGraph.cutoff_is_suffix line 75
  7. theorem OAI.KLInvariance.BruhatGraph.intervalBoundary_upper_kernel line 85
  8. def OAI.KLInvariance.BruhatGraph.FreeSuffixes line 118
  9. theorem OAI.KLInvariance.BruhatGraph.target_free_of_upper_suffixes line 124
  10. theorem OAI.KLInvariance.BruhatGraph.no_conditions_free line 167
  11. theorem OAI.KLInvariance.BruhatGraph.schedule_kernels_free_of_images_eq line 181

    Source documentation

    Reverse traversal of the actual schedule, after embedded image equality. Both kernels used in Schanuel have already been made free at this point.

     theorem schedule_kernels_free_of_images_eq (p : List (Edge cs u b))
    (heq : ∀ e q, e::q <:+ p →
      B.sheaf.lowerImage e (remainingConditions cs u b q ((graph cs u b).source e)) =
      (B.sheaf.upperImage e (remainingConditions cs u b q ((graph cs u b).target e))).map
        (edgeFactorMap cs basis u b hub B e)) :
    ∀ q, q <:+ p → ∀ x : Interval cs u b,
      Module.Free (Coefficient (σ := σ))
…

    Mentions: OAI.KLInvariance.BruhatGraph.Edge, OAI.KLInvariance.BruhatGraph.remainingConditions, OAI.KLInvariance.BruhatGraph.graph, OAI.KLInvariance.BruhatGraph.source, OAI.KLInvariance.BruhatGraph.target, OAI.KLInvariance.BruhatGraph.edgeFactorMap, OAI.KLInvariance.Interval, OAI.KLInvariance.BruhatGraph.Coefficient

  12. theorem OAI.KLInvariance.BruhatGraph.schedule_kernels_free_of_endpoint_eq line 217
  13. theorem OAI.KLInvariance.BruhatGraph.transported_initial_scaledStalk line 255
  14. theorem OAI.KLInvariance.BruhatGraph.actual_comparison_of_upper_freeness line 264
  15. theorem OAI.KLInvariance.BruhatGraph.actual_endpoint_of_rTilde_eq line 278
  16. theorem OAI.KLInvariance.BruhatGraph.actual_freeSuffixes_of_rTilde_eq line 296
  17. def OAI.KLInvariance.Comparison.scaledPolynomial line 325
  18. theorem OAI.KLInvariance.Comparison.eq_of_scaled_difference_reciprocal line 328
  19. theorem OAI.KLInvariance.Comparison.matrix_difference_single line 350
  20. theorem OAI.KLInvariance.Comparison.matrix_difference_le line 366
  21. theorem OAI.KLInvariance.BruhatGraph.scaledStalk_upper_top line 399
  22. theorem OAI.KLInvariance.BruhatGraph.rTilde_eval_le_of_comparison line 410
  23. theorem OAI.KLInvariance.BruhatGraph.rTilde_eval_le_of_upper_freeness line 444
  24. theorem OAI.KLInvariance.Comparison.polynomial_eq_of_transfer_eval_eq line 462