OAI/RepresentationTheory/KazhdanLusztig/EdgeLocalization.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

Bruhat sheaf localization, graded transport, local edge-image bounds and support.

  1. def OAI.KLInvariance.BruhatGraph.transportedEdge line 23
  2. theorem OAI.KLInvariance.BruhatGraph.transportedEdge_injective line 28
  3. def OAI.KLInvariance.BruhatGraph.transportedScore line 35
  4. def OAI.KLInvariance.BruhatGraph.transportedSchedule line 40

    Source documentation

    Decreasing list, in the convention for the outermost-first matrix product. Its reverse is chronological increasing reflection order.

     def transportedSchedule : List (Edge cs u b) := by
…

    Mentions: OAI.KLInvariance.BruhatGraph.Edge

  5. theorem OAI.KLInvariance.BruhatGraph.transportedSchedule_nodup line 45
  6. theorem OAI.KLInvariance.BruhatGraph.transportedSchedule_full line 50
  7. theorem OAI.KLInvariance.BruhatGraph.transportedSchedule_pairwise line 56
  8. theorem OAI.KLInvariance.BruhatGraph.transportedEdge_lift line 62
  9. theorem OAI.KLInvariance.BruhatGraph.transported_dispatch_entry line 79
  10. theorem OAI.KLInvariance.BruhatGraph.transported_entry_eq_rTilde line 118
  11. theorem OAI.KLInvariance.SchedulePaths.dispatch_map line 143
  12. theorem OAI.KLInvariance.scaledKL_reciprocity_upper line 161
  13. theorem OAI.KLInvariance.BruhatGraph.transported_entry_eval line 209
  14. theorem OAI.KLInvariance.BruhatGraph.transported_dispatch_matrix line 219
  15. theorem OAI.KLInvariance.BruhatGraph.transported_reciprocal_vector line 230
  16. theorem OAI.KLInvariance.BruhatGraph.boundarySheaf_gradedIso line 264
  17. theorem OAI.KLInvariance.BruhatGraph.stalkCharacter_eq_character line 273
  18. def OAI.KLInvariance.BruhatGraph.upperInclusion line 300
  19. theorem OAI.KLInvariance.BruhatGraph.upperInclusion_injective line 308
  20. theorem OAI.KLInvariance.BruhatGraph.upperInclusion_outgoing line 313
  21. def OAI.KLInvariance.BruhatGraph.restrictBoundary line 332
  22. theorem OAI.KLInvariance.BruhatGraph.stalkCharacter_upperRestriction line 337
  23. theorem OAI.KLInvariance.BruhatGraph.stalkCharacter_natDegree_le line 364
  24. def OAI.KLInvariance.BruhatGraph.scaledStalk line 377
  25. theorem OAI.KLInvariance.BruhatGraph.scaledStalk_reciprocity_inverse line 381
  26. theorem OAI.KLInvariance.BruhatGraph.scaledStalk_reciprocity line 423
  27. theorem OAI.KLInvariance.BruhatGraph.scaledStalk_reciprocity_upper line 430
  28. theorem OAI.KLInvariance.Graded.ModuleData.MinimalCover.hom_bijective line 482
  29. theorem OAI.KLInvariance.MomentGraph.Sheaf.AboveIso.stalk_hom_bijective line 524
  30. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.Hom.edge_bijective_of_vertex line 593
  31. def OAI.KLInvariance.MomentGraph.GradedSheaf.Hom.isoOfBijective line 611
  32. def OAI.KLInvariance.MomentGraph.GradedSheaf.Hom.aboveIso line 621
  33. theorem OAI.KLInvariance.MomentGraph.BoundarySheaf.hom_vertex_bijective line 654
  34. def OAI.KLInvariance.MomentGraph.BoundarySheaf.homIso line 678
  35. def OAI.KLInvariance.MomentGraph.GradedSheaf.Iso.hom line 700
  36. def OAI.KLInvariance.MomentGraph.GradedSheaf.Iso.invHom line 706
  37. theorem OAI.KLInvariance.MomentGraph.BoundarySheaf.hom_vertex_bijective_of_iso line 748
  38. def OAI.KLInvariance.MomentGraph.BoundarySheaf.homIsoOfIso line 762
  39. theorem OAI.KLInvariance.MomentGraph.GradedSheaf.SplitIn.comparison_bijective line 785
  40. def OAI.KLInvariance.TitsSpace.bottCanonicalAdjointHom line 822
  41. theorem OAI.KLInvariance.TitsSpace.bottCanonicalAdjointHom_top_bijective line 826
  42. def OAI.KLInvariance.TitsSpace.bottCanonicalAdjointIso line 833
  43. theorem OAI.KLInvariance.TitsSpace.bottCanonicalAdjointIso_vertex line 847
  44. theorem OAI.KLInvariance.TitsSpace.bottSplitRightWord_fixed line 876
  45. theorem OAI.KLInvariance.TitsSpace.bottCanonicalAdjointWord line 888
  46. def OAI.KLInvariance.TitsSpace.bottCanonicalPerfectPairing line 902
  47. theorem OAI.KLInvariance.TitsSpace.bottCanonicalPerfectPairing_apply line 906
  48. theorem OAI.KLInvariance.TitsSpace.bottCanonicalPerfectPairing_symmetric line 918
  49. structure OAI.KLInvariance.MomentGraph.GradedSheaf.SymmetricPerfectPairing line 941
  50. def OAI.KLInvariance.MomentGraph.GradedSheaf.SymmetricPerfectPairing.pullback line 945
  51. def OAI.KLInvariance.MomentGraph.GradedSheaf.SymmetricPerfectPairing.coefficientChange line 953
  52. theorem OAI.KLInvariance.TitsSpace.symmetricBoundarySheaf_symmetricPairing_word line 977
  53. theorem OAI.KLInvariance.TitsSpace.symmetricBoundarySheaf_symmetricPairing line 988
  54. theorem OAI.KLInvariance.BruhatGraph.boundarySheaf_symmetricPairing line 1006
  55. theorem OAI.KLInvariance.Graded.homogeneous_positive_nonzero line 1043
  56. theorem OAI.KLInvariance.Graded.dual_mem_ideal line 1060
  57. theorem OAI.KLInvariance.Graded.local_diagonal_strict_degree line 1077
  58. theorem OAI.KLInvariance.IntegralSupport.supportEquivDual_pairing line 1108