The type-A Hecke algebra on n strands

For a commutative ring R, a unit q : Rˣ and a number of strands n, the type-A Hecke algebra TypeAHeckeAlgebra R q n is the associative unital R-algebra on the n - 1 generators T i, i : Fin (n - 1), subject to

• the quadratic relation T i * T i = (q - q⁻¹) • T i + 1, equivalently (T i - q) * (T i + q⁻¹) = 0,
• the braid relation T i * T j * T i = T j * T i * T j when j = i + 1, and
• distant commutation T i * T j = T j * T i when |i - j| ≥ 2.

The generator T i crosses the strands i and i + 1 (counted from 0), so on at most one strand there are no generators and the algebra is R (TauCeti.TypeAHeckeAlgebra.algEquivOfLeOne). The algebra is built as the quotient of FreeAlgebra R (Fin (n - 1)) by these relations, which makes the universal property TauCeti.TypeAHeckeAlgebra.lift available.

The elementary braids map to the generators, giving a homomorphism from the braid group on n strands to the units (TauCeti.TypeAHeckeAlgebra.braidHom) whose image spans the algebra. Adding an uncrossed last strand gives the tower map TauCeti.TypeAHeckeAlgebra.strandIncl, T i ↦ T i, compatible with the strand inclusions of the braid groups. Adding an uncrossed first strand gives TauCeti.TypeAHeckeAlgebra.tailIncl, T i ↦ T (i + 1). The parameters q and -q give isomorphic algebras by the sign twist T i ↦ -T i (TauCeti.TypeAHeckeAlgebra.negEquiv).

The finite presentation maps onto the stage of the first n strands of the infinite type-A Hecke algebra (TauCeti.TypeAHeckeAlgebra.range_toInfinite), compatibly with the tower maps. That this map is injective, so that the finite presentation is isomorphic to the stage, is proved in TauCeti.Algebra.TypeAHeckeAlgebra.Embedding from the basis theorem.

Main definitions

• TauCeti.TypeAHeckeAlgebra.Rel: the defining relations on the free algebra.
• TauCeti.TypeAHeckeAlgebra: the type-A Hecke algebra on n strands with parameter q.
• TauCeti.TypeAHeckeAlgebra.T: the generators, and TauCeti.TypeAHeckeAlgebra.unitT the same generators as units.
• TauCeti.TypeAHeckeAlgebra.lift: the universal property.
• TauCeti.TypeAHeckeAlgebra.braidHom: the homomorphism from the braid group on n strands to the units.
• TauCeti.TypeAHeckeAlgebra.strandIncl: the tower map from n to n + 1 strands.
• TauCeti.TypeAHeckeAlgebra.castAdd and TauCeti.TypeAHeckeAlgebra.natAdd: the block maps placing the Hecke algebras on a and on b strands on the first a and on the last b of a + b strands.
• TauCeti.TypeAHeckeAlgebra.toInfinite: the map to the infinite type-A Hecke algebra.
• TauCeti.TypeAHeckeAlgebra.negEquiv: the sign twist between parameters q and -q.

Main results

• TauCeti.TypeAHeckeAlgebra.T_mul_self, TauCeti.TypeAHeckeAlgebra.T_braid and TauCeti.TypeAHeckeAlgebra.commute_T: the defining relations.
• TauCeti.TypeAHeckeAlgebra.lift_T and TauCeti.TypeAHeckeAlgebra.hom_ext: the universal property.
• TauCeti.TypeAHeckeAlgebra.span_range_braidHom: the images of the braids span the algebra.
• TauCeti.TypeAHeckeAlgebra.braidHom_strandIncl: the braid homomorphisms are compatible with the tower maps.
• TauCeti.TypeAHeckeAlgebra.range_toInfinite: the image in the infinite algebra is the stage of the first n strands.
• TauCeti.TypeAHeckeAlgebra.commute_castAdd_natAdd, TauCeti.TypeAHeckeAlgebra.toInfinite_castAdd and TauCeti.TypeAHeckeAlgebra.toInfinite_natAdd: the two blocks commute, and in the infinite algebra the right block map is the strand shift.
• TauCeti.TypeAHeckeAlgebra.algebraMap_injective: the presentation does not collapse the scalars.
• TauCeti.TypeAHeckeAlgebra.T_ne_algebraMap: a generator is not a scalar when q ≠ -q⁻¹.

References

• V. F. R. Jones, Hecke algebra representations of braid groups and link polynomials, Ann. of Math. 126 (1987), 335–388, Section 4.
• The quotient presentation and universal-property API follow the construction pattern in Mathlib.LinearAlgebra.CliffordAlgebra.Basic and in TauCeti.InfiniteTypeAHeckeAlgebra.

inductive TauCeti.TypeAHeckeAlgebra.Rel (R : Type u_1) [CommRing R] (q : Rˣ) (n : ℕ) : FreeAlgebra R (Fin (n - 1)) → FreeAlgebra R (Fin (n - 1)) → Prop

The defining relations of the type-A Hecke algebra on n strands with parameter q, as a relation on the free algebra over the generators Fin (n - 1): the quadratic relation T i * T i = (q - q⁻¹) • T i + 1, the braid relation for adjacent generators and commutation of distant generators. The last two are imposed for one ordering of the pair, which suffices since the quotient relation is symmetric.

• mul_self {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (i : Fin (n - 1)) : Rel R q n (FreeAlgebra.ι R i * FreeAlgebra.ι R i) ((↑q - ↑q⁻¹) • FreeAlgebra.ι R i + 1)
• braid {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {i j : Fin (n - 1)} (h : ↑i + 1 = ↑j) : Rel R q n (FreeAlgebra.ι R i * FreeAlgebra.ι R j * FreeAlgebra.ι R i) (FreeAlgebra.ι R j * FreeAlgebra.ι R i * FreeAlgebra.ι R j)
• distant {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {i j : Fin (n - 1)} (h : ↑i + 2 ≤ ↑j) : Rel R q n (FreeAlgebra.ι R i * FreeAlgebra.ι R j) (FreeAlgebra.ι R j * FreeAlgebra.ι R i)

def TauCeti.TypeAHeckeAlgebra (R : Type u_1) [CommRing R] (q : Rˣ) (n : ℕ) : Type u_1

The type-A Hecke algebra over R on n strands with parameter q: the free R-algebra on Fin (n - 1) modulo TauCeti.TypeAHeckeAlgebra.Rel.

@[instance_reducible]

instance TauCeti.instRingTypeAHeckeAlgebra (R : Type u_1) [CommRing R] (q : Rˣ) (n : ℕ) : Ring (TypeAHeckeAlgebra R q n)

@[instance_reducible, instance 900]

instance TauCeti.TypeAHeckeAlgebra.instAlgebra' (R : Type u_1) [CommRing R] (q : Rˣ) (n : ℕ) {S : Type u_2} [CommSemiring S] [Algebra S R] : Algebra S (TypeAHeckeAlgebra R q n)

The type-A Hecke algebra over R is an algebra over every ring that R is an algebra over.

@[instance_reducible]

instance TauCeti.instAlgebraTypeAHeckeAlgebra (R : Type u_1) [CommRing R] (q : Rˣ) (n : ℕ) : Algebra R (TypeAHeckeAlgebra R q n)

instance TauCeti.instIsScalarTowerTypeAHeckeAlgebra (R : Type u_1) [CommRing R] (q : Rˣ) (n : ℕ) {S : Type u_2} {T : Type u_3} [CommSemiring S] [CommSemiring T] [SMul S T] [Algebra S R] [Algebra T R] [IsScalarTower S T R] : IsScalarTower S T (TypeAHeckeAlgebra R q n)

def TauCeti.TypeAHeckeAlgebra.mkAlgHom (R : Type u_1) [CommRing R] (q : Rˣ) (n : ℕ) : FreeAlgebra R (Fin (n - 1)) →ₐ[R] TypeAHeckeAlgebra R q n

The quotient map from the free algebra to the type-A Hecke algebra on n strands.

def TauCeti.TypeAHeckeAlgebra.T {R : Type u_1} [CommRing R] (q : Rˣ) {n : ℕ} (i : Fin (n - 1)) : TypeAHeckeAlgebra R q n

The generator T i of the type-A Hecke algebra on n strands, the image of the elementary braid crossing the strands i and i + 1.

@[simp]

theorem TauCeti.TypeAHeckeAlgebra.mkAlgHom_ι {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (i : Fin (n - 1)) : (mkAlgHom R q n) (FreeAlgebra.ι R i) = T q i

The quotient map takes each free-algebra generator to the corresponding Hecke generator.

theorem TauCeti.TypeAHeckeAlgebra.mkAlgHom_surjective {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} : Function.Surjective ⇑(mkAlgHom R q n)

Every element of the type-A Hecke algebra is represented by a free-algebra element.

theorem TauCeti.TypeAHeckeAlgebra.mkAlgHom_rel {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {x y : FreeAlgebra R (Fin (n - 1))} (h : Rel R q n x y) : (mkAlgHom R q n) x = (mkAlgHom R q n) y

Related elements of the free algebra have the same image in the type-A Hecke algebra.

@[simp]

theorem TauCeti.TypeAHeckeAlgebra.T_mul_self {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (i : Fin (n - 1)) : T q i * T q i = (↑q - ↑q⁻¹) • T q i + 1

The quadratic relation of a Hecke generator.

theorem TauCeti.TypeAHeckeAlgebra.T_sub_algebraMap_mul_T_add_algebraMap_eq_zero {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (i : Fin (n - 1)) : (T q i - (algebraMap R (TypeAHeckeAlgebra R q n)) ↑q) * (T q i + (algebraMap R (TypeAHeckeAlgebra R q n)) ↑q⁻¹) = 0

The quadratic relation in factored form: each generator is annihilated by the polynomial with roots q and -q⁻¹.

theorem TauCeti.TypeAHeckeAlgebra.T_add_algebraMap_mul_self {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (i : Fin (n - 1)) : (T q i + (algebraMap R (TypeAHeckeAlgebra R q n)) ↑q⁻¹) * (T q i + (algebraMap R (TypeAHeckeAlgebra R q n)) ↑q⁻¹) = (↑q + ↑q⁻¹) • (T q i + (algebraMap R (TypeAHeckeAlgebra R q n)) ↑q⁻¹)

The element T i + q⁻¹ is idempotent up to q + q⁻¹.

theorem TauCeti.TypeAHeckeAlgebra.T_braid {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {i j : Fin (n - 1)} (h : ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i) : T q i * T q j * T q i = T q j * T q i * T q j

Two generators on adjacent pairs of strands satisfy the braid relation.

theorem TauCeti.TypeAHeckeAlgebra.commute_T {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {i j : Fin (n - 1)} (h : ↑i + 2 ≤ ↑j ∨ ↑j + 2 ≤ ↑i) : Commute (T q i) (T q j)

Two generators on disjoint pairs of strands commute.

def TauCeti.TypeAHeckeAlgebra.unitT {R : Type u_1} [CommRing R] (q : Rˣ) {n : ℕ} (i : Fin (n - 1)) : (TypeAHeckeAlgebra R q n)ˣ

The generator T i as a unit. Its inverse is T i - (q - q⁻¹), by the quadratic relation.

@[simp]

theorem TauCeti.TypeAHeckeAlgebra.val_unitT {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (i : Fin (n - 1)) : ↑(unitT q i) = T q i

The underlying element of unitT q i is the generator T q i.

@[simp]

theorem TauCeti.TypeAHeckeAlgebra.val_inv_unitT {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (i : Fin (n - 1)) : ↑(unitT q i)⁻¹ = T q i - (algebraMap R (TypeAHeckeAlgebra R q n)) (↑q - ↑q⁻¹)

The inverse of a generator is T i - (q - q⁻¹).

theorem TauCeti.TypeAHeckeAlgebra.isUnit_T {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (i : Fin (n - 1)) : IsUnit (T q i)

Each generator of the type-A Hecke algebra is a unit.

theorem TauCeti.TypeAHeckeAlgebra.commute_inv_unitT {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {i j : Fin (n - 1)} (h : ↑i + 2 ≤ ↑j ∨ ↑j + 2 ≤ ↑i) : Commute ↑(unitT q i)⁻¹ ↑(unitT q j)⁻¹

The inverses of two generators on disjoint pairs of strands commute.

def TauCeti.TypeAHeckeAlgebra.lift {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {A : Type u_2} [Semiring A] [Algebra R A] (f : Fin (n - 1) → A) (hself : ∀ (i : Fin (n - 1)), f i * f i = (↑q - ↑q⁻¹) • f i + 1) (hbraid : ∀ {i j : Fin (n - 1)}, ↑i + 1 = ↑j → f i * f j * f i = f j * f i * f j) (hdist : ∀ {i j : Fin (n - 1)}, ↑i + 2 ≤ ↑j → f i * f j = f j * f i) : TypeAHeckeAlgebra R q n →ₐ[R] A

The universal property of the type-A Hecke presentation on n strands: a family in an R-algebra indexed by Fin (n - 1) satisfying the quadratic relation, the braid relation for adjacent indices and commutation for distant indices extends to an algebra map out of TypeAHeckeAlgebra R q n.

@[simp]

theorem TauCeti.TypeAHeckeAlgebra.lift_T {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {A : Type u_2} [Semiring A] [Algebra R A] (f : Fin (n - 1) → A) (hself : ∀ (i : Fin (n - 1)), f i * f i = (↑q - ↑q⁻¹) • f i + 1) (hbraid : ∀ {i j : Fin (n - 1)}, ↑i + 1 = ↑j → f i * f j * f i = f j * f i * f j) (hdist : ∀ {i j : Fin (n - 1)}, ↑i + 2 ≤ ↑j → f i * f j = f j * f i) (i : Fin (n - 1)) : (lift f hself hbraid hdist) (T q i) = f i

The algebra map built by TauCeti.TypeAHeckeAlgebra.lift takes each generator to its prescribed value.

theorem TauCeti.TypeAHeckeAlgebra.hom_ext {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {A : Type u_2} [Semiring A] [Algebra R A] {F G : TypeAHeckeAlgebra R q n →ₐ[R] A} (h : ∀ (i : Fin (n - 1)), F (T q i) = G (T q i)) : F = G

Two algebra maps out of the type-A Hecke algebra agreeing on the generators are equal.

theorem TauCeti.TypeAHeckeAlgebra.hom_ext_iff {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {A : Type u_2} [Semiring A] [Algebra R A] {F G : TypeAHeckeAlgebra R q n →ₐ[R] A} : F = G ↔ ∀ (i : Fin (n - 1)), F (T q i) = G (T q i)

theorem TauCeti.TypeAHeckeAlgebra.adjoin_range_T {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} : Algebra.adjoin R (Set.range (T q)) = ⊤

The generators generate the type-A Hecke algebra as an R-algebra.

def TauCeti.TypeAHeckeAlgebra.braidHom (R : Type u_1) [CommRing R] (q : Rˣ) (n : ℕ) : BraidGroup n →* (TypeAHeckeAlgebra R q n)ˣ

The homomorphism from the braid group on n strands to the units of the type-A Hecke algebra, sending the elementary braid σ i to the generator T i.

@[simp]

theorem TauCeti.TypeAHeckeAlgebra.braidHom_sigma {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (i : Fin (n - 1)) : (braidHom R q n) (BraidGroup.sigma i) = unitT q i

The braid homomorphism sends each elementary braid to the corresponding generator.

theorem TauCeti.TypeAHeckeAlgebra.span_range_braidHom {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} : Submodule.span R (Set.range fun (b : BraidGroup n) => ↑((braidHom R q n) b)) = ⊤

The images of the braids on n strands span the type-A Hecke algebra as an R-module.

def TauCeti.TypeAHeckeAlgebra.strandIncl (R : Type u_1) [CommRing R] (q : Rˣ) (n : ℕ) : TypeAHeckeAlgebra R q n →ₐ[R] TypeAHeckeAlgebra R q (n + 1)

The tower map of the type-A Hecke algebras, adding an uncrossed last strand: the generator T i on n strands goes to the generator T i on n + 1 strands.

@[simp]

theorem TauCeti.TypeAHeckeAlgebra.strandIncl_T {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (i : Fin (n - 1)) : (strandIncl R q n) (T q i) = T q (Fin.castLE ⋯ i)

The tower map sends each generator to the generator with the same index.

theorem TauCeti.TypeAHeckeAlgebra.strandIncl_T_castSucc {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (i : Fin n) : (strandIncl R q (n + 1)) (T q i) = T q i.castSucc

On a positive number of strands, the generator index under the tower map is castSucc.

theorem TauCeti.TypeAHeckeAlgebra.commute_T_last_strandIncl_strandIncl {R : Type u_1} [CommRing R] {q : Rˣ} (n : ℕ) (x : TypeAHeckeAlgebra R q (n + 1)) : Commute (T q (Fin.last (n + 1))) ((strandIncl R q (n + 2)) ((strandIncl R q (n + 1)) x))

The last generator commutes with every element coming from two stages earlier in the finite Hecke tower.

@[simp]

theorem TauCeti.TypeAHeckeAlgebra.braidHom_strandIncl {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (b : BraidGroup (n + 1)) : ↑((braidHom R q (n + 2)) (BraidGroup.strandIncl b)) = (strandIncl R q (n + 1)) ↑((braidHom R q (n + 1)) b)

Adding an uncrossed last strand to a braid adds an uncrossed last strand to its image: the braid homomorphisms are compatible with the strand inclusions of the braid groups and the tower maps.

def TauCeti.TypeAHeckeAlgebra.tailIncl {R : Type u_1} [CommRing R] (q : Rˣ) (n : ℕ) : TypeAHeckeAlgebra R q n →ₐ[R] TypeAHeckeAlgebra R q (n + 1)

Adding an uncrossed first strand: T i goes to T (i + 1).

@[simp]

theorem TauCeti.TypeAHeckeAlgebra.tailIncl_T {R : Type u_1} [CommRing R] (q : Rˣ) {n : ℕ} (i : Fin (n - 1)) : (tailIncl q n) (T q i) = T q ⟨↑i + 1, ⋯⟩

The shifted-tail inclusion sends each generator to its successor.

theorem TauCeti.TypeAHeckeAlgebra.tailIncl_T_succ {R : Type u_1} [CommRing R] (q : Rˣ) {n : ℕ} (i : Fin n) : (tailIncl q (n + 1)) (T q i) = T q i.succ

In positive rank the generator formula uses the usual Fin.succ index.

def TauCeti.TypeAHeckeAlgebra.toInfinite (R : Type u_1) [CommRing R] (q : Rˣ) (n : ℕ) : TypeAHeckeAlgebra R q n →ₐ[R] InfiniteTypeAHeckeAlgebra R q

The map from the type-A Hecke algebra on n strands to the infinite type-A Hecke algebra, sending each generator to the generator with the same index. Its image is the stage of the first n strands (TauCeti.TypeAHeckeAlgebra.range_toInfinite), and it is injective (TauCeti.TypeAHeckeAlgebra.toInfinite_injective).

@[simp]

theorem TauCeti.TypeAHeckeAlgebra.toInfinite_T {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (i : Fin (n - 1)) : (toInfinite R q n) (T q i) = InfiniteTypeAHeckeAlgebra.T q ↑i

The map to the infinite type-A Hecke algebra sends each generator to the generator with the same index.

theorem TauCeti.TypeAHeckeAlgebra.range_toInfinite {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} : (toInfinite R q n).range = InfiniteTypeAHeckeAlgebra.stage R q n

The image of the type-A Hecke algebra on n strands in the infinite type-A Hecke algebra is the stage of the first n strands.

@[simp]

theorem TauCeti.TypeAHeckeAlgebra.toInfinite_strandIncl {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (x : TypeAHeckeAlgebra R q n) : (toInfinite R q (n + 1)) ((strandIncl R q n) x) = (toInfinite R q n) x

The maps to the infinite type-A Hecke algebra are compatible with the tower maps.

@[simp]

theorem TauCeti.TypeAHeckeAlgebra.toInfinite_tailIncl {R : Type u_1} [CommRing R] (q : Rˣ) (n : ℕ) (x : TypeAHeckeAlgebra R q n) : (toInfinite R q (n + 1)) ((tailIncl q n) x) = (InfiniteTypeAHeckeAlgebra.shift R q 1) ((toInfinite R q n) x)

In the infinite algebra, the shifted-tail inclusion is the shift by one strand.

@[simp]

theorem TauCeti.TypeAHeckeAlgebra.toInfinite_braidHom {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (b : BraidGroup n) : (toInfinite R q n) ↑((braidHom R q n) b) = ↑((InfiniteTypeAHeckeAlgebra.braidHom R q n) b)

The map to the infinite type-A Hecke algebra intertwines the two braid homomorphisms.

theorem TauCeti.TypeAHeckeAlgebra.algebraMap_injective {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} : Function.Injective ⇑(algebraMap R (TypeAHeckeAlgebra R q n))

The presentation does not collapse the scalars: R embeds in the type-A Hecke algebra on any number of strands.

instance TauCeti.TypeAHeckeAlgebra.instNontrivial {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} [Nontrivial R] : Nontrivial (TypeAHeckeAlgebra R q n)

theorem TauCeti.TypeAHeckeAlgebra.T_ne_algebraMap {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (hq : ↑q ≠ -↑q⁻¹) (i : Fin (n - 1)) (r : R) : T q i ≠ (algebraMap R (TypeAHeckeAlgebra R q n)) r

A generator is not a scalar when the two eigenvalues q and -q⁻¹ are distinct.

@[simp]

theorem TauCeti.TypeAHeckeAlgebra.T_ne_zero {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} [Nontrivial R] (i : Fin (n - 1)) : T q i ≠ 0

Over a nontrivial base ring, no generator vanishes.

def TauCeti.TypeAHeckeAlgebra.castAdd (R : Type u_1) [CommRing R] (q : Rˣ) (a b : ℕ) : TypeAHeckeAlgebra R q a →ₐ[R] TypeAHeckeAlgebra R q (a + b)

The left block map: the Hecke algebra on a strands acting on the first a of a + b strands, sending the generator T i to the generator T i.

@[simp]

theorem TauCeti.TypeAHeckeAlgebra.castAdd_T {R : Type u_1} [CommRing R] {q : Rˣ} {a b : ℕ} (i : Fin (a - 1)) : (castAdd R q a b) (T q i) = T q (Fin.castLE ⋯ i)

The left block map sends each generator to the generator with the same index.

def TauCeti.TypeAHeckeAlgebra.natAdd (R : Type u_1) [CommRing R] (q : Rˣ) (a b : ℕ) : TypeAHeckeAlgebra R q b →ₐ[R] TypeAHeckeAlgebra R q (a + b)

The right block map: the Hecke algebra on b strands acting on the last b of a + b strands, sending the generator T j to the generator T (a + j).

@[simp]

theorem TauCeti.TypeAHeckeAlgebra.natAdd_T {R : Type u_1} [CommRing R] {q : Rˣ} {a b : ℕ} (j : Fin (b - 1)) : (natAdd R q a b) (T q j) = T q ⟨a + ↑j, ⋯⟩

The right block map sends the generator T j to the generator T (a + j).

theorem TauCeti.TypeAHeckeAlgebra.commute_castAdd_natAdd {R : Type u_1} [CommRing R] {q : Rˣ} {a b : ℕ} (x : TypeAHeckeAlgebra R q a) (y : TypeAHeckeAlgebra R q b) : Commute ((castAdd R q a b) x) ((natAdd R q a b) y)

The images of the two block maps commute: they act on disjoint blocks of strands.

@[simp]

theorem TauCeti.TypeAHeckeAlgebra.toInfinite_castAdd {R : Type u_1} [CommRing R] {q : Rˣ} {a b : ℕ} (x : TypeAHeckeAlgebra R q a) : (toInfinite R q (a + b)) ((castAdd R q a b) x) = (toInfinite R q a) x

The left block map is compatible with the maps to the infinite type-A Hecke algebra.

@[simp]

theorem TauCeti.TypeAHeckeAlgebra.toInfinite_natAdd {R : Type u_1} [CommRing R] {q : Rˣ} {a b : ℕ} (y : TypeAHeckeAlgebra R q b) : (toInfinite R q (a + b)) ((natAdd R q a b) y) = (InfiniteTypeAHeckeAlgebra.shift R q a) ((toInfinite R q b) y)

In the infinite type-A Hecke algebra, the right block map is the strand shift by a.

theorem TauCeti.TypeAHeckeAlgebra.algebraMap_surjective_of_le_one {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (h : n ≤ 1) : Function.Surjective ⇑(algebraMap R (TypeAHeckeAlgebra R q n))

On at most one strand there are no generators, so every element is a scalar.

noncomputable def TauCeti.TypeAHeckeAlgebra.algEquivOfLeOne (R : Type u_1) [CommRing R] (q : Rˣ) {n : ℕ} (h : n ≤ 1) : R ≃ₐ[R] TypeAHeckeAlgebra R q n

On at most one strand the type-A Hecke algebra is canonically the coefficient ring.

@[simp]

theorem TauCeti.TypeAHeckeAlgebra.algEquivOfLeOne_apply {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (h : n ≤ 1) (r : R) : (algEquivOfLeOne R q h) r = (algebraMap R (TypeAHeckeAlgebra R q n)) r

The identification of the coefficient ring with the type-A Hecke algebra on at most one strand is the structure map.

def TauCeti.TypeAHeckeAlgebra.negEquiv (R : Type u_1) [CommRing R] (q : Rˣ) (n : ℕ) : TypeAHeckeAlgebra R q n ≃ₐ[R] TypeAHeckeAlgebra R (-q) n

The sign twist: the type-A Hecke algebras with parameters q and -q are isomorphic by T i ↦ -T i. Both parameters give the same quadratic relation up to this sign.

@[simp]

theorem TauCeti.TypeAHeckeAlgebra.negEquiv_T {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (i : Fin (n - 1)) : (negEquiv R q n) (T q i) = -T (-q) i

The sign twist sends T i to -T i.

@[simp]

theorem TauCeti.TypeAHeckeAlgebra.negEquiv_symm_T {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (i : Fin (n - 1)) : (negEquiv R q n).symm (T (-q) i) = -T q i

The inverse of the sign twist sends T i to -T i.