OAI/RepresentationTheory/KazhdanLusztig/ReflectionSchedules.lean

GitHub source file

161 declarations, 0 contain sorry, 0 declared as axioms

Reflection schedules, decreasing paths, root-space and edge algebra, and dihedral path recursions.

  1. def OAI.KLInvariance.ReflectionSchedules.coordinatePolynomial line 18
  2. theorem OAI.KLInvariance.ReflectionSchedules.coordinatePolynomial_coeff line 21
  3. theorem OAI.KLInvariance.ReflectionSchedules.coordinatePolynomial_injective line 33
  4. def OAI.KLInvariance.ReflectionSchedules.momentFunctional line 39
  5. theorem OAI.KLInvariance.ReflectionSchedules.coordinatePolynomial_eval line 44
  6. theorem OAI.KLInvariance.ReflectionSchedules.exists_generic_functional line 49
  7. def OAI.KLInvariance.TitsSpace.height line 86
  8. theorem OAI.KLInvariance.TitsSpace.PositiveRoot.height_pos line 93
  9. def OAI.KLInvariance.TitsSpace.normalizedRoot line 103
  10. theorem OAI.KLInvariance.TitsSpace.normalizedRoot_injective line 105
  11. theorem OAI.KLInvariance.TitsSpace.countable_Positiveroot line 121
  12. theorem OAI.KLInvariance.TitsSpace.exists_geometric_functional line 126
  13. theorem OAI.KLInvariance.TitsSpace.functionalRatio_between line 138

    Source documentation

    Betweenness of all positive combinations is the angular-order condition on every root plane. This is the genuine geometric reflection-order property.

    theorem functionalRatio_between (f : Module.Dual ℝ (I → ℝ))
    (a b c : PositiveRoot M cs) {r s : ℝ} (hr : 0 < r) (hs : 0 < s)
    (hc : c.val = r • a.val + s • b.val)
    (hab : f a.val / height a.val < f b.val / height b.val) :
    f a.val / height a.val < f c.val / height c.val ∧
      f c.val / height c.val < f b.val / height b.val := by
…

    Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.TitsSpace.height

  14. def OAI.KLInvariance.TitsSpace.positiveAction line 167

    Source documentation

    Conjugation on the actual root lines, represented by positive roots.

    def positiveAction (w : W) (a : PositiveRoot M cs) : PositiveRoot M cs :=
…

    Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot

  15. theorem OAI.KLInvariance.TitsSpace.positiveAction_represents line 171
  16. theorem OAI.KLInvariance.TitsSpace.positiveAction_eq_of_nonneg line 176
  17. theorem OAI.KLInvariance.TitsSpace.positiveAction_eq_of_nonpos line 182
  18. theorem OAI.KLInvariance.TitsSpace.rootReflection_positiveAction line 189
  19. theorem OAI.KLInvariance.TitsSpace.positiveAction_one line 193
  20. theorem OAI.KLInvariance.TitsSpace.positiveAction_mul line 199
  21. def OAI.KLInvariance.TitsSpace.positiveActionEquiv line 208
  22. abbrev OAI.KLInvariance.TitsSpace.rootRef line 214
  23. theorem OAI.KLInvariance.TitsSpace.positiveAction_involutive line 216
  24. def OAI.KLInvariance.TitsSpace.rootInverted line 221
  25. theorem OAI.KLInvariance.TitsSpace.not_rootInverted_iff line 224
  26. theorem OAI.KLInvariance.TitsSpace.rootInverted_mul_of_nonneg line 232
  27. theorem OAI.KLInvariance.TitsSpace.rootInverted_mul_of_nonpos line 240
  28. theorem OAI.KLInvariance.TitsSpace.negative_pair_sum line 249
  29. theorem OAI.KLInvariance.TitsSpace.negative_pair_coefficient_pos line 255
  30. theorem OAI.KLInvariance.TitsSpace.negative_pair_not_both line 267

    Source documentation

    The crucial direct positivity argument: over an ascent in alpha, the negative root-pair for its reflection cannot both already be inversions. This works in degenerate planes and does not assume a dihedral presentation.

    theorem negative_pair_not_both (x : W) (a b : PositiveRoot M cs)
    (hx : ¬ rootInverted x a)
    (hn : ∀ i, action M cs (rootRef a) b.val i ≤ 0) :
    ¬ (rootInverted x b ∧ rootInverted x (positiveAction (rootRef a) b)) := by
…

    Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.TitsSpace.rootInverted, OAI.KLInvariance.TitsSpace.action, OAI.KLInvariance.TitsSpace.rootRef, OAI.KLInvariance.TitsSpace.positiveAction

  31. theorem OAI.KLInvariance.TitsSpace.finite_rootInverted line 298
  32. def OAI.KLInvariance.TitsSpace.inversionVector line 301
  33. theorem OAI.KLInvariance.TitsSpace.inversionVector_apply line 307
  34. theorem OAI.KLInvariance.TitsSpace.inversionVector_sum line 312
  35. def OAI.KLInvariance.TitsSpace.rootChange line 333
  36. def OAI.KLInvariance.TitsSpace.rootPlane line 335
  37. def OAI.KLInvariance.TitsSpace.planeDefect line 340

    Source documentation

    The finitely supported change in root inversions, with the distinguished root removed, grouped by actual root planes.

    def planeDefect (x y : W) (a : PositiveRoot M cs) : Submodule ℝ (I → ℝ) →₀ ℤ :=
…

    Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot

  38. theorem OAI.KLInvariance.TitsSpace.rootInverted_mul_self line 343
  39. theorem OAI.KLInvariance.TitsSpace.rootChange_distinguished line 348
  40. theorem OAI.KLInvariance.TitsSpace.planeDefect_sum line 355
  41. abbrev OAI.KLInvariance.TitsSpace.partner line 376
  42. theorem OAI.KLInvariance.TitsSpace.partner_self line 378
  43. theorem OAI.KLInvariance.TitsSpace.partner_involutive line 385
  44. theorem OAI.KLInvariance.TitsSpace.partner_eq_self_of_eq line 388
  45. abbrev OAI.KLInvariance.TitsSpace.flipped line 396
  46. theorem OAI.KLInvariance.TitsSpace.flipped_partner_iff line 399
  47. theorem OAI.KLInvariance.TitsSpace.partner_mem line 422
  48. theorem OAI.KLInvariance.TitsSpace.rootPlane_partner line 431
  49. theorem OAI.KLInvariance.TitsSpace.negative_partner_fixed line 442
  50. def OAI.KLInvariance.TitsSpace.goodPairRoot line 460

    Source documentation

    Roots in a negative pair which are both positive before the ascent.

    def goodPairRoot (x : W) (a b : PositiveRoot M cs) : Prop :=
…

    Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot

  51. theorem OAI.KLInvariance.TitsSpace.goodPairRoot_partner line 463
  52. theorem OAI.KLInvariance.TitsSpace.rootChange_pair line 469

    Source documentation

    The pairwise change is either zero or two, with no negative case.

    theorem rootChange_pair (x : W) (a b : PositiveRoot M cs) (hx : ¬ rootInverted x a) :
    rootChange x (rootRef a*x) b + rootChange x (rootRef a*x) (partner a b) =
      if goodPairRoot x a b then 2 else 0 := by
…

    Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.TitsSpace.rootInverted, OAI.KLInvariance.TitsSpace.rootChange, OAI.KLInvariance.TitsSpace.rootRef, OAI.KLInvariance.TitsSpace.partner, OAI.KLInvariance.TitsSpace.goodPairRoot

  53. def OAI.KLInvariance.TitsSpace.geometricFunctional line 503
  54. def OAI.KLInvariance.TitsSpace.geometricSlope line 505
  55. theorem OAI.KLInvariance.TitsSpace.geometricSlope_injective line 507
  56. def OAI.KLInvariance.TitsSpace.geometricOrder line 511
  57. theorem OAI.KLInvariance.TitsSpace.geometricSlope_between line 513
  58. def OAI.KLInvariance.TitsSpace.partnerEquiv line 519
  59. theorem OAI.KLInvariance.TitsSpace.partnerEquiv_apply line 522
  60. theorem OAI.KLInvariance.TitsSpace.partnerEquiv_symm_apply line 523
  61. def OAI.KLInvariance.TitsSpace.extraRoot line 525
  62. theorem OAI.KLInvariance.TitsSpace.extraRoot_partner line 527
  63. theorem OAI.KLInvariance.TitsSpace.extraRoot_finite line 531
  64. def OAI.KLInvariance.TitsSpace.halfRoot line 536
  65. theorem OAI.KLInvariance.TitsSpace.halfRoot_finite line 539
  66. def OAI.KLInvariance.TitsSpace.rootIndicator line 542
  67. theorem OAI.KLInvariance.TitsSpace.rootIndicator_apply line 546
  68. def OAI.KLInvariance.TitsSpace.extraVector line 549
  69. def OAI.KLInvariance.TitsSpace.halfVector line 550
  70. theorem OAI.KLInvariance.TitsSpace.extraVector_eq_half line 553

    Source documentation

    A choice of one root in each actual two-element negative pair.

    theorem extraVector_eq_half (x : W) (a : PositiveRoot M cs) :
    extraVector x a = halfVector x a + Finsupp.mapDomain (partnerEquiv a) (halfVector x a) := by
…

    Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.TitsSpace.extraVector, OAI.KLInvariance.TitsSpace.halfVector, OAI.KLInvariance.TitsSpace.partnerEquiv

  71. theorem OAI.KLInvariance.TitsSpace.erasedChange_pair line 569

    Source documentation

    All apparent negative contributions cancel under the actual reflection on root lines; the remaining pairs are precisely extraVector.

    theorem erasedChange_pair (x : W) (a : PositiveRoot M cs) (hx : ¬ rootInverted x a) :
    (rootChange x (rootRef a*x)).erase a +
      Finsupp.mapDomain (partnerEquiv a) ((rootChange x (rootRef a*x)).erase a) =
        extraVector x a + extraVector x a := by
…

    Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.TitsSpace.rootInverted, OAI.KLInvariance.TitsSpace.rootChange, OAI.KLInvariance.TitsSpace.rootRef, OAI.KLInvariance.TitsSpace.partnerEquiv, OAI.KLInvariance.TitsSpace.extraVector

  72. theorem OAI.KLInvariance.TitsSpace.mapDomain_plane_partner line 584
  73. def OAI.KLInvariance.TitsSpace.planeWeight line 592
  74. theorem OAI.KLInvariance.TitsSpace.planeDefect_eq_double_weight line 596
  75. theorem OAI.KLInvariance.TitsSpace.planeWeight_nonneg line 610
  76. theorem OAI.KLInvariance.TitsSpace.sum_planeWeight line 621

    Source documentation

    Exact ambient degree formula, with actual roots, finite support and nonnegative integral planar weights; no labeled interval isomorphism enters.

    theorem sum_planeWeight (x : W) (a : PositiveRoot M cs) (hx : ¬ rootInverted x a) :
    2 * (planeWeight x a).sum (fun _ n => n) =
      (cs.length (rootRef a*x) : ℤ) - cs.length x - 1 := by
…

    Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.TitsSpace.rootInverted, OAI.KLInvariance.TitsSpace.planeWeight, OAI.KLInvariance.TitsSpace.rootRef

  77. theorem OAI.KLInvariance.TitsSpace.positiveRoots_independent line 640
  78. theorem OAI.KLInvariance.TitsSpace.rootPlane_finrank line 648
  79. theorem OAI.KLInvariance.TitsSpace.rootPlane_self_finrank line 663
  80. theorem OAI.KLInvariance.TitsSpace.rootPlane_eq_iff line 669
  81. def OAI.KLInvariance.TitsSpace.planeLength line 705

    Source documentation

    The actual finite count of ambient inversions belonging to a root plane. No Coxeter presentation of the plane subgroup is assumed here.

    def planeLength (P : Submodule ℝ (I → ℝ)) (w : W) : ℤ :=
…
  82. theorem OAI.KLInvariance.TitsSpace.rootPlane_grouped_erase line 708
  83. theorem OAI.KLInvariance.TitsSpace.planeDefect_eq_relative_difference line 733
  84. theorem OAI.KLInvariance.TitsSpace.planeWeight_relative_degree line 742
  85. theorem OAI.KLInvariance.EdgeAlgebra.symmetric_ι_injective line 759
  86. def OAI.KLInvariance.EdgeAlgebra.rootIdeal line 771
  87. def OAI.KLInvariance.EdgeAlgebra.rootLine line 774
  88. def OAI.KLInvariance.EdgeAlgebra.symQuotientMap line 776
  89. theorem OAI.KLInvariance.EdgeAlgebra.symQuotientMap_ι line 779
  90. theorem OAI.KLInvariance.EdgeAlgebra.rootIdeal_le_ker line 784
  91. def OAI.KLInvariance.EdgeAlgebra.quotientForward line 795
  92. def OAI.KLInvariance.EdgeAlgebra.quotientRootMap line 799
  93. def OAI.KLInvariance.EdgeAlgebra.quotientBackward line 810
  94. theorem OAI.KLInvariance.EdgeAlgebra.quotientForward_mk line 813
  95. theorem OAI.KLInvariance.EdgeAlgebra.quotientBackward_ι_mk line 816
  96. def OAI.KLInvariance.EdgeAlgebra.rootQuotientEquiv line 824

    Source documentation

    Exact coefficient-ring identification used for the manuscript's C=A/(alpha). This is an isomorphism of the actual quotient, not a replacement invariant.

    def rootQuotientEquiv (a : V) : (SymmetricAlgebra k V ⧸ rootIdeal (k := k) a) ≃ₐ[k]
…

    Mentions: OAI.KLInvariance.EdgeAlgebra.rootIdeal

  97. theorem OAI.KLInvariance.EdgeAlgebra.rootQuotientEquiv_mk_ι line 845
  98. theorem OAI.KLInvariance.EdgeAlgebra.reducedRoot_ne_zero line 850
  99. theorem OAI.KLInvariance.EdgeAlgebra.linear_homogeneous line 861
  100. def OAI.KLInvariance.EdgeAlgebra.rootQuotientPolynomial line 871

    Source documentation

    Polynomial coordinates on the actual symmetric-algebra quotient.

    def rootQuotientPolynomial (a : V) (b : Basis κ k (V ⧸ rootLine (k := k) a)) :
…

    Mentions: OAI.KLInvariance.EdgeAlgebra.rootLine

  101. theorem OAI.KLInvariance.EdgeAlgebra.reducedRoot_homogeneous line 875
  102. theorem OAI.KLInvariance.TitsSpace.planeWeight_support_root line 895
  103. def OAI.KLInvariance.TitsSpace.planeRoot line 908
  104. theorem OAI.KLInvariance.TitsSpace.planeRoot_ne line 912
  105. theorem OAI.KLInvariance.TitsSpace.planeRoot_plane line 916
  106. theorem OAI.KLInvariance.TitsSpace.embed_not_rootLine line 920
  107. abbrev OAI.KLInvariance.TitsSpace.EdgeCoefficient line 930
  108. def OAI.KLInvariance.TitsSpace.reducedPlaneRoot line 933
  109. theorem OAI.KLInvariance.TitsSpace.reducedPlaneRoot_ne_zero line 938
  110. def OAI.KLInvariance.TitsSpace.edgeFactor line 944

    Source documentation

    The manuscript's actual product of reduced root forms, with its proved nonnegative integral plane exponents. No abstract invariant is substituted.

    def edgeFactor (x : W) (a : PositiveRoot M cs) : EdgeCoefficient a :=
…

    Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.TitsSpace.EdgeCoefficient

  111. def OAI.KLInvariance.TitsSpace.edgeFactorDegree line 947
  112. def OAI.KLInvariance.TitsSpace.edgePolynomial line 950
  113. theorem OAI.KLInvariance.TitsSpace.edgeFactor_nonzero line 954
  114. theorem OAI.KLInvariance.TitsSpace.edgeFactor_homogeneous line 966
  115. theorem OAI.KLInvariance.TitsSpace.edgeFactor_totalDegree line 975
  116. theorem OAI.KLInvariance.TitsSpace.edgeFactorDegree_cast line 985
  117. theorem OAI.KLInvariance.TitsSpace.edgeFactor_degree_formula line 993
  118. theorem OAI.KLInvariance.EdgeAlgebra.rootIdeal_eq_ker line 1009
  119. theorem OAI.KLInvariance.EdgeAlgebra.rootIdeal_isPrime line 1018
  120. theorem OAI.KLInvariance.EdgeAlgebra.symmetric_ι_prime line 1022
  121. theorem OAI.KLInvariance.EdgeAlgebra.reducedRoot_prime line 1030
  122. theorem OAI.KLInvariance.EdgeAlgebra.symmetric_ι_dvd_iff line 1047
  123. theorem OAI.KLInvariance.EdgeAlgebra.mkQ_mem_span_iff line 1065
  124. theorem OAI.KLInvariance.EdgeAlgebra.reducedRoot_dvd_iff line 1087
  125. theorem OAI.KLInvariance.TitsSpace.embed_mem_span_pair line 1114
  126. theorem OAI.KLInvariance.TitsSpace.reducedPlaneRoot_prime line 1129
  127. theorem OAI.KLInvariance.TitsSpace.reducedPlaneRoot_dvd_iff line 1134
  128. def OAI.KLInvariance.SchedulePaths.IsPath line 1161
  129. def OAI.KLInvariance.SchedulePaths.pathTerm line 1166
  130. def OAI.KLInvariance.SchedulePaths.step line 1172

    Source documentation

    One elementary matrix 1+T E_xy, acting without choosing an enumeration of the finite vertex set.

    def step (T : R) (e : E) (v : V → R) : V → R :=
…
  131. def OAI.KLInvariance.SchedulePaths.dispatch line 1177

    Source documentation

    Edges are listed in decreasing schedule order, so the chronologically last transfer is the outermost one.

    def dispatch (T : R) (v : V → R) : List E → V → R
  | [] => v
  | e :: p => step source target T e (dispatch T v p)

/-- The full matrix expansion, each sublist contributing exactly one path
term. Noncomposable sublists contribute zero by the definition of pathTerm. -/

    Mentions: OAI.KLInvariance.SchedulePaths.step

  132. theorem OAI.KLInvariance.SchedulePaths.dispatch_eq_path_sum line 1183

    Source documentation

    The full matrix expansion, each sublist contributing exactly one path term. Noncomposable sublists contribute zero by the definition of pathTerm.

    theorem dispatch_eq_path_sum (T : R) (v : V → R) (p : List E) (x : V) :
    dispatch source target T v p x =
      ((p.sublists').map (fun q => pathTerm source target T v q x)).sum := by
…

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

  133. theorem OAI.KLInvariance.SchedulePaths.pathTerm_delta line 1200

    Source documentation

    With a delta initial value, a path contributes its length weight, not an invariant defined by the desired conclusion.

    theorem pathTerm_delta (T : R) (x y : V) (p : List E) :
    pathTerm source target T (fun z => if z = y then 1 else 0) p x =
      if IsPath source target x y p then T ^ p.length else 0 := by
…

    Mentions: OAI.KLInvariance.SchedulePaths.pathTerm, OAI.KLInvariance.SchedulePaths.IsPath

  134. theorem OAI.KLInvariance.SchedulePaths.entry_eq_weighted_paths line 1217

    Source documentation

    The entry of the elementary-matrix product is exactly the sum of weights of directed schedule-subpaths.

    theorem entry_eq_weighted_paths (T : R) (p : List E) (x y : V) :
    dispatch source target T (fun z => if z = y then 1 else 0) p x =
      ((p.sublists').map (fun q =>
        if IsPath source target x y q then T ^ q.length else 0)).sum := by
…

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

  135. theorem OAI.KLInvariance.SchedulePaths.decreasing_of_schedule_path line 1233

    Source documentation

    Ties in a legitimate reflection schedule cannot occur on a composable pair. Hence every nonzero term in the schedule expansion has strictly rather than merely weakly decreasing labels.

    theorem decreasing_of_schedule_path
    (hties : ∀ e f, label e = label f → target e ≠ source f)
    {p : List E} {x y : V}
    (hp : IsPath source target x y p)
    (hs : p.Pairwise (fun e f => label f ≤ label e)) :
    p.Pairwise (fun e f => label f < label e) := by
…

    Mentions: OAI.KLInvariance.SchedulePaths.IsPath

  136. theorem OAI.KLInvariance.SchedulePaths.sublist_of_decreasing_subset line 1260

    Source documentation

    Every strictly decreasing edge list contained in a weakly decreasing schedule occurs as a sublist. This also handles arbitrary ordering of ties: a strict list can use at most one edge of each label.

    theorem sublist_of_decreasing_subset {p schedule : List E}
    (hp : p.Pairwise (fun e f => label f < label e))
    (hs : schedule.Pairwise (fun e f => label f ≤ label e))
    (hmem : p ⊆ schedule) : List.Sublist p schedule := by
…
  137. theorem OAI.KLInvariance.ReflectionPlane.reflection_triple_in_plane line 1307

    Source documentation

    The product of three normalized reflections in a root plane is again an actual orthogonal reflection. The plane itself need not be nondegenerate.

    theorem reflection_triple_in_plane
    (B : LinearMap.BilinForm ℝ V) (hB : B.IsSymm)
    (a b c : V) (ha : B a a = 2) (hb : B b b = 2) (hc : B c c = 2)
    (hplane : c ∈ Submodule.span ℝ {a,b}) :
    ∃ d : V, ∃ hd : B d d = 2,
      Module.reflection ha * Module.reflection hb * Module.reflection hc =
        Module.reflection hd := by
…
  138. theorem OAI.KLInvariance.TitsSpace.Represents.triple_isReflection line 1370

    Source documentation

    A product of three genuine Coxeter reflections in one root plane is a Coxeter reflection, using the proved reflection faithfulness of the actual Tits extension. This is the sufficiency direction of graph diamond closure.

    theorem Represents.triple_isReflection {t s r : W} {a b c : I → ℝ}
    (ha : Represents M cs t a) (hb : Represents M cs s b) (hc : Represents M cs r c)
    (hplane : c ∈ Submodule.span ℝ {a,b}) : cs.IsReflection (t*s*r) := by
…

    Mentions: OAI.KLInvariance.TitsSpace.Represents

  139. theorem OAI.KLInvariance.BruhatStep.label_reflection line 1403
  140. theorem OAI.KLInvariance.BruhatStep.composable_labels_ne line 1409
  141. def OAI.KLInvariance.TitsSpace.graphRoot line 1425
  142. theorem OAI.KLInvariance.TitsSpace.graphRoot_represents line 1428
  143. theorem OAI.KLInvariance.TitsSpace.graphRoot_ne_of_same_source line 1432
  144. theorem OAI.KLInvariance.TitsSpace.graphRoot_ne_of_path line 1440
  145. theorem OAI.KLInvariance.TitsSpace.graphRoot_square_plane line 1447
  146. theorem OAI.KLInvariance.TitsSpace.bruhatStep_diamond_closure line 1474

    Source documentation

    Soundness of the eight-edge diamond closure rule for the genuine Bruhat reflection graph. Vertex ranks need not be consecutive; the proof uses actual root planes and reflection faithfulness, not a labeled graph isomorphism.

     theorem bruhatStep_diamond_closure {x a b c d z : W}
    (hxa : BruhatStep cs x a) (hxb : BruhatStep cs x b)
    (hac : BruhatStep cs a c) (had : BruhatStep cs a d)
    (hbc : BruhatStep cs b c) (hbd : BruhatStep cs b d)
    (hcz : BruhatStep cs c z) (hdz : BruhatStep cs d z)
    (hab : a ≠ b) (hcd : c ≠ d) : BruhatStep cs x z := by
…

    Mentions: OAI.KLInvariance.BruhatStep

  147. inductive OAI.KLInvariance.DiamondEdges line 1529

    Source documentation

    The entirely unlabelled closure used in graph reconstruction. Its completeness for Bruhat graphs is a separate obligation; this definition neither changes Bruhat order nor defines the R/KL polynomials.

    inductive DiamondEdges {X : Type u} [PartialOrder X] : X → X → Prop
  | cover {x y : X} : x ⋖ y → DiamondEdges x y
  | diamond {x a b c d z : X} :
      DiamondEdges x a → DiamondEdges x b →
      DiamondEdges a c → DiamondEdges a d →
      DiamondEdges b c → DiamondEdges b d →
      DiamondEdges c z → DiamondEdges d z →
      a ≠ b → c ≠ d → DiamondEdges x z
  148. theorem OAI.KLInvariance.DiamondEdges.map line 1538
  149. theorem OAI.KLInvariance.DiamondEdges.map_iff line 1546
  150. theorem OAI.KLInvariance.bruhatStep_of_interval_covBy line 1553
  151. theorem OAI.KLInvariance.diamondEdges_bruhatStep line 1569
  152. theorem OAI.KLInvariance.Dihedral.alt_add_two line 1585
  153. theorem OAI.KLInvariance.Dihedral.alt_odd_sandwich line 1589
  154. theorem OAI.KLInvariance.Dihedral.odd_alt_reflection line 1599
  155. theorem OAI.KLInvariance.Dihedral.reflection_iff_odd line 1611
  156. theorem OAI.KLInvariance.Dihedral.step_iff_odd line 1621
  157. theorem OAI.KLInvariance.Dihedral.two_elements_length line 1639
  158. theorem OAI.KLInvariance.Dihedral.two_step_rank_two line 1673
  159. theorem OAI.KLInvariance.interval_covBy_of_length_succ line 1697
  160. theorem OAI.KLInvariance.Dihedral.two_interval_elements_length line 1717
  161. theorem OAI.KLInvariance.Dihedral.diamondEdges_of_bruhatStep line 1734

    Source documentation

    Completeness of the actual unlabelled eight-edge closure for genuine rank-two Coxeter systems. This is a necessary local case of Dyer's general reconstruction, not a replacement main theorem.

    theorem diamondEdges_of_bruhatStep (cs : CoxeterSystem M₂ W)
    {u b : W} {x y : Interval cs u b} (hxy : BruhatStep cs x.val y.val) :
    DiamondEdges x y := by
…

    Mentions: OAI.KLInvariance.Interval, OAI.KLInvariance.BruhatStep, OAI.KLInvariance.DiamondEdges