Documentation

TauCeti.Algebra.TypeAHeckeAlgebra.Star

The real-parameter involution on type-A Hecke algebras #

For a star-fixed unit parameter in a commutative star ring, InfiniteTypeAHeckeAlgebra has an involution fixing every generator and conjugating scalars. In particular, real nonzero parameters give complex star algebras. The construction descends to the relation quotient by checking the quadratic relation and the reversed braid and distant-commutation relations in the opposite algebra. Its finite stages are invariant under the involution, and strand shifts and the index/sign characters commute with it.

The finite presentation TypeAHeckeAlgebra inherits its involution through toInfinite and stageEquiv. The lemmas TypeAHeckeAlgebra.star_T and TypeAHeckeAlgebra.star_Tw describe its action on generators and PBW vectors; TypeAHeckeAlgebra.toInfinite_star and TypeAHeckeAlgebra.strandIncl_star show that the embedding and tower maps preserve star.

This supplies the algebraic star structure needed to discuss positive traces and self-adjoint elements; no positivity or C*-completion is asserted. The unit-circle convention, in which the generators are unitary rather than self-adjoint, is a different involution and is not constructed here.

The conjugate-opposite construction follows the same Algebra.compHom strategy as TauCeti.QuantumGroups.UqSl2.Star, without importing its quantum-group presentation.

References #

source
@[instance_reducible]
instance TauCeti.InfiniteTypeAHeckeAlgebra.instStarRing {R : Type u_1} [CommRing R] [StarRing R] {q : Rˣ} [hq : Fact (IsSelfAdjoint ↑q)] :
StarRing (InfiniteTypeAHeckeAlgebra R q)

The real-parameter star ring structure: generators are self-adjoint and scalars are conjugated. Requires Fact (IsSelfAdjoint (q : R)), i.e. a star-fixed (e.g. real) parameter.

source
@[simp]
theorem TauCeti.InfiniteTypeAHeckeAlgebra.star_T {R : Type u_1} [CommRing R] [StarRing R] {q : Rˣ} [hq : Fact (IsSelfAdjoint ↑q)] (i : ℕ) :
star (T q i) = T q i

Every generator is self-adjoint in the real-parameter convention.

source
theorem TauCeti.InfiniteTypeAHeckeAlgebra.star_val_inv_unitT {R : Type u_1} [CommRing R] [StarRing R] {q : Rˣ} [hq : Fact (IsSelfAdjoint ↑q)] (i : ℕ) :
star ↑(unitT q i)⁻¹ = ↑(unitT q i)⁻¹

The inverse of every generator is self-adjoint in the real-parameter convention.

source
instance TauCeti.InfiniteTypeAHeckeAlgebra.instStarModule {R : Type u_1} [CommRing R] [StarRing R] {q : Rˣ} [hq : Fact (IsSelfAdjoint ↑q)] :
StarModule R (InfiniteTypeAHeckeAlgebra R q)

The real-parameter involution is conjugate-linear over the coefficient ring.

source
theorem TauCeti.InfiniteTypeAHeckeAlgebra.map_star_iff {R : Type u_1} [CommRing R] [StarRing R] {q : Rˣ} [hq : Fact (IsSelfAdjoint ↑q)] {A : Type u_2} [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] {F : InfiniteTypeAHeckeAlgebra R q →ₐ[R] A} :
(∀ (x : InfiniteTypeAHeckeAlgebra R q), F (star x) = star (F x)) ↔ ∀ (i : ℕ), IsSelfAdjoint (F (T q i))

An algebra map out of the real-parameter Hecke algebra preserves star exactly when its generator images are self-adjoint. Thus its presentation also has the expected universal property as a star algebra.

source
@[simp]
theorem TauCeti.InfiniteTypeAHeckeAlgebra.star_mem_stage_iff {R : Type u_1} [CommRing R] [StarRing R] {q : Rˣ} [hq : Fact (IsSelfAdjoint ↑q)] {n : ℕ} {x : InfiniteTypeAHeckeAlgebra R q} :
star x ∈ stage R q n ↔ x ∈ stage R q n

Every finite stage is invariant under the real-parameter involution.

source
@[simp]
theorem TauCeti.InfiniteTypeAHeckeAlgebra.shift_star {R : Type u_1} [CommRing R] [StarRing R] {q : Rˣ} [hq : Fact (IsSelfAdjoint ↑q)] (k : ℕ) (x : InfiniteTypeAHeckeAlgebra R q) :
(shift R q k) (star x) = star ((shift R q k) x)

Shifting all generator labels commutes with the involution.

source
@[simp]
theorem TauCeti.InfiniteTypeAHeckeAlgebra.indexCharacter_star {R : Type u_1} [CommRing R] [StarRing R] {q : Rˣ} [hq : Fact (IsSelfAdjoint ↑q)] (x : InfiniteTypeAHeckeAlgebra R q) :
(indexCharacter R q) (star x) = star ((indexCharacter R q) x)

The scalar character sending every generator to q preserves the involution.

source
@[simp]
theorem TauCeti.InfiniteTypeAHeckeAlgebra.signCharacter_star {R : Type u_1} [CommRing R] [StarRing R] {q : Rˣ} [hq : Fact (IsSelfAdjoint ↑q)] (x : InfiniteTypeAHeckeAlgebra R q) :
(signCharacter R q) (star x) = star ((signCharacter R q) x)

The scalar character sending every generator to -q⁻¹ preserves the involution.

source
@[instance_reducible]
noncomputable instance TauCeti.TypeAHeckeAlgebra.instStarRing {R : Type u_1} [CommRing R] [StarRing R] {q : Rˣ} {n : ℕ} [Fact (IsSelfAdjoint ↑q)] :
StarRing (TypeAHeckeAlgebra R q n)

For a star-fixed parameter, the finite Hecke algebra is a star ring with self-adjoint simple generators.

source
@[simp]
theorem TauCeti.TypeAHeckeAlgebra.toInfinite_star {R : Type u_1} [CommRing R] [StarRing R] {q : Rˣ} {n : ℕ} [Fact (IsSelfAdjoint ↑q)] (x : TypeAHeckeAlgebra R q n) :
(toInfinite R q n) (star x) = star ((toInfinite R q n) x)

The finite-to-infinite embedding preserves the real-parameter involution.

source
@[simp]
theorem TauCeti.TypeAHeckeAlgebra.star_T {R : Type u_1} [CommRing R] [StarRing R] {q : Rˣ} {n : ℕ} [Fact (IsSelfAdjoint ↑q)] (i : Fin (n - 1)) :
star (T q i) = T q i

Simple generators of the finite presentation are self-adjoint.

source
instance TauCeti.TypeAHeckeAlgebra.instStarModule {R : Type u_1} [CommRing R] [StarRing R] {q : Rˣ} {n : ℕ} [Fact (IsSelfAdjoint ↑q)] :
StarModule R (TypeAHeckeAlgebra R q n)

The finite involution conjugates coefficients.

source
@[simp]
theorem TauCeti.TypeAHeckeAlgebra.strandIncl_star {R : Type u_1} [CommRing R] [StarRing R] {q : Rˣ} {n : ℕ} [Fact (IsSelfAdjoint ↑q)] (x : TypeAHeckeAlgebra R q n) :
(strandIncl R q n) (star x) = star ((strandIncl R q n) x)

The unit-preserving tower maps preserve the real-parameter involutions.

source
@[simp]
theorem TauCeti.TypeAHeckeAlgebra.star_Tw {R : Type u_1} [CommRing R] [StarRing R] {q : Rˣ} {n : ℕ} [Fact (IsSelfAdjoint ↑q)] {W : Type u_2} [Group W] (cs : CoxeterSystem (CoxeterMatrix.A (n - 1)) W) (w : W) :
star (Tw q cs w) = Tw q cs w⁻¹

The real-parameter involution sends the PBW vector T_w to T_(w⁻¹).