structure HeckeAlgebra.StructureConstants (B : Type u_3) (R : Type u_4) [CommRing R] : Type (max u_3 u_4)

The pair of scalars $(a_s, b_s)_{s ∈ B}$ defining the quadratic relation $T_s^2 = a_s T_s + b_s T_1$ for a generic Hecke algebra.

• a : B → R
• b : B → R

def HeckeAlgebra.StructureConstants.ConjugacyInvariant {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {R : Type u_3} [CommRing R] (sc : StructureConstants B R) (cs : CoxeterSystem M W) : Prop

The structure constants are conjugacy-invariant if conjugate simple reflections have equal $(a_s, b_s)$ values.

structure HeckeAlgebra.GenericAlgebra {B : Type u_1} (M : CoxeterMatrix B) (R : Type u_4) [CommRing R] : Type (max (max u_1 u_4) (u_5 + 1))

A generic Hecke algebra over $R$ for the Coxeter matrix $M$: an $R$-module carrier with basis $\{T_w : w ∈ W\}$, satisfying the length-up rule $T_s T_w = T_{sw}$ when $\ell(sw) > \ell(w)$, the quadratic relation $T_s^2 = a_s T_s + b_s T_1$, left/right identity for $T_1$, two-sided generator associativity, and a basis-span induction principle.

• carrier : Type u_5
• 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
• sc : StructureConstants B R
• length_up : let cs := M.toCoxeterSystem; ∀ (s : B) (w : M.Group), cs.length (cs.simple s * w) > cs.length w → self.mul (self.basis (cs.simple s)) (self.basis w) = self.basis (cs.simple s * w)
• quadratic : let cs := M.toCoxeterSystem; ∀ (s : B), self.mul (self.basis (cs.simple s)) (self.basis (cs.simple s)) = self.add (self.smul (self.sc.a s) (self.basis (cs.simple s))) (self.smul (self.sc.b s) (self.basis 1))
• 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)
• gen_left_assoc : let cs := M.toCoxeterSystem; ∀ (s : B) (x y : self.carrier), self.mul (self.basis (cs.simple s)) (self.mul x y) = self.mul (self.mul (self.basis (cs.simple s)) x) y
• gen_right_assoc : let cs := M.toCoxeterSystem; ∀ (t : B) (x y : self.carrier), self.mul (self.mul x y) (self.basis (cs.simple t)) = self.mul x (self.mul y (self.basis (cs.simple t)))
• 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

theorem HeckeAlgebra.length_swt_gt_sw {B : Type u_1} {M : CoxeterMatrix B} (cs : CoxeterSystem M M.Group) (s t : B) (w : M.Group) (hsw : cs.length (cs.simple s * w) < cs.length w) (hwt : cs.length (w * cs.simple t) > cs.length w) : cs.length (cs.simple s * w * cs.simple t) > cs.length (cs.simple s * w)

Length inequality used in the right-length-up induction.

theorem HeckeAlgebra.s_mul_swt_eq_wt {B : Type u_1} {M : CoxeterMatrix B} (cs : CoxeterSystem M M.Group) (s t : B) (w : M.Group) : cs.simple s * (cs.simple s * w * cs.simple t) = w * cs.simple t

Cancellation identity $s · (s · w · t) = w · t$ in the Coxeter group.

theorem HeckeAlgebra.GenericAlgebra.SatisfiesLengthDownRule {B : Type u_1} {M : CoxeterMatrix B} {R : Type u_3} [CommRing R] (A : GenericAlgebra M R) : have cs := M.toCoxeterSystem; ∀ (s : B) (w : M.Group), cs.length (cs.simple s * w) < cs.length w → A.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)))

Length-down rule derived from the length-up rule and the quadratic relation: when $\ell(sw) < \ell(w)$, $T_s T_w = a_s T_w + b_s T_{sw}$.

theorem HeckeAlgebra.GenericAlgebra.SatisfiesRightLengthUpRule {B : Type u_1} {M : CoxeterMatrix B} {R : Type u_3} [CommRing R] (A : GenericAlgebra M R) : have cs := M.toCoxeterSystem; ∀ (t : B) (w : M.Group), cs.length (w * cs.simple t) > cs.length w → A.mul (A.basis w) (A.basis (cs.simple t)) = A.basis (w * cs.simple t)

Right-multiplication analogue of the length-up rule: when $\ell(wt) > \ell(w)$, $T_w T_t = T_{wt}$. Proved by induction on $\ell(w)$.

theorem HeckeAlgebra.GenericAlgebra.basis_left_mul_assoc {B : Type u_1} {M : CoxeterMatrix B} {R : Type u_3} [CommRing R] (A : GenericAlgebra M R) : have _cs := M.toCoxeterSystem; ∀ (w : M.Group) (y z : A.carrier), A.mul (A.basis w) (A.mul y z) = A.mul (A.mul (A.basis w) y) z

Left-multiplication by a basis element is associative: $T_w · (y · z) = (T_w · y) · z$. Proved by induction on $\ell(w)$ using gen_left_assoc.

theorem HeckeAlgebra.GenericAlgebra.mul_assoc {B : Type u_1} {M : CoxeterMatrix B} {R : Type u_3} [CommRing R] (A : GenericAlgebra M R) (x y z : A.carrier) : A.mul (A.mul x y) z = A.mul x (A.mul y z)

Full associativity of the generic Hecke product, $(x · y) · z = x · (y · z)$, obtained from basis_left_mul_assoc via the basis-span principle.

theorem HeckeAlgebra.GenericAlgebra.SatisfiesRightLengthDownRule {B : Type u_1} {M : CoxeterMatrix B} {R : Type u_3} [CommRing R] (A : GenericAlgebra M R) : have cs := M.toCoxeterSystem; ∀ (s : B) (w : M.Group), cs.length (w * cs.simple s) < cs.length w → A.mul (A.basis w) (A.basis (cs.simple s)) = A.add (A.smul (A.sc.a s) (A.basis w)) (A.smul (A.sc.b s) (A.basis (w * cs.simple s)))

Right-multiplication length-down rule: when $\ell(ws) < \ell(w)$, $T_w T_s = a_s T_w + b_s T_{ws}$.

structure HeckeAlgebra.IwahoriHeckeData (B : Type u_4) (R : Type u_5) [CommRing R] : Type (max u_4 u_5)

Data of an Iwahori–Hecke specialization: parameters $q_s$ for each simple reflection $s$.

• q : B → R

def HeckeAlgebra.IwahoriHeckeData.toStructureConstants {B : Type u_1} {R : Type u_3} [CommRing R] (d : IwahoriHeckeData B R) : StructureConstants B R

Converts Iwahori–Hecke parameters $q_s$ into the generic structure constants $(a_s, b_s) = (q_s - 1, q_s)$.