Product densities on word spaces

Given weights p : ι → R on an alphabet, the product density TauCeti.productDensity p is the diagonal operator on the word space (Fin n → ι) →₀ R multiplying the basis word w by the product ∏ i, p (w i) of the weights of its letters. These are the tensor powers of the diagonal operator with eigenvalues p, written in the canonical word basis, so no tensor products or choice of basis are needed. They serve as the enhancements and densities of weighted traces of braid and Hecke algebra representations on word spaces.

Main definitions

• TauCeti.productDensity: the product density of a weight function on the word space.

noncomputable def TauCeti.productDensity {R : Type u_1} [CommSemiring R] {ι : Type u_2} {n : ℕ} (p : ι → R) : Module.End R ((Fin n → ι) →₀ R)

The product density of the weights p on the word space: the basis word w is multiplied by ∏ i, p (w i).

@[simp]

theorem TauCeti.productDensity_single_one {R : Type u_1} [CommSemiring R] {ι : Type u_2} {n : ℕ} (p : ι → R) (w : Fin n → ι) : (productDensity p) (Finsupp.single w 1) = (∏ i : Fin n, p (w i)) • Finsupp.single w 1

The product density acts diagonally in the word basis.

@[simp]

theorem TauCeti.productDensity_apply {R : Type u_1} [CommSemiring R] {ι : Type u_2} {n : ℕ} (p : ι → R) (v : (Fin n → ι) →₀ R) (w : Fin n → ι) : ((productDensity p) v) w = (∏ i : Fin n, p (w i)) * v w

The coefficient of a word after applying the product density is its original coefficient multiplied by the product of the weights of its letters.

@[simp]

theorem TauCeti.productDensity_one {R : Type u_1} [CommSemiring R] {ι : Type u_2} {n : ℕ} : productDensity 1 = 1

The product density of the constant weight one is the identity.

theorem TauCeti.productDensity_mul {R : Type u_1} [CommSemiring R] {ι : Type u_2} {n : ℕ} (p p' : ι → R) : productDensity p * productDensity p' = productDensity (p * p')

Composing product densities multiplies their weights.