Decomposition.lean`

120 declarations, 0 contain sorry, 0 declared as axioms

Graded decomposition characters, reflection-plane algebras and reflection Frobenius structures.

def OAI.KLInvariance.MomentGraph.GradedSheaf.freeStalkChar line 18
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.ModelSum.character line 23
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.exists_stalkCharacter_decomposition line 69
def OAI.KLInvariance.BruhatGraph.lowerCharacter line 104
theorem OAI.KLInvariance.BruhatGraph.boundaryModels_character line 108
theorem OAI.KLInvariance.BruhatGraph.lowerCharacter_zero line 123
theorem OAI.KLInvariance.BruhatGraph.lowerCharacter_nonneg line 126
def OAI.KLInvariance.PairProjection.relation line 153
abbrev OAI.KLInvariance.PairProjection.Edge line 154
def OAI.KLInvariance.PairProjection.lower line 156
def OAI.KLInvariance.PairProjection.upper line 157
theorem OAI.KLInvariance.PairProjection.diagonal_zero line 159
theorem OAI.KLInvariance.PairProjection.compatible line 162
theorem OAI.KLInvariance.PairProjection.compatible_iff line 168
theorem OAI.KLInvariance.PairProjection.kernel_lower line 181
theorem OAI.KLInvariance.PairProjection.lower_surjective line 191
theorem OAI.KLInvariance.PairProjection.upper_surjective line 201
theorem OAI.KLInvariance.PairProjection.difference_annihilates line 213
Source documentation
A genuine right-action eigenvalue difference annihilates the edge quotient. This uses only the integral module, not a fraction-field equality.
```
theorem difference_annihilates (hf : Function.Surjective f)
    (hg : Function.Surjective g) (T : M →ₗ[R] M) (r s : R)
    (hr : ∀ m, f (T m)=r • f m) (hs : ∀ m, g (T m)=s • g m)
    (v : Edge f g) : (r-s) • v=0 := by
…
```
Mentions: OAI.KLInvariance.PairProjection.Edge
def OAI.KLInvariance.Dihedral.pairMatrix line 240
Source documentation
The matrix of a pair of distinct involutions.
```
def pairMatrix (s t : G) (hs : s * s = 1) (hst : s ≠ t) : CoxeterMatrix Bool where
…
```

theorem OAI.KLInvariance.Dihedral.wordProd_alt_even line 257

Source documentation

Alternating even words are powers of the product of the two generators.

theorem wordProd_alt_even {N : CoxeterMatrix Bool} {H : Type*} [Group H]
    (cs : CoxeterSystem N H) (i : Bool) (n : ℕ) :
    cs.wordProd (alt i (2 * n)) = (cs.simple i * cs.simple (!i)) ^ n := by
…

Mentions: OAI.KLInvariance.Dihedral.alt

theorem OAI.KLInvariance.Dihedral.injective_of_simple_order line 269

Source documentation

Homomorphisms out of a rank-two Coxeter group that do not lower its product order and do not kill either generator are injective.

theorem injective_of_simple_order {N : CoxeterMatrix Bool} {H : Type*} [Group H]
    (cs : CoxeterSystem N H) (f : H →* G)
    (hne : ∀ i, f (cs.simple i) ≠ 1)
    (horder : ∀ i, orderOf (f (cs.simple i) * f (cs.simple (!i))) = N i (!i)) :
    Function.Injective f := by
…

def OAI.KLInvariance.Dihedral.pairLift line 299
Source documentation
The map from the genuine presented rank-two Coxeter group.
```
def pairLift : (pairMatrix s t hs hst).Group →* G :=
…
```
Mentions: OAI.KLInvariance.Dihedral.pairMatrix
theorem OAI.KLInvariance.Dihedral.pairLift_simple line 313
theorem OAI.KLInvariance.Dihedral.pairLift_injective line 319
Source documentation
No relation other than the Coxeter relations is introduced by the pair.
```
theorem pairLift_injective (hs1 : s ≠ 1) (ht1 : t ≠ 1) :
    Function.Injective (pairLift s t hs ht hst) := by
…
```
Mentions: OAI.KLInvariance.Dihedral.pairLift
theorem OAI.KLInvariance.Dihedral.pairLift_range line 335
Source documentation
The presented pair generates exactly the subgroup generated by its images.
```
theorem pairLift_range :
    (pairLift s t hs ht hst).range = Subgroup.closure {s, t} := by
…
```
Mentions: OAI.KLInvariance.Dihedral.pairLift
def OAI.KLInvariance.Dihedral.pairSystem line 357
Source documentation
An actual Coxeter system on the generated subgroup, not an extra assumption.
```
def pairSystem (hs1 : s ≠ 1) (ht1 : t ≠ 1) :
    CoxeterSystem (pairMatrix s t hs hst) (Subgroup.closure {s, t}) :=
…
```
Mentions: OAI.KLInvariance.Dihedral.pairMatrix
theorem OAI.KLInvariance.Dihedral.pairSystem_simple line 366
theorem OAI.KLInvariance.TitsSpace.rootPlane_eq_of_mem line 382
Source documentation
Any two distinct positive roots in a two-dimensional root plane span it.
```
theorem rootPlane_eq_of_mem (a b l r : PositiveRoot M cs) (hab : a ≠ b)
    (hl : l.val ∈ rootPlane a b) (hr : r.val ∈ rootPlane a b) (hlr : l ≠ r) :
    rootPlane l r = rootPlane a b := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.TitsSpace.rootPlane
theorem OAI.KLInvariance.TitsSpace.positive_combination_of_slope_between line 395
Source documentation
Slope betweenness detects the actual positive cone, not only one implication.
```
theorem positive_combination_of_slope_between (a b c : PositiveRoot M cs)
    (hc : c.val ∈ rootPlane a b)
    (hac : geometricSlope a < geometricSlope c)
    (hcb : geometricSlope c < geometricSlope b) :
    ∃ r s : ℝ, 0 < r ∧ 0 < s ∧ c.val = r • a.val + s • b.val := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.TitsSpace.rootPlane, OAI.KLInvariance.TitsSpace.geometricSlope

theorem OAI.KLInvariance.TitsSpace.noninverted_of_positive_combination line 434

Source documentation

Positivity is convex in the root cone.

theorem noninverted_of_positive_combination (w : W) (a b c : PositiveRoot M cs)
    {r s : ℝ} (hr : 0 ≤ r) (hs : 0 ≤ s)
    (hc : c.val = r • a.val + s • b.val)
    (ha : ¬ rootInverted w a) (hb : ¬ rootInverted w b) :
    ¬ rootInverted w c := by
…

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

theorem OAI.KLInvariance.TitsSpace.not_rootInverted_one line 444
theorem OAI.KLInvariance.TitsSpace.rootInverted_ref_self line 450
theorem OAI.KLInvariance.TitsSpace.exists_plane_extreme_inverted line 456
Source documentation
A root plane has an extreme positive root. Finiteness of inversion sets replaces the false assertion that the (real-valued) root heights are discrete.
```
theorem exists_plane_extreme_inverted (a b : PositiveRoot M cs) (hab : a ≠ b) :
    ∃ p : PositiveRoot M cs, p.val ∈ rootPlane a b ∧ rootInverted (rootRef a) p ∧
      ((∀ r : PositiveRoot M cs, r.val ∈ rootPlane a b →
          geometricSlope p ≤ geometricSlope r) ∨
       (∀ r : PositiveRoot M cs, r.val ∈ rootPlane a b →
          geometricSlope r ≤ geometricSlope p)) := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.TitsSpace.rootPlane, OAI.KLInvariance.TitsSpace.rootInverted, OAI.KLInvariance.TitsSpace.rootRef, OAI.KLInvariance.TitsSpace.geometricSlope
def OAI.KLInvariance.TitsSpace.PlaneSimple line 497
Source documentation
The canonical simple-root criterion stated on the actual ambient roots.
```
def PlaneSimple (P : Submodule ℝ (I → ℝ)) (a : PositiveRoot M cs) : Prop :=
…
```
Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot
theorem OAI.KLInvariance.TitsSpace.rootInverted_ref_iff_flipped line 501

theorem OAI.KLInvariance.TitsSpace.planeSimple_of_extreme line 507

Source documentation

An angular extreme inverts exactly its own positive root.

theorem planeSimple_of_extreme {P : Submodule ℝ (I → ℝ)}
    (a : PositiveRoot M cs) (ha : a.val ∈ P)
    (hext : (∀ r : PositiveRoot M cs, r.val ∈ P → geometricSlope a ≤ geometricSlope r) ∨
      (∀ r : PositiveRoot M cs, r.val ∈ P → geometricSlope r ≤ geometricSlope a)) :
    PlaneSimple P a := by
…

Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.TitsSpace.geometricSlope, OAI.KLInvariance.TitsSpace.PlaneSimple

theorem OAI.KLInvariance.TitsSpace.PlaneSimple.partner_val line 545
theorem OAI.KLInvariance.TitsSpace.PlaneSimple.exists_nonpositive_pair line 554
theorem OAI.KLInvariance.TitsSpace.noninverted_ref_of_pairing_nonpos line 566

theorem OAI.KLInvariance.TitsSpace.exists_opposite_plane_extreme line 576

Source documentation

The other endpoint exists even in an infinite or degenerate plane.

theorem exists_opposite_plane_extreme (a b p : PositiveRoot M cs) (hab : a ≠ b)
    (hp : p.val ∈ rootPlane a b)
    (hext : (∀ r : PositiveRoot M cs, r.val ∈ rootPlane a b →
        geometricSlope p ≤ geometricSlope r) ∨
      (∀ r : PositiveRoot M cs, r.val ∈ rootPlane a b →
        geometricSlope r ≤ geometricSlope p)) :
    ∃ q : PositiveRoot M cs, q.val ∈ rootPlane a b ∧ q ≠ p ∧
      (((∀ r : PositiveRoot M cs, r.val ∈ rootPlane a b →
          geometricSlope p ≤ geometricSlope r) ∧
        (∀ r : PositiveRoot M cs, r.val ∈ rootPlane a b →
          geometricSlope r ≤ geometricSlope q)) ∨
       ((∀ r : PositiveRoot M cs, r.val ∈ rootPlane a b →
…

Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.TitsSpace.rootPlane, OAI.KLInvariance.TitsSpace.geometricSlope

structure OAI.KLInvariance.TitsSpace.PlaneBasis line 619
Source documentation
Canonical angular endpoints of a plane; no Coxeter-system assertion is built into this data. The latter will be proved from the inversion criterion.
```
structure PlaneBasis (P : Submodule ℝ (I → ℝ)) where
…
```
theorem OAI.KLInvariance.TitsSpace.nonempty_planeBasis line 627
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.left_mem line 638
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.right_mem line 642
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.left_simple line 646
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.right_simple line 649
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.positive_cone line 653
Source documentation
Every positive root in the plane is in its canonical nonnegative cone.
```
theorem positive_cone (r : PositiveRoot M cs) (hr : r.val ∈ P) :
    ∃ c d : ℝ, 0 ≤ c ∧ 0 ≤ d ∧ r.val = c • B.left.val + d • B.right.val := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot
theorem OAI.KLInvariance.TitsSpace.PlaneSimple.planeWeight_eq_zero line 671
Source documentation
Canonical-simple reflections have no extra root pair in their own plane.
```
theorem PlaneSimple.planeWeight_eq_zero {P : Submodule ℝ (I → ℝ)}
    {a : PositiveRoot M cs} (ha : PlaneSimple P a) (x : W) :
    planeWeight x a P = 0 := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.TitsSpace.PlaneSimple, OAI.KLInvariance.TitsSpace.planeWeight
theorem OAI.KLInvariance.TitsSpace.PlaneSimple.planeLength_step line 691
Source documentation
The relative inversion count has the genuine simple-reflection step.
```
theorem PlaneSimple.planeLength_step {P : Submodule ℝ (I → ℝ)}
    {a b : PositiveRoot M cs} (ha : PlaneSimple P a)
    (hab : a ≠ b) (hP : rootPlane a b = P) (x : W)
    (hx : ¬ rootInverted x a) :
    planeLength (M := M) (cs := cs) P (rootRef a * x) =
…
```
Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.TitsSpace.PlaneSimple, OAI.KLInvariance.TitsSpace.rootPlane, OAI.KLInvariance.TitsSpace.rootInverted, OAI.KLInvariance.TitsSpace.planeLength, OAI.KLInvariance.TitsSpace.rootRef
theorem OAI.KLInvariance.TitsSpace.PlaneSimple.planeLength_step_down line 701
theorem OAI.KLInvariance.TitsSpace.rootInverted_inverse_action line 714
Source documentation
The usual inversion bijection, proved on the actual positive roots.
```
theorem rootInverted_inverse_action (w : W) (a : PositiveRoot M cs) :
    rootInverted w⁻¹ (positiveAction w⁻¹ a) ↔ rootInverted w a := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.TitsSpace.rootInverted, OAI.KLInvariance.TitsSpace.positiveAction
theorem OAI.KLInvariance.TitsSpace.inversionVector_inverse line 730
Source documentation
Reindexing the inversion indicator by the inverse root action.
```
theorem inversionVector_inverse (w : W) :
    inversionVector (M := M) (cs := cs) w⁻¹ =
…
```
Mentions: OAI.KLInvariance.TitsSpace.inversionVector
theorem OAI.KLInvariance.TitsSpace.positiveAction_mem_plane line 742
theorem OAI.KLInvariance.TitsSpace.positiveAction_mem_plane_iff line 750
theorem OAI.KLInvariance.TitsSpace.planeLength_inv line 759
Source documentation
Relative inversion count is invariant under inverse on the actual plane subgroup.
```
theorem planeLength_inv {P : Submodule ℝ (I → ℝ)} {w : W}
    (hw : w ∈ planeSubgroup M cs P) :
    planeLength (M := M) (cs := cs) P w⁻¹ = planeLength (M := M) (cs := cs) P w := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup, OAI.KLInvariance.TitsSpace.planeLength
theorem OAI.KLInvariance.TitsSpace.planeLength_nonneg line 771
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.reflection_inverts_endpoint line 784
Source documentation
A plane reflection must invert at least one of the canonical endpoints. This uses convex positivity, not any assumed Coxeter structure on the subgroup.
```
theorem reflection_inverts_endpoint (r : PositiveRoot M cs) (hr : r.val ∈ P) :
    rootInverted (rootRef r) B.left ∨ rootInverted (rootRef r) B.right := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.TitsSpace.rootInverted, OAI.KLInvariance.TitsSpace.rootRef
theorem OAI.KLInvariance.TitsSpace.PlaneSimple.inverted_after_mul line 796
Source documentation
The second descent in a simple conjugation of a nonsimple reflection.
```
theorem PlaneSimple.inverted_after_mul {P : Submodule ℝ (I → ℝ)}
    {a r : PositiveRoot M cs} (ha : PlaneSimple P a) (hr : r.val ∈ P)
    (hra : r ≠ a) (hi : rootInverted (rootRef r) a) :
    rootInverted (rootRef r * rootRef a) a := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.TitsSpace.PlaneSimple, OAI.KLInvariance.TitsSpace.rootInverted, OAI.KLInvariance.TitsSpace.rootRef
theorem OAI.KLInvariance.TitsSpace.PlaneSimple.planeLength_conj_drop line 807
Source documentation
The honest relative length drops by two under the chosen simple conjugation.
```
theorem PlaneSimple.planeLength_conj_drop {P : Submodule ℝ (I → ℝ)}
    {a b r : PositiveRoot M cs} (ha : PlaneSimple P a)
    (hab : a ≠ b) (hP : rootPlane a b = P) (hr : r.val ∈ P)
    (hra : r ≠ a) (hi : rootInverted (rootRef r) a) :
    planeLength (M := M) (cs := cs) P (rootRef (partner a r)) =
…
```
Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.TitsSpace.PlaneSimple, OAI.KLInvariance.TitsSpace.rootPlane, OAI.KLInvariance.TitsSpace.rootInverted, OAI.KLInvariance.TitsSpace.rootRef, OAI.KLInvariance.TitsSpace.planeLength, OAI.KLInvariance.TitsSpace.partner
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.rootRef_mem_pairClosure line 833
Source documentation
The canonical endpoint reflections generate every ambient reflection in the plane.
```
theorem rootRef_mem_pairClosure (r : PositiveRoot M cs) (hr : r.val ∈ P) :
    rootRef r ∈ Subgroup.closure {rootRef B.left, rootRef B.right} := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.TitsSpace.rootRef
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.pairClosure_eq_planeSubgroup line 869
Source documentation
Exact identification with the manuscript's maximal root-plane subgroup.
```
theorem pairClosure_eq_planeSubgroup :
    Subgroup.closure {rootRef B.left, rootRef B.right} = planeSubgroup M cs P := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.rootRef, OAI.KLInvariance.TitsSpace.planeSubgroup
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.rootRef_distinct line 890
Source documentation
Distinct positive roots give distinct actual reflections.
```
theorem rootRef_distinct : rootRef B.left ≠ rootRef B.right := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.rootRef
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.rootRef_ne_one line 896
def OAI.KLInvariance.TitsSpace.PlaneBasis.matrix line 901
Source documentation
The genuine dihedral matrix attached to the canonical plane endpoints.
```
def matrix : CoxeterMatrix Bool :=
…
```
def OAI.KLInvariance.TitsSpace.PlaneBasis.system line 906
Source documentation
A proved Coxeter system on the actual maximal plane subgroup.
```
def system : CoxeterSystem B.matrix (planeSubgroup M cs P) :=
…
```
Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup
def OAI.KLInvariance.TitsSpace.PlaneBasis.simpleRoot line 915
Source documentation
Canonical simple positive roots, indexed by Bool just like the system.
```
def simpleRoot (i : Bool) : PositiveRoot M cs := if i then B.right else B.left
```
Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.simpleRoot_mem line 917
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.simpleRoot_simple line 922
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.system_simple line 927

theorem OAI.KLInvariance.TitsSpace.PlaneBasis.simple_sign line 937

Source documentation

The positive simple-sign criterion for the induced plane root system.

theorem simple_sign {t : planeSubgroup M cs P} {a : I → ℝ}
    (ha : Represents M cs t.val a) (haP : a ∈ P) (hp : ∀ k, 0 ≤ a k) (i : Bool) :
    ((∀ k, action M cs (B.system.simple i : W) a k ≤ 0) ↔ t = B.system.simple i) ∧
    ((∀ k, 0 ≤ action M cs (B.system.simple i : W) a k) ↔ t ≠ B.system.simple i) := by
…

Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup, OAI.KLInvariance.TitsSpace.Represents, OAI.KLInvariance.TitsSpace.action

structure OAI.KLInvariance.TitsSpace.PlaneBasis.InducedSigned line 965
Source documentation
Signed roots for the induced system. The vectors are the original ambient roots, and membership in the actual plane is part of the relation.
```
structure InducedSigned (p : planeSubgroup M cs P × ZMod 2) (a : I → ℝ) : Prop where
…
```
Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.InducedSigned.simple line 970
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.InducedSigned.act line 996
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.inversion_iff line 1010
Source documentation
The induced positive roots have precisely the intrinsic Coxeter inversion signs. No change of realization or extra canonical-system assumption is used.
```
theorem inversion_iff {t : planeSubgroup M cs P} {a : I → ℝ}
    (ha : Represents M cs t.val a) (haP : a ∈ P) (hp : ∀ i, 0 ≤ a i)
    (w : planeSubgroup M cs P) :
    (∀ i, action M cs (w : W)⁻¹ a i ≤ 0) ↔ B.system.IsLeftInversion w t := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup, OAI.KLInvariance.TitsSpace.Represents, OAI.KLInvariance.TitsSpace.action
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.reflection_iff line 1058
Source documentation
The intrinsic reflections are exactly the ambient reflections in the actual maximal plane subgroup.
```
theorem reflection_iff (t : planeSubgroup M cs P) :
    B.system.IsReflection t ↔ cs.IsReflection (t : W) := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup
def OAI.KLInvariance.TitsSpace.PlaneBasis.inversionEquiv line 1083
Source documentation
The true ambient plane inversions are in bijection with the inversions of the canonical induced system.
```
def inversionEquiv (w : planeSubgroup M cs P) :
    {a : PositiveRoot M cs // a.val ∈ P ∧ rootInverted (w:W) a} ≃
      {t : planeSubgroup M cs P // B.system.IsLeftInversion w t} where
…
```
Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup, OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.TitsSpace.rootInverted
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.length_eq line 1108
Source documentation
Relative inversion count is the actual Coxeter length, completing the length identification, not merely a rank-two presentation.
```
theorem length_eq (w : planeSubgroup M cs P) :
    planeLength (M := M) (cs := cs) P (w:W) = (B.system.length w : ℤ) := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup, OAI.KLInvariance.TitsSpace.planeLength
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.leftInversion_iff line 1141
Source documentation
Intrinsic and ambient left inversions coincide on the plane subgroup.
```
theorem leftInversion_iff (w t : planeSubgroup M cs P) :
    B.system.IsLeftInversion w t ↔ cs.IsLeftInversion (w:W) (t:W) := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.bruhatStep_iff line 1153
Source documentation
The intrinsic directed dihedral graph is the actual ambient graph restricted to the maximal plane subgroup.
```
theorem bruhatStep_iff (g h : planeSubgroup M cs P) :
    BruhatStep cs (g:W) (h:W) ↔ BruhatStep B.system g h := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup, OAI.KLInvariance.BruhatStep
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.coset_step_iff line 1178
Source documentation
The exact canonical coset graph theorem needed by the reconstruction.
```
theorem coset_step_iff {a₀ : W}
    (hmin : ∀ z ∈ planeSubgroup M cs P, cs.length a₀ ≤ cs.length (z*a₀))
    (g h : planeSubgroup M cs P) :
    BruhatStep cs ((g:W)*a₀) ((h:W)*a₀) ↔ BruhatStep B.system g h :=
…
```
Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup, OAI.KLInvariance.BruhatStep

theorem OAI.KLInvariance.TitsSpace.PlaneBasis.coset_bruhat line 1185

Source documentation

Relative dihedral paths give actual ambient Bruhat paths in the coset.

theorem coset_bruhat {a₀ : W}
    (hmin : ∀ z ∈ planeSubgroup M cs P, cs.length a₀ ≤ cs.length (z*a₀))
    {g h : planeSubgroup M cs P} (hgh : BruhatLE B.system g h) :
    BruhatLE cs ((g:W)*a₀) ((h:W)*a₀) := by
…

Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup, OAI.KLInvariance.BruhatLE

theorem OAI.KLInvariance.TitsSpace.PlaneBasis.coset_length_eq line 1196
Source documentation
The source inversion-count characterization holds on every minimal representative coset, with its actual induced length.
```
theorem coset_length_eq {a₀ : W}
    (hmin : ∀ z ∈ planeSubgroup M cs P, cs.length a₀ ≤ cs.length (z*a₀))
    (w : planeSubgroup M cs P) :
    planeLength (M := M) (cs := cs) P ((w:W)*a₀) = (B.system.length w : ℤ) := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup, OAI.KLInvariance.TitsSpace.planeLength
theorem OAI.KLInvariance.TitsSpace.exists_positive_plane line 1220
Source documentation
Every nonsaturated reflection edge has a genuine rank-two contribution whose induced relative edge gap is at least three.
```
theorem exists_positive_plane (x : W) (a : PositiveRoot M cs)
    (hx : ¬ rootInverted x a)
    (hlen : cs.length x + 1 < cs.length (rootRef a*x)) :
    ∃ b : PositiveRoot M cs, a ≠ b ∧ 0 < planeWeight x a (rootPlane a b) := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.TitsSpace.rootInverted, OAI.KLInvariance.TitsSpace.rootRef, OAI.KLInvariance.TitsSpace.planeWeight, OAI.KLInvariance.TitsSpace.rootPlane

theorem OAI.KLInvariance.Dihedral.edge_diamond line 1243

Source documentation

Every nonsaturated dihedral edge contains a full eight-edge rectangle.

theorem edge_diamond (ds : CoxeterSystem N G) {x y : G}
    (hxy : BruhatStep ds x y) (hlen : ds.length x + 1 < ds.length y) :
    ∃ a b c d : G, a ≠ b ∧ c ≠ d ∧
      BruhatStep ds x a ∧ BruhatStep ds x b ∧
      BruhatStep ds a c ∧ BruhatStep ds a d ∧
      BruhatStep ds b c ∧ BruhatStep ds b d ∧
      BruhatStep ds c y ∧ BruhatStep ds d y := by
…

Mentions: OAI.KLInvariance.BruhatStep

theorem OAI.KLInvariance.TitsSpace.ambient_edge_diamond line 1283

Source documentation

Every genuine ambient reflection edge of length gap greater than one contains a full eight-edge diamond. The chosen plane comes from an actual positive inversion contribution, avoiding the false arbitrary-plane claim.

theorem ambient_edge_diamond {x y : W} (hxy : BruhatStep cs x y)
    (hlen : cs.length x+1 < cs.length y) :
    ∃ a b c d : W, a ≠ b ∧ c ≠ d ∧
      BruhatStep cs x a ∧ BruhatStep cs x b ∧
      BruhatStep cs a c ∧ BruhatStep cs a d ∧
      BruhatStep cs b c ∧ BruhatStep cs b d ∧
      BruhatStep cs c y ∧ BruhatStep cs d y := by
…

Mentions: OAI.KLInvariance.BruhatStep

theorem OAI.KLInvariance.diamondEdges_of_bruhatStep line 1347
Source documentation
General unlabelled Bruhat graph reconstruction completeness, for genuine finite-rank Coxeter systems and arbitrary bottoms and interval ranks.
```
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
theorem OAI.KLInvariance.intervalIso_bruhatStep_iff line 1406
Source documentation
An abstract interval order isomorphism determines its actual directed reflection edges. No root labels, generators or geometric data are supplied to that isomorphism. This proves the finite-rank graph input of the source main.
```
theorem intervalIso_bruhatStep_iff {I' W' : Type*} [Fintype I'] [Group W']
    {M' : CoxeterMatrix I'} (cs : CoxeterSystem M W) (cs' : CoxeterSystem M' W')
    {u b : W} {u' b' : W'} (e : Interval cs u b ≃o Interval cs' u' b')
    (x y : Interval cs u b) :
    BruhatStep cs' (e x).val (e y).val ↔ BruhatStep cs x.val y.val := by
…
```
Mentions: OAI.KLInvariance.Interval, OAI.KLInvariance.BruhatStep
def OAI.KLInvariance.ReflectionFrobenius.fixed line 1435
theorem OAI.KLInvariance.ReflectionFrobenius.mem_fixed line 1439
theorem OAI.KLInvariance.ReflectionFrobenius.fixed_val line 1443
def OAI.KLInvariance.ReflectionFrobenius.expand line 1447
theorem OAI.KLInvariance.ReflectionFrobenius.expand_apply line 1454
theorem OAI.KLInvariance.ReflectionFrobenius.quotient_fixed line 1462
theorem OAI.KLInvariance.ReflectionFrobenius.expand_injective line 1469
theorem OAI.KLInvariance.ReflectionFrobenius.expand_surjective line 1486
def OAI.KLInvariance.ReflectionFrobenius.coordinates line 1504
Source documentation
The actual invariant-ring basis 1, α, with no finiteness assumption.
```
def coordinates : A ≃ₗ[fixed τ] (fixed τ × fixed τ) :=
…
```
Mentions: OAI.KLInvariance.ReflectionFrobenius.fixed
theorem OAI.KLInvariance.ReflectionFrobenius.expand_coordinates line 1508
theorem OAI.KLInvariance.ReflectionFrobenius.coordinates_expand line 1512
def OAI.KLInvariance.ReflectionFrobenius.trace line 1517
theorem OAI.KLInvariance.ReflectionFrobenius.trace_expand line 1520
theorem OAI.KLInvariance.ReflectionFrobenius.square_fixed line 1527
theorem OAI.KLInvariance.ReflectionFrobenius.trace_mul line 1530
def OAI.KLInvariance.ReflectionFrobenius.crossPair line 1552
theorem OAI.KLInvariance.ReflectionFrobenius.crossPair_bijective line 1560
def OAI.KLInvariance.ReflectionFrobenius.crossPairEquiv line 1577
def OAI.KLInvariance.ReflectionFrobenius.duality line 1583
Source documentation
The Frobenius duality over the invariant ring is integral and perfect.
```
def duality : A ≃ₗ[fixed τ] Module.Dual (fixed τ) A :=
…
```
Mentions: OAI.KLInvariance.ReflectionFrobenius.fixed
theorem OAI.KLInvariance.ReflectionFrobenius.duality_apply line 1588
theorem OAI.KLInvariance.ReflectionFrobenius.duality_balanced line 1593
def OAI.KLInvariance.ReflectionFrobenius.symmetricMap line 1604
theorem OAI.KLInvariance.ReflectionFrobenius.symmetricMap_ι line 1608
theorem OAI.KLInvariance.ReflectionFrobenius.symmetricMap_comp line 1613
theorem OAI.KLInvariance.ReflectionFrobenius.symmetricMap_refl line 1620
def OAI.KLInvariance.ReflectionFrobenius.symmetricAction line 1627
Source documentation
The algebra action is induced by the linear reflection, not postulated.
```
def symmetricAction (e : V ≃ₗ[k] V) : SymmetricAlgebra k V ≃ₐ[k] SymmetricAlgebra k V :=
…
```
theorem OAI.KLInvariance.ReflectionFrobenius.symmetricAction_ι line 1633
abbrev OAI.KLInvariance.ReflectionFrobenius.reflectionAction line 1639
theorem OAI.KLInvariance.ReflectionFrobenius.reflectionAction_involutive line 1643
theorem OAI.KLInvariance.ReflectionFrobenius.reflectionAction_anti line 1654
theorem OAI.KLInvariance.ReflectionFrobenius.reflectionRoot_ne_zero line 1660
theorem OAI.KLInvariance.ReflectionFrobenius.reflectionAction_divisible line 1667
def OAI.KLInvariance.ReflectionFrobenius.reflectionDuality line 1687
Source documentation
A genuine simple-reflection integral Frobenius extension in characteristic zero, for the symmetric algebra of any representation carrying the reflection.
```
def reflectionDuality :
    SymmetricAlgebra k V ≃ₗ[fixed (reflectionAction root coroot hroot)]
      Module.Dual (fixed (reflectionAction root coroot hroot)) (SymmetricAlgebra k V) :=
…
```
Mentions: OAI.KLInvariance.ReflectionFrobenius.fixed, OAI.KLInvariance.ReflectionFrobenius.reflectionAction