The reversal anti-automorphism of the infinite type-A Hecke algebra

The defining relations of the infinite type-A Hecke algebra are invariant under reading words backwards: the quadratic relation involves a single generator, and the braid and distant-commutation relations are palindromic or symmetric. So there is an R-linear anti-automorphism TauCeti.InfiniteTypeAHeckeAlgebra.reverse fixing every generator T i and reversing the order of products, reverse (x * y) = reverse y * reverse x. It is an involution and preserves every finite stage. On the reduced-word elements T_w it is the anti-involution T_w ↦ T_(w⁻¹), since a reduced word for w read backwards is a reduced word for w⁻¹; that identification is not needed here.

This anti-automorphism exchanges left and right multiplication, so it transports statements about left modules over the stages into statements about right modules. Unlike the real-parameter involution of TauCeti.Algebra.TypeAHeckeAlgebra.Star, it is linear over the coefficients and needs no star structure or hypothesis on q.

Main definitions

• TauCeti.InfiniteTypeAHeckeAlgebra.reverseOp: the reversal as an algebra homomorphism to the opposite algebra.
• TauCeti.InfiniteTypeAHeckeAlgebra.reverse: the reversal as a linear map.
• TauCeti.InfiniteTypeAHeckeAlgebra.reverseOpEquiv: the reversal as an algebra isomorphism with the opposite algebra.
• TauCeti.InfiniteTypeAHeckeAlgebra.stageReverse: its restriction to the stage of the first n strands, as a linear isomorphism.

Main results

• TauCeti.InfiniteTypeAHeckeAlgebra.reverse_T and TauCeti.InfiniteTypeAHeckeAlgebra.reverse_mul: the reversal fixes the generators and reverses products.
• TauCeti.InfiniteTypeAHeckeAlgebra.reverse_reverse: the reversal is an involution.
• TauCeti.InfiniteTypeAHeckeAlgebra.reverse_mem_stage_iff: it preserves the finite stages.

References

• M. Geck and G. Pfeiffer, Characters of Finite Coxeter Groups and Iwahori-Hecke Algebras, OUP (2000), Chapter 4, for the anti-involution T_w ↦ T_(w⁻¹).
• The bundling through the opposite algebra follows CliffordAlgebra.reverseOp and CliffordAlgebra.reverse in Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation.

def TauCeti.InfiniteTypeAHeckeAlgebra.reverseOp {R : Type u_1} [CommRing R] (q : Rˣ) : InfiniteTypeAHeckeAlgebra R q →ₐ[R] (InfiniteTypeAHeckeAlgebra R q)ᵐᵒᵖ

The reversal, as an algebra homomorphism to the opposite algebra: it sends each generator T i to op (T i).

@[simp]

theorem TauCeti.InfiniteTypeAHeckeAlgebra.reverseOp_T {R : Type u_1} [CommRing R] (q : Rˣ) (i : ℕ) : (reverseOp q) (T q i) = MulOpposite.op (T q i)

The reversal fixes every generator.

def TauCeti.InfiniteTypeAHeckeAlgebra.reverse {R : Type u_1} [CommRing R] (q : Rˣ) : InfiniteTypeAHeckeAlgebra R q →ₗ[R] InfiniteTypeAHeckeAlgebra R q

The reversal anti-automorphism of the infinite type-A Hecke algebra: the R-linear map fixing every generator T i and reversing the order of products.

@[simp]

theorem TauCeti.InfiniteTypeAHeckeAlgebra.unop_reverseOp {R : Type u_1} [CommRing R] {q : Rˣ} (x : InfiniteTypeAHeckeAlgebra R q) : MulOpposite.unop ((reverseOp q) x) = (reverse q) x

@[simp]

theorem TauCeti.InfiniteTypeAHeckeAlgebra.op_reverse {R : Type u_1} [CommRing R] {q : Rˣ} (x : InfiniteTypeAHeckeAlgebra R q) : MulOpposite.op ((reverse q) x) = (reverseOp q) x

@[simp]

theorem TauCeti.InfiniteTypeAHeckeAlgebra.reverse_T {R : Type u_1} [CommRing R] {q : Rˣ} (i : ℕ) : (reverse q) (T q i) = T q i

The reversal fixes every generator.

@[simp]

theorem TauCeti.InfiniteTypeAHeckeAlgebra.reverse_algebraMap {R : Type u_1} [CommRing R] {q : Rˣ} (r : R) : (reverse q) ((algebraMap R (InfiniteTypeAHeckeAlgebra R q)) r) = (algebraMap R (InfiniteTypeAHeckeAlgebra R q)) r

The reversal fixes the scalars.

@[simp]

theorem TauCeti.InfiniteTypeAHeckeAlgebra.reverse_one {R : Type u_1} [CommRing R] {q : Rˣ} : (reverse q) 1 = 1

@[simp]

theorem TauCeti.InfiniteTypeAHeckeAlgebra.reverse_mul {R : Type u_1} [CommRing R] {q : Rˣ} (x y : InfiniteTypeAHeckeAlgebra R q) : (reverse q) (x * y) = (reverse q) y * (reverse q) x

The reversal reverses the order of products.

theorem TauCeti.InfiniteTypeAHeckeAlgebra.reverse_list_prod {R : Type u_1} [CommRing R] {q : Rˣ} (l : List (InfiniteTypeAHeckeAlgebra R q)) : (reverse q) l.prod = (List.map (⇑(reverse q)) l).reverse.prod

The reversal of a product of a list is the product of the reversals in the opposite order.

@[simp]

theorem TauCeti.InfiniteTypeAHeckeAlgebra.reverse_reverse {R : Type u_1} [CommRing R] {q : Rˣ} (x : InfiniteTypeAHeckeAlgebra R q) : (reverse q) ((reverse q) x) = x

The reversal is an involution.

theorem TauCeti.InfiniteTypeAHeckeAlgebra.reverse_involutive {R : Type u_1} [CommRing R] {q : Rˣ} : Function.Involutive ⇑(reverse q)

@[simp]

theorem TauCeti.InfiniteTypeAHeckeAlgebra.reverse_comp_reverse {R : Type u_1} [CommRing R] {q : Rˣ} : reverse q ∘ₗ reverse q = LinearMap.id

The reversal is an involution, as a linear map.

def TauCeti.InfiniteTypeAHeckeAlgebra.reverseOpEquiv {R : Type u_1} [CommRing R] (q : Rˣ) : InfiniteTypeAHeckeAlgebra R q ≃ₐ[R] (InfiniteTypeAHeckeAlgebra R q)ᵐᵒᵖ

The reversal, as an algebra isomorphism of the infinite type-A Hecke algebra with its opposite algebra.

@[simp]

theorem TauCeti.InfiniteTypeAHeckeAlgebra.reverseOpEquiv_apply {R : Type u_1} [CommRing R] {q : Rˣ} (x : InfiniteTypeAHeckeAlgebra R q) : (reverseOpEquiv q) x = (reverseOp q) x

@[simp]

theorem TauCeti.InfiniteTypeAHeckeAlgebra.reverseOpEquiv_symm_apply {R : Type u_1} [CommRing R] {q : Rˣ} (x : (InfiniteTypeAHeckeAlgebra R q)ᵐᵒᵖ) : (reverseOpEquiv q).symm x = (reverse q) (MulOpposite.unop x)

The inverse of reverseOpEquiv is the reversal read in the opposite algebra.

@[simp]

theorem TauCeti.InfiniteTypeAHeckeAlgebra.reverse_mem_stage_iff {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {x : InfiniteTypeAHeckeAlgebra R q} : (reverse q) x ∈ stage R q n ↔ x ∈ stage R q n

The reversal preserves the stage of the first n strands.

def TauCeti.InfiniteTypeAHeckeAlgebra.stageReverse {R : Type u_1} [CommRing R] (q : Rˣ) (n : ℕ) : ↥(stage R q n) ≃ₗ[R] ↥(stage R q n)

The reversal restricted to the stage of the first n strands, as a linear isomorphism.

@[simp]

theorem TauCeti.InfiniteTypeAHeckeAlgebra.coe_stageReverse {R : Type u_1} [CommRing R] {q : Rˣ} (n : ℕ) (x : ↥(stage R q n)) : ↑((stageReverse q n) x) = (reverse q) ↑x

Restriction to a stage agrees with the ambient reversal.

@[simp]

theorem TauCeti.InfiniteTypeAHeckeAlgebra.stageReverse_symm {R : Type u_1} [CommRing R] {q : Rˣ} (n : ℕ) : (stageReverse q n).symm = stageReverse q n

The reversal on a stage is its own inverse.