Telescoping strings in a group algebra

Let g and y be elements of a commutative group G. Multiplying the string y + y g⁻¹ + ⋯ + y g⁻⁽ⁿ⁻¹⁾ of basis elements of R[G] by 1 - g⁻¹ telescopes to y - y g⁻ⁿ, and multiplying y g + ⋯ + y gⁿ by 1 - g⁻¹ telescopes to y gⁿ - y. In additive notation, with e^x for the basis element at x, these are the identities (1 - e^{-α}) (e^y + e^{y - α} + ⋯ + e^{y - (n - 1) α}) = e^y - e^{y - n α} and (1 - e^{-α}) (e^{y + α} + ⋯ + e^{y + n α}) = e^{y + n α} - e^y for root strings in the group algebra of a weight lattice.

Main statements

• TauCeti.one_sub_single_inv_mul_sum_div: the descending string telescopes; its additive form is TauCeti.one_sub_single_neg_mul_sum_sub.
• TauCeti.one_sub_single_inv_mul_sum_mul: the ascending string telescopes; its additive form is TauCeti.one_sub_single_neg_mul_sum_add.

theorem TauCeti.one_sub_single_inv_mul_sum_div {R : Type u_1} [Ring R] {G : Type u_2} [CommGroup G] (g y : G) (n : ℕ) : (1 - MonoidAlgebra.single g⁻¹ 1) * ∑ j ∈ Finset.range n, MonoidAlgebra.single (y / g ^ j) 1 = MonoidAlgebra.single y 1 - MonoidAlgebra.single (y / g ^ n) 1

Multiplying the descending string y + y g⁻¹ + ⋯ + y g⁻⁽ⁿ⁻¹⁾ by 1 - g⁻¹ telescopes.

theorem TauCeti.one_sub_single_neg_mul_sum_sub {R : Type u_1} [Ring R] {G : Type u_2} [AddCommGroup G] (g y : G) (n : ℕ) : (1 - AddMonoidAlgebra.single (-g) 1) * ∑ j ∈ Finset.range n, AddMonoidAlgebra.single (y - j • g) 1 = AddMonoidAlgebra.single y 1 - AddMonoidAlgebra.single (y - n • g) 1

Multiplying the descending string e^y + e^{y - α} + ⋯ + e^{y - (n - 1) α} by 1 - e^{-α} telescopes.

theorem TauCeti.one_sub_single_inv_mul_sum_mul {R : Type u_1} [Ring R] {G : Type u_2} [CommGroup G] (g y : G) (n : ℕ) : (1 - MonoidAlgebra.single g⁻¹ 1) * ∑ j ∈ Finset.range n, MonoidAlgebra.single (y * g ^ (j + 1)) 1 = MonoidAlgebra.single (y * g ^ n) 1 - MonoidAlgebra.single y 1

Multiplying the ascending string y g + ⋯ + y gⁿ by 1 - g⁻¹ telescopes.

theorem TauCeti.one_sub_single_neg_mul_sum_add {R : Type u_1} [Ring R] {G : Type u_2} [AddCommGroup G] (g y : G) (n : ℕ) : (1 - AddMonoidAlgebra.single (-g) 1) * ∑ j ∈ Finset.range n, AddMonoidAlgebra.single (y + (j + 1) • g) 1 = AddMonoidAlgebra.single (y + n • g) 1 - AddMonoidAlgebra.single y 1

Multiplying the ascending string e^{y + α} + ⋯ + e^{y + n α} by 1 - e^{-α} telescopes.