structure HeckeAlgebra.HeckeMultiplication {B' : Type u_1} (M : CoxeterMatrix B') (R : Type u_3) [CommRing R] (C : Type u_4) : Type (max (max u_1 u_3) u_4)

Abstract data of a Hecke-algebra multiplication on C over $R$ with basis indexed by $W = M.\mathrm{Group}$: the length-up product $T_s T_w = T_{sw}$ when $\ell(sw) > \ell(w)$, the length-down product $T_s T_w = a_s T_w + b_s T_{sw}$, left-identity, distributivity, scalar associativity, and a span principle on the basis.

• basis : M.Group → C
• smul : R → C → C
• mul : C → C → C
• add : C → C → C
• sc : StructureConstants B' R
• 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)
• 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.sc.a s) (self.basis w)) (self.smul (self.sc.b s) (self.basis (M.toCoxeterSystem.simple s * w)))
• identity_left (x : C) : self.mul (self.basis 1) x = x
• mul_add_right (x y z : C) : self.mul x (self.add y z) = self.add (self.mul x y) (self.mul x z)
• mul_add_left (x y z : C) : self.mul (self.add x y) z = self.add (self.mul x z) (self.mul y z)
• mul_smul_right (r : R) (x y : C) : self.mul x (self.smul r y) = self.smul r (self.mul x y)
• smul_mul_left (r : R) (x y : C) : self.mul (self.smul r x) y = self.smul r (self.mul x y)
• gen_left_assoc (s : B') (x y : C) : self.mul (self.basis (M.toCoxeterSystem.simple s)) (self.mul x y) = self.mul (self.mul (self.basis (M.toCoxeterSystem.simple s)) x) y
• basis_span (P : C → Prop) : (∀ (w : M.Group), P (self.basis w)) → (∀ (x y : C), P x → P y → P (self.add x y)) → (∀ (r : R) (x : C), P x → P (self.smul r x)) → ∀ (z : C), P z

theorem HeckeAlgebra.basis_eq_of_h_basis {B' : Type u_1} {M' : CoxeterMatrix B'} {R' : Type u_2} [CommRing R'] {C : Type u_3} {H₁ H₂ : HeckeMultiplication M' R' C} (h_basis : H₁.basis = H₂.basis) (w : M'.Group) : H₁.basis w = H₂.basis w

If two Hecke multiplications share the same basis function, they agree pointwise on basis elements.

theorem HeckeAlgebra.HeckeMultiplication.mul_gen_basis_eq {B' : Type u_1} {M' : CoxeterMatrix B'} {R' : Type u_2} [CommRing R'] {C : Type u_3} (H₁ H₂ : HeckeMultiplication M' R' C) (h_basis : H₁.basis = H₂.basis) (h_add : H₁.add = H₂.add) (h_smul : H₁.smul = H₂.smul) (h_sc : H₁.sc = H₂.sc) (s : B') (w : M'.Group) : H₁.mul (H₁.basis (M'.toCoxeterSystem.simple s)) (H₁.basis w) = H₂.mul (H₁.basis (M'.toCoxeterSystem.simple s)) (H₁.basis w)

Step in the uniqueness argument: two Hecke multiplications agree on products $T_s · T_w$ where $T_s$ is a simple generator and $T_w$ is any basis element.

theorem HeckeAlgebra.HeckeMultiplication.mul_gen_eq {B' : Type u_1} {M' : CoxeterMatrix B'} {R' : Type u_2} [CommRing R'] {C : Type u_3} (H₁ H₂ : HeckeMultiplication M' R' C) (h_basis : H₁.basis = H₂.basis) (h_add : H₁.add = H₂.add) (h_smul : H₁.smul = H₂.smul) (h_sc : H₁.sc = H₂.sc) (s : B') (z : C) : H₁.mul (H₁.basis (M'.toCoxeterSystem.simple s)) z = H₂.mul (H₁.basis (M'.toCoxeterSystem.simple s)) z

Two Hecke multiplications agree on products $T_s · z$ for any $z ∈ C$, given agreement on basis, addition, scalar action, and structure constants.

theorem HeckeAlgebra.HeckeMultiplication.mul_basis_eq {B' : Type u_1} {M' : CoxeterMatrix B'} {R' : Type u_2} [CommRing R'] {C : Type u_3} (H₁ H₂ : HeckeMultiplication M' R' C) (h_basis : H₁.basis = H₂.basis) (h_add : H₁.add = H₂.add) (h_smul : H₁.smul = H₂.smul) (h_sc : H₁.sc = H₂.sc) (w : M'.Group) (z : C) : H₁.mul (H₁.basis w) z = H₂.mul (H₁.basis w) z

Uniqueness on the basis: under agreement of basis, add, smul, and structure constants, two Hecke multiplications coincide on all products $T_w · z$. The proof proceeds by induction on $\ell(w)$.