OAI/RepresentationTheory/KazhdanLusztig/TerminalKernels.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

All-section transport, terminal kernels, scalar quotients, height-one membership in free targets and scaled edge-image inclusion.

  1. theorem OAI.KLInvariance.MomentGraph.Sheaf.Iso.scaledImages line 19
  2. theorem OAI.KLInvariance.MomentGraph.Sheaf.structure_scaledImages line 62

    Source documentation

    A quotient-product equality gives the actual two embedded model images. The common quotient is the edge module's coefficient ring.

     theorem structure_scaledImages (e : E)
    (F : Set (Outgoing (G := G) (G.source e)))
…

    Mentions: OAI.KLInvariance.MomentGraph.Sheaf.Outgoing

  3. theorem OAI.KLInvariance.MomentGraph.Sheaf.structure_scaledImages_of_count line 82
  4. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.scheduledLower_root_ne line 123
  5. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.outgoingUpper_root_ne line 138
  6. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.coset_structure_scaledImages line 146
  7. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.localized_boundary_decomposition line 200
  8. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.localized_boundary_scaledImages line 245
  9. theorem OAI.KLInvariance.FlatSubmodule.baseChange_ker line 279
  10. theorem OAI.KLInvariance.FlatSubmodule.baseChange_map line 284
  11. def OAI.KLInvariance.MomentGraph.Sheaf.kernelConstraint line 317
  12. theorem OAI.KLInvariance.MomentGraph.Sheaf.ker_kernelConstraint line 321
  13. theorem OAI.KLInvariance.MomentGraph.Sheaf.kernelConstraint_tensor line 330
  14. theorem OAI.KLInvariance.MomentGraph.Sheaf.baseChange_upwardKernel line 347
  15. theorem OAI.KLInvariance.MomentGraph.Sheaf.baseChange_lowerImage line 360
  16. theorem OAI.KLInvariance.MomentGraph.Sheaf.baseChange_upperImage line 367
  17. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.localizedCoset_kernel line 393
  18. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.ambient_boundary_scaledImages line 418
  19. theorem OAI.KLInvariance.BruhatGraph.boundary_plane_scaledImages line 462
  20. abbrev OAI.KLInvariance.BruhatGraph.EdgeRing line 516
  21. def OAI.KLInvariance.BruhatGraph.edgeRingEquiv line 519
  22. theorem OAI.KLInvariance.BruhatGraph.edgeRingEquiv_root line 524
  23. instance OAI.KLInvariance.BruhatGraph.edgeRing_isDomain line 531
  24. instance OAI.KLInvariance.BruhatGraph.edgeRing_ufm line 536
  25. theorem OAI.KLInvariance.BruhatGraph.reducedPolynomialRoot_prime line 539
  26. theorem OAI.KLInvariance.BruhatGraph.planePrime_span line 546
  27. def OAI.KLInvariance.ScalarQuotient.coordinateReduction line 573
  28. theorem OAI.KLInvariance.ScalarQuotient.coordinateReduction_surjective line 578
  29. theorem OAI.KLInvariance.ScalarQuotient.coordinateReduction_kernel line 586
  30. theorem OAI.KLInvariance.ScalarQuotient.free_of_scalar_presentation line 595
  31. def OAI.KLInvariance.ScalarQuotient.submodule line 613
  32. theorem OAI.KLInvariance.ScalarQuotient.saturated_image_free line 624
  33. theorem OAI.KLInvariance.BruhatGraph.edgeTorsion line 665
  34. def OAI.KLInvariance.BruhatGraph.edgeModule line 669
  35. theorem OAI.KLInvariance.BruhatGraph.edgeModule_tower line 674
  36. theorem OAI.KLInvariance.BruhatGraph.edgeModule_free line 681
  37. theorem OAI.KLInvariance.BruhatGraph.upperImage_free line 691
  38. theorem OAI.KLInvariance.BruhatGraph.reducedRoot_dvd_iff_mem_plane line 732
  39. theorem OAI.KLInvariance.BruhatGraph.reducedFactor_ne_zero line 746
  40. theorem OAI.KLInvariance.BruhatGraph.prime_dvd_reducedFactor line 752
  41. def OAI.KLInvariance.MomentGraph.Sheaf.outgoingLabelProduct line 781
  42. theorem OAI.KLInvariance.MomentGraph.Sheaf.outgoingLabelProduct_dvd line 784
  43. theorem OAI.KLInvariance.MomentGraph.Sheaf.outgoingLabelProduct_smul_mem line 788
  44. theorem OAI.KLInvariance.MomentGraph.Sheaf.outgoingLabelProduct_smul_upperImage line 798
  45. theorem OAI.KLInvariance.BruhatGraph.incoming_root_ne_outgoing line 822
  46. theorem OAI.KLInvariance.BruhatGraph.reducedKernelProduct_ne_zero line 827
  47. theorem OAI.KLInvariance.BruhatGraph.prime_dvd_reducedKernelProduct line 838
  48. theorem OAI.KLInvariance.ScalarQuotient.scalarImage line 867
  49. theorem OAI.KLInvariance.ScalarQuotient.free_scalarImage line 880
  50. theorem OAI.KLInvariance.TensorLocalMembership.baseChange_eq_localized line 909
  51. theorem OAI.KLInvariance.TensorLocalMembership.denominator line 914
  52. theorem OAI.KLInvariance.MomentGraph.Sheaf.scaledImages_denominator line 946
  53. theorem OAI.KLInvariance.BruhatGraph.mem_of_plane_denominators line 992
  54. theorem OAI.KLInvariance.BruhatGraph.boundary_edge_image_le line 1045
  55. def OAI.KLInvariance.BruhatGraph.intervalBoundary line 1123
  56. theorem OAI.KLInvariance.BruhatGraph.schedule_edge_image_le line 1126
  57. theorem OAI.KLInvariance.BruhatGraph.schedule_comparison_of_upper_freeness line 1171
  58. theorem OAI.KLInvariance.BruhatGraph.schedule_final_of_character line 1208
  59. theorem OAI.KLInvariance.BruhatGraph.schedule_all_conditions line 1224
  60. theorem OAI.KLInvariance.BruhatGraph.schedule_initial_of_duality_character line 1232
  61. theorem OAI.KLInvariance.BruhatGraph.normalized_emptyKernel_scaledStalk line 1273
  62. theorem OAI.KLInvariance.BruhatGraph.normalized_fullKernel_scaledStalk line 1284
  63. theorem OAI.KLInvariance.BruhatGraph.schedule_final_scaledStalk line 1324
  64. theorem OAI.KLInvariance.BruhatGraph.schedule_initial_scaledStalk line 1336
  65. theorem OAI.KLInvariance.BruhatGraph.native_endpoint_eq line 1346
  66. theorem OAI.KLInvariance.SchedulePaths.exists_suffix_score_gt line 1372