noncomputable def HeckeAlgebra.lambdaOnBasis {B : Type u_1} {M : CoxeterMatrix B} {R : Type u_2} [CommRing R] (cs : CoxeterSystem M M.Group) (a b : B → R) (s : B) (w : M.Group) : M.Group →₀ R

Left-multiplication operator $λ_s$ on the basis: $λ_s(T_w) = T_{sw}$ when $\ell(sw) > \ell(w)$ and $λ_s(T_w) = a_s T_w + b_s T_{sw}$ otherwise.

noncomputable def HeckeAlgebra.rhoOnBasis {B : Type u_1} {M : CoxeterMatrix B} {R : Type u_2} [CommRing R] (cs : CoxeterSystem M M.Group) (a b : B → R) (t : B) (w : M.Group) : M.Group →₀ R

Right-multiplication operator $ρ_t$ on the basis: $ρ_t(T_w) = T_{wt}$ when $\ell(wt) > \ell(w)$ and $ρ_t(T_w) = a_t T_w + b_t T_{wt}$ otherwise.

noncomputable def HeckeAlgebra.lambdaLift {B : Type u_1} {M : CoxeterMatrix B} {R : Type u_2} [CommRing R] (cs : CoxeterSystem M M.Group) (a b : B → R) (s : B) : (M.Group →₀ R) →ₗ[R] M.Group →₀ R

Linear extension of lambdaOnBasis to the free $R$-module $R[W]$.

noncomputable def HeckeAlgebra.rhoLift {B : Type u_1} {M : CoxeterMatrix B} {R : Type u_2} [CommRing R] (cs : CoxeterSystem M M.Group) (a b : B → R) (t : B) : (M.Group →₀ R) →ₗ[R] M.Group →₀ R

Linear extension of rhoOnBasis to the free $R$-module $R[W]$.

theorem HeckeAlgebra.lambdaLift_single {B : Type u_1} [DecidableEq B] [Fintype B] {M : CoxeterMatrix B} {R : Type u_2} [CommRing R] (cs : CoxeterSystem M M.Group) (a b : B → R) (s : B) (w : M.Group) (r : R) : (lambdaLift cs a b s) (Finsupp.single w r) = r • lambdaOnBasis cs a b s w

Evaluation of lambdaLift on a single basis element: $λ_s(r · T_w) = r · λ_s(T_w)$.

theorem HeckeAlgebra.rhoLift_single {B : Type u_1} [DecidableEq B] [Fintype B] {M : CoxeterMatrix B} {R : Type u_2} [CommRing R] (cs : CoxeterSystem M M.Group) (a b : B → R) (t : B) (w : M.Group) (r : R) : (rhoLift cs a b t) (Finsupp.single w r) = r • rhoOnBasis cs a b t w

Evaluation of rhoLift on a single basis element.

theorem HeckeAlgebra.swt_eq_w_of_length {B : Type u_1} [DecidableEq B] [Fintype B] {M : CoxeterMatrix B} (cs : CoxeterSystem M M.Group) (s t : B) (w : M.Group) (h_swt : cs.length (cs.simple s * w * cs.simple t) = cs.length w) (h_sw_wt : cs.length (cs.simple s * w) = cs.length (w * cs.simple t)) : cs.simple s * w * cs.simple t = w

Coxeter-exchange consequence: if $\ell(swt) = \ell(w)$ and $\ell(sw) = \ell(wt)$, then $swt = w$.

theorem HeckeAlgebra.sw_eq_wt_of_swt_eq_w {B : Type u_1} [DecidableEq B] [Fintype B] {M : CoxeterMatrix B} (cs : CoxeterSystem M M.Group) (s t : B) (w : M.Group) (h : cs.simple s * w * cs.simple t = w) : cs.simple s * w = w * cs.simple t

From $swt = w$ deduce $sw = wt$ by right-multiplying by $t$.

theorem HeckeAlgebra.lambda_rho_commute_on_basis {B : Type u_1} [DecidableEq B] [Fintype B] {M : CoxeterMatrix B} {R : Type u_2} [CommRing R] (cs : CoxeterSystem M M.Group) (sc : StructureConstants B R) (hconj : sc.ConjugacyInvariant cs) (s t : B) (w : M.Group) : (lambdaLift cs sc.a sc.b s) (rhoOnBasis cs sc.a sc.b t w) = (rhoLift cs sc.a sc.b t) (lambdaOnBasis cs sc.a sc.b s w)

Operator commutativity $λ_s ρ_t = ρ_t λ_s$ on basis elements (Section 6.1 step), under the conjugacy-invariance assumption on the structure constants.

structure HeckeAlgebra.FreeModuleHeckeData {B' : Type u_3} (M : CoxeterMatrix B') (R : Type u_5) [CommRing R] : Type (max (max u_3 u_5) (u_6 + 1))

Data of a candidate Hecke-algebra structure on a free $R$-module, packaging both left and right length-up/length-down rules together with module operations, two-sided generator associativity, and conjugacy invariance of $(a_s, b_s)$.

• carrier : Type u_6
• basis : M.Group → self.carrier
• smul : R → self.carrier → self.carrier
• mul : self.carrier → self.carrier → self.carrier
• add : self.carrier → self.carrier → self.carrier
• a : B' → R
• b : B' → R
• left_length_up (s : B') (w : M.Group) : M.toCoxeterSystem.length (M.toCoxeterSystem.simple s * w) > M.toCoxeterSystem.length w → self.mul (self.basis (M.toCoxeterSystem.simple s)) (self.basis w) = self.basis (M.toCoxeterSystem.simple s * w)
• left_length_down (s : B') (w : M.Group) : M.toCoxeterSystem.length (M.toCoxeterSystem.simple s * w) < M.toCoxeterSystem.length w → self.mul (self.basis (M.toCoxeterSystem.simple s)) (self.basis w) = self.add (self.smul (self.a s) (self.basis w)) (self.smul (self.b s) (self.basis (M.toCoxeterSystem.simple s * w)))
• right_length_up (t : B') (w : M.Group) : M.toCoxeterSystem.length (w * M.toCoxeterSystem.simple t) > M.toCoxeterSystem.length w → self.mul (self.basis w) (self.basis (M.toCoxeterSystem.simple t)) = self.basis (w * M.toCoxeterSystem.simple t)
• right_length_down (t : B') (w : M.Group) : M.toCoxeterSystem.length (w * M.toCoxeterSystem.simple t) < M.toCoxeterSystem.length w → self.mul (self.basis w) (self.basis (M.toCoxeterSystem.simple t)) = self.add (self.smul (self.a t) (self.basis w)) (self.smul (self.b t) (self.basis (w * M.toCoxeterSystem.simple t)))
• identity_left (x : self.carrier) : self.mul (self.basis 1) x = x
• identity_right (x : self.carrier) : self.mul x (self.basis 1) = x
• mul_add_right (x y z : self.carrier) : self.mul x (self.add y z) = self.add (self.mul x y) (self.mul x z)
• mul_add_left (x y z : self.carrier) : self.mul (self.add x y) z = self.add (self.mul x z) (self.mul y z)
• mul_smul_right (r : R) (x y : self.carrier) : self.mul x (self.smul r y) = self.smul r (self.mul x y)
• smul_mul_left (r : R) (x y : self.carrier) : self.mul (self.smul r x) y = self.smul r (self.mul x y)
• add_comm (x y : self.carrier) : self.add x y = self.add y x
• add_assoc' (x y z : self.carrier) : self.add (self.add x y) z = self.add x (self.add y z)
• smul_add (r : R) (x y : self.carrier) : self.smul r (self.add x y) = self.add (self.smul r x) (self.smul r y)
• smul_smul (r₁ r₂ : R) (x : self.carrier) : self.smul r₁ (self.smul r₂ x) = self.smul (r₁ * r₂) x
• basis_span (P : self.carrier → Prop) : (∀ (w : M.Group), P (self.basis w)) → (∀ (x y : self.carrier), P x → P y → P (self.add x y)) → (∀ (r : R) (x : self.carrier), P x → P (self.smul r x)) → ∀ (z : self.carrier), P z
• conj_inv (s₁ s₂ : B') (w : M.Group) : w * M.toCoxeterSystem.simple s₁ * w⁻¹ = M.toCoxeterSystem.simple s₂ → self.a s₁ = self.a s₂ ∧ self.b s₁ = self.b s₂
• gen_left_assoc (s : B') (x y : self.carrier) : self.mul (self.basis (M.toCoxeterSystem.simple s)) (self.mul x y) = self.mul (self.mul (self.basis (M.toCoxeterSystem.simple s)) x) y
• gen_right_assoc (t : B') (x y : self.carrier) : self.mul (self.mul x y) (self.basis (M.toCoxeterSystem.simple t)) = self.mul x (self.mul y (self.basis (M.toCoxeterSystem.simple t)))

def HeckeAlgebra.FreeModuleHeckeData.toGenericAlgebra {B' : Type u_3} {M' : CoxeterMatrix B'} {R' : Type u_4} [CommRing R'] (D : FreeModuleHeckeData M' R') : GenericAlgebra M' R'

Converts a FreeModuleHeckeData into a GenericAlgebra: the quadratic relation is derived from the left length-down rule applied at $w = s$.

theorem HeckeAlgebra.isReduced_cons_iff {B' : Type u_3} {M' : CoxeterMatrix B'} (s : B') (rest : List B') : M'.toCoxeterSystem.IsReduced (s :: rest) ↔ M'.toCoxeterSystem.IsReduced rest ∧ M'.toCoxeterSystem.length (M'.toCoxeterSystem.simple s * M'.toCoxeterSystem.wordProd rest) = M'.toCoxeterSystem.length (M'.toCoxeterSystem.wordProd rest) + 1

A word $s :: \mathit{rest}$ is reduced iff rest is reduced and prepending $s$ increases the length by exactly one.

theorem HeckeAlgebra.GenericAlgebra.foldl_gen_left' {B' : Type u_3} {M' : CoxeterMatrix B'} {R' : Type u_4} [CommRing R'] (A : GenericAlgebra M' R') (s : B') (init : A.carrier) (rest : List B') : A.mul (A.basis (M'.toCoxeterSystem.simple s)) (List.foldl (fun (acc : A.carrier) (u : B') => A.mul acc (A.basis (M'.toCoxeterSystem.simple u))) init rest) = List.foldl (fun (acc : A.carrier) (u : B') => A.mul acc (A.basis (M'.toCoxeterSystem.simple u))) (A.mul (A.basis (M'.toCoxeterSystem.simple s)) init) rest

Generator left-associativity for repeated foldl multiplication over a list of simple generators: left-multiplying the accumulator by $T_s$ commutes with the fold.

theorem HeckeAlgebra.mul_alt_length_down {B' : Type u_3} {M' : CoxeterMatrix B'} {R' : Type u_4} [CommRing R'] (A : GenericAlgebra M' R') (mul₂ : A.carrier → A.carrier → A.carrier) (h_length_up : ∀ (s : B') (w : M'.Group), M'.toCoxeterSystem.length (M'.toCoxeterSystem.simple s * w) > M'.toCoxeterSystem.length w → mul₂ (A.basis (M'.toCoxeterSystem.simple s)) (A.basis w) = A.basis (M'.toCoxeterSystem.simple s * w)) (h_quadratic : ∀ (s : B'), mul₂ (A.basis (M'.toCoxeterSystem.simple s)) (A.basis (M'.toCoxeterSystem.simple s)) = A.add (A.smul (A.sc.a s) (A.basis (M'.toCoxeterSystem.simple s))) (A.smul (A.sc.b s) (A.basis 1))) (h_identity_left : ∀ (x : A.carrier), mul₂ (A.basis 1) x = x) (h_mul_add_left : ∀ (x y z : A.carrier), mul₂ (A.add x y) z = A.add (mul₂ x z) (mul₂ y z)) (h_smul_mul_left : ∀ (r : R') (x y : A.carrier), mul₂ (A.smul r x) y = A.smul r (mul₂ x y)) (h_gen_left_assoc : ∀ (s : B') (x y : A.carrier), mul₂ (A.basis (M'.toCoxeterSystem.simple s)) (mul₂ x y) = mul₂ (mul₂ (A.basis (M'.toCoxeterSystem.simple s)) x) y) : have cs := M'.toCoxeterSystem; ∀ (s : B') (w : M'.Group), cs.length (cs.simple s * w) < cs.length w → mul₂ (A.basis (cs.simple s)) (A.basis w) = A.add (A.smul (A.sc.a s) (A.basis w)) (A.smul (A.sc.b s) (A.basis (cs.simple s * w)))

Any alternative multiplication mul₂ on the same carrier satisfying the length-up, quadratic, identity, distributivity, scalar, and left-associativity axioms automatically satisfies the length-down rule of $A$.

theorem HeckeAlgebra.mul_alt_gen_eq {B' : Type u_3} {M' : CoxeterMatrix B'} {R' : Type u_4} [CommRing R'] (A : GenericAlgebra M' R') (mul₂ : A.carrier → A.carrier → A.carrier) (h_length_up : ∀ (s : B') (w : M'.Group), M'.toCoxeterSystem.length (M'.toCoxeterSystem.simple s * w) > M'.toCoxeterSystem.length w → mul₂ (A.basis (M'.toCoxeterSystem.simple s)) (A.basis w) = A.basis (M'.toCoxeterSystem.simple s * w)) (h_quadratic : ∀ (s : B'), mul₂ (A.basis (M'.toCoxeterSystem.simple s)) (A.basis (M'.toCoxeterSystem.simple s)) = A.add (A.smul (A.sc.a s) (A.basis (M'.toCoxeterSystem.simple s))) (A.smul (A.sc.b s) (A.basis 1))) (h_identity_left : ∀ (x : A.carrier), mul₂ (A.basis 1) x = x) (h_mul_add_right : ∀ (x y z : A.carrier), mul₂ x (A.add y z) = A.add (mul₂ x y) (mul₂ x z)) (h_mul_add_left : ∀ (x y z : A.carrier), mul₂ (A.add x y) z = A.add (mul₂ x z) (mul₂ y z)) (h_mul_smul_right : ∀ (r : R') (x y : A.carrier), mul₂ x (A.smul r y) = A.smul r (mul₂ x y)) (h_smul_mul_left : ∀ (r : R') (x y : A.carrier), mul₂ (A.smul r x) y = A.smul r (mul₂ x y)) (h_gen_left_assoc : ∀ (s : B') (x y : A.carrier), mul₂ (A.basis (M'.toCoxeterSystem.simple s)) (mul₂ x y) = mul₂ (mul₂ (A.basis (M'.toCoxeterSystem.simple s)) x) y) (s : B') (y : A.carrier) : mul₂ (A.basis (M'.toCoxeterSystem.simple s)) y = A.mul (A.basis (M'.toCoxeterSystem.simple s)) y

An alternative multiplication agrees with $A.\mathrm{mul}$ on products $T_s · y$ for any $y$, under the standard axiom set on mul₂.

theorem HeckeAlgebra.mul_alt_basis_left_eq {B' : Type u_3} {M' : CoxeterMatrix B'} {R' : Type u_4} [CommRing R'] (A : GenericAlgebra M' R') (mul₂ : A.carrier → A.carrier → A.carrier) (h_length_up : ∀ (s : B') (w : M'.Group), M'.toCoxeterSystem.length (M'.toCoxeterSystem.simple s * w) > M'.toCoxeterSystem.length w → mul₂ (A.basis (M'.toCoxeterSystem.simple s)) (A.basis w) = A.basis (M'.toCoxeterSystem.simple s * w)) (h_quadratic : ∀ (s : B'), mul₂ (A.basis (M'.toCoxeterSystem.simple s)) (A.basis (M'.toCoxeterSystem.simple s)) = A.add (A.smul (A.sc.a s) (A.basis (M'.toCoxeterSystem.simple s))) (A.smul (A.sc.b s) (A.basis 1))) (h_identity_left : ∀ (x : A.carrier), mul₂ (A.basis 1) x = x) (h_mul_add_right : ∀ (x y z : A.carrier), mul₂ x (A.add y z) = A.add (mul₂ x y) (mul₂ x z)) (h_mul_add_left : ∀ (x y z : A.carrier), mul₂ (A.add x y) z = A.add (mul₂ x z) (mul₂ y z)) (h_mul_smul_right : ∀ (r : R') (x y : A.carrier), mul₂ x (A.smul r y) = A.smul r (mul₂ x y)) (h_smul_mul_left : ∀ (r : R') (x y : A.carrier), mul₂ (A.smul r x) y = A.smul r (mul₂ x y)) (h_gen_left_assoc : ∀ (s : B') (x y : A.carrier), mul₂ (A.basis (M'.toCoxeterSystem.simple s)) (mul₂ x y) = mul₂ (mul₂ (A.basis (M'.toCoxeterSystem.simple s)) x) y) (w : M'.Group) (y : A.carrier) : mul₂ (A.basis w) y = A.mul (A.basis w) y

An alternative multiplication agrees with $A.\mathrm{mul}$ on $T_w · y$ for every $w$ and $y$, by induction on $\ell(w)$.

theorem HeckeAlgebra.generic_algebra_unique {B' : Type u_3} {M' : CoxeterMatrix B'} {R' : Type u_4} [CommRing R'] (A : GenericAlgebra M' R') (mul₂ : A.carrier → A.carrier → A.carrier) (h_length_up : ∀ (s : B') (w : M'.Group), M'.toCoxeterSystem.length (M'.toCoxeterSystem.simple s * w) > M'.toCoxeterSystem.length w → mul₂ (A.basis (M'.toCoxeterSystem.simple s)) (A.basis w) = A.basis (M'.toCoxeterSystem.simple s * w)) (h_quadratic : ∀ (s : B'), mul₂ (A.basis (M'.toCoxeterSystem.simple s)) (A.basis (M'.toCoxeterSystem.simple s)) = A.add (A.smul (A.sc.a s) (A.basis (M'.toCoxeterSystem.simple s))) (A.smul (A.sc.b s) (A.basis 1))) (h_identity_left : ∀ (x : A.carrier), mul₂ (A.basis 1) x = x) (h_identity_right : ∀ (x : A.carrier), mul₂ x (A.basis 1) = x) (h_mul_add_right : ∀ (x y z : A.carrier), mul₂ x (A.add y z) = A.add (mul₂ x y) (mul₂ x z)) (h_mul_add_left : ∀ (x y z : A.carrier), mul₂ (A.add x y) z = A.add (mul₂ x z) (mul₂ y z)) (h_mul_smul_right : ∀ (r : R') (x y : A.carrier), mul₂ x (A.smul r y) = A.smul r (mul₂ x y)) (h_smul_mul_left : ∀ (r : R') (x y : A.carrier), mul₂ (A.smul r x) y = A.smul r (mul₂ x y)) (h_gen_left_assoc : ∀ (s : B') (x y : A.carrier), mul₂ (A.basis (M'.toCoxeterSystem.simple s)) (mul₂ x y) = mul₂ (mul₂ (A.basis (M'.toCoxeterSystem.simple s)) x) y) (h_gen_right_assoc : ∀ (t : B') (x y : A.carrier), mul₂ (mul₂ x y) (A.basis (M'.toCoxeterSystem.simple t)) = mul₂ x (mul₂ y (A.basis (M'.toCoxeterSystem.simple t)))) (x y : A.carrier) : mul₂ x y = A.mul x y

Uniqueness of the generic Hecke multiplication: any alternative product mul₂ on $A$'s carrier satisfying the same axioms must equal $A.\mathrm{mul}$ on all inputs.