Documentation

TauCeti.Algebra.TypeAHeckeAlgebra.Infinite

The infinite type-A Hecke algebra and its finite stages #

For a commutative ring R and a unit q : Rˣ, the infinite type-A Hecke algebra InfiniteTypeAHeckeAlgebra R q is the associative unital R-algebra on generators T i, i : ℕ, subject to

It is built as the quotient of FreeAlgebra R ℕ by these relations, which makes the universal property TauCeti.InfiniteTypeAHeckeAlgebra.lift available. The generator T i crosses the strands i and i + 1 (counted from 0), so the algebra is the union of its stages TauCeti.InfiniteTypeAHeckeAlgebra.stage R q n, each a quotient image of the Hecke algebra on n strands. These images are injective (TauCeti.TypeAHeckeAlgebra.toInfinite_injective, in TauCeti.Algebra.TypeAHeckeAlgebra.Embedding), so the union is one of embedded copies. The algebra is the natural carrier of the Ocneanu trace, which is a single linear functional on this union rather than a compatible family of functionals.

Stages #

The stage TauCeti.InfiniteTypeAHeckeAlgebra.stage R q n is the subalgebra generated by the first n - 1 generators T 0, …, T (n - 2), the image of the Hecke algebra on n strands. The stages increase with n (TauCeti.InfiniteTypeAHeckeAlgebra.stage_mono), contain only scalars on at most one strand (TauCeti.InfiniteTypeAHeckeAlgebra.stage_eq_bot_of_le_one), and exhaust the algebra (TauCeti.InfiniteTypeAHeckeAlgebra.iSup_stage). The braid group on n strands maps into the units of the algebra (TauCeti.InfiniteTypeAHeckeAlgebra.braidHom), with image in the stage n (TauCeti.InfiniteTypeAHeckeAlgebra.braidHom_mem_stage), compatibly with adding a last strand, and its image spans the stage as an R-module. Each stage is isomorphic to the Hecke algebra presented on n - 1 generators (TauCeti.TypeAHeckeAlgebra.stageEquiv, in TauCeti.Algebra.TypeAHeckeAlgebra.Embedding), and so is free of rank n!.

As a submodule, the stage of the first n + 2 strands is Hₙ₊₁ + Hₙ₊₁ Tₙ Hₙ₊₁, where Hₙ₊₁ is the stage of the first n + 1 strands (TauCeti.InfiniteTypeAHeckeAlgebra.toSubmodule_stage_add_two). This gives an induction principle for submodules, TauCeti.InfiniteTypeAHeckeAlgebra.eq_top_of_algebraMap_mem_of_mul_T_mul_mem, along which Markov traces are computed recursively.

Shifts and disjoint blocks #

Shifting every strand index by k gives the algebra endomorphism TauCeti.InfiniteTypeAHeckeAlgebra.shift R q k, T i ↦ T (i + k). An element of the stage a lives on the first a strands and the shift by a of any element lives on the strands from a on, so the two commute (TauCeti.InfiniteTypeAHeckeAlgebra.commute_shift_of_mem_stage). Hence placing an element of the stage a on the first a strands and an element of the stage b on the next b strands is an algebra map from the tensor product (TauCeti.InfiniteTypeAHeckeAlgebra.blockIncl). These are the disjoint block maps along which Markov traces are multiplicative; that they are injective, so embeddings, needs the basis theorem and is not proved here.

Main definitions #

Main results #

References #

source
inductive TauCeti.InfiniteTypeAHeckeAlgebra.Rel (R : Type u_1) [CommRing R] (q : Rˣ) :
FreeAlgebra R ℕ → FreeAlgebra R ℕ → Prop

The defining relations of the infinite type-A Hecke algebra with parameter q, as a relation on the free algebra over the generators ℕ: 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 one is imposed for one ordering of the pair, which suffices since the quotient relation is symmetric.

Instances For
    source
    def TauCeti.InfiniteTypeAHeckeAlgebra (R : Type u_1) [CommRing R] (q : Rˣ) :
    Type u_1

    The infinite type-A Hecke algebra over R with parameter q: the free R-algebra on ℕ modulo TauCeti.InfiniteTypeAHeckeAlgebra.Rel. It is the union of its finite stages TauCeti.InfiniteTypeAHeckeAlgebra.stage R q n; see the module docstring for what is proved about them.

    Instances For
      source
      @[instance_reducible]
      instance TauCeti.instRingInfiniteTypeAHeckeAlgebra (R : Type u_1) [CommRing R] (q : Rˣ) :
      Ring (InfiniteTypeAHeckeAlgebra R q)
      source
      @[instance_reducible, instance 900]
      instance TauCeti.InfiniteTypeAHeckeAlgebra.instAlgebra' (R : Type u_1) [CommRing R] (q : Rˣ) {S : Type u_2} [CommSemiring S] [Algebra S R] :
      Algebra S (InfiniteTypeAHeckeAlgebra R q)

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

      source
      @[instance_reducible]
      instance TauCeti.instAlgebraInfiniteTypeAHeckeAlgebra (R : Type u_1) [CommRing R] (q : Rˣ) :
      Algebra R (InfiniteTypeAHeckeAlgebra R q)
      source
      instance TauCeti.instIsScalarTowerInfiniteTypeAHeckeAlgebra (R : Type u_1) [CommRing R] (q : Rˣ) {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 (InfiniteTypeAHeckeAlgebra R q)
      source
      def TauCeti.InfiniteTypeAHeckeAlgebra.mkAlgHom (R : Type u_1) [CommRing R] (q : Rˣ) :
      FreeAlgebra R ℕ →ₐ[R] InfiniteTypeAHeckeAlgebra R q

      The quotient map from the free algebra to the infinite type-A Hecke algebra.

      Instances For
        source
        def TauCeti.InfiniteTypeAHeckeAlgebra.T {R : Type u_1} [CommRing R] (q : Rˣ) (i : ℕ) :
        InfiniteTypeAHeckeAlgebra R q

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

        Instances For
          source
          @[simp]
          theorem TauCeti.InfiniteTypeAHeckeAlgebra.mkAlgHom_ι {R : Type u_1} [CommRing R] {q : Rˣ} (i : ℕ) :
          (mkAlgHom R q) (FreeAlgebra.ι R i) = T q i

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

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

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

          source
          theorem TauCeti.InfiniteTypeAHeckeAlgebra.mkAlgHom_rel {R : Type u_1} [CommRing R] {q : Rˣ} {x y : FreeAlgebra R ℕ} (h : Rel R q x y) :
          (mkAlgHom R q) x = (mkAlgHom R q) y

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

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

          The quadratic relation of a Hecke generator.

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

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

          source
          theorem TauCeti.InfiniteTypeAHeckeAlgebra.T_braid {R : Type u_1} [CommRing R] {q : Rˣ} (i : ℕ) :
          T q i * T q (i + 1) * T q i = T q (i + 1) * T q i * T q (i + 1)

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

          source
          theorem TauCeti.InfiniteTypeAHeckeAlgebra.commute_T {R : Type u_1} [CommRing R] {q : Rˣ} {i j : ℕ} (h : i + 2 ≤ j ∨ j + 2 ≤ i) :
          Commute (T q i) (T q j)

          Two generators on disjoint pairs of strands commute.

          source
          def TauCeti.InfiniteTypeAHeckeAlgebra.unitT {R : Type u_1} [CommRing R] (q : Rˣ) (i : ℕ) :
          (InfiniteTypeAHeckeAlgebra R q)ˣ

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

          Instances For
            source
            @[simp]
            theorem TauCeti.InfiniteTypeAHeckeAlgebra.val_unitT {R : Type u_1} [CommRing R] {q : Rˣ} (i : ℕ) :
            ↑(unitT q i) = T q i

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

            source
            @[simp]
            theorem TauCeti.InfiniteTypeAHeckeAlgebra.val_inv_unitT {R : Type u_1} [CommRing R] {q : Rˣ} (i : ℕ) :
            ↑(unitT q i)⁻¹ = T q i - (algebraMap R (InfiniteTypeAHeckeAlgebra R q)) (↑q - ↑q⁻¹)

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

            source
            theorem TauCeti.InfiniteTypeAHeckeAlgebra.T_sub_val_inv_unitT {R : Type u_1} [CommRing R] {q : Rˣ} (i : ℕ) :
            T q i - ↑(unitT q i)⁻¹ = (algebraMap R (InfiniteTypeAHeckeAlgebra R q)) (↑q - ↑q⁻¹)

            The difference between a generator and its inverse is the Hecke skein scalar.

            source
            theorem TauCeti.InfiniteTypeAHeckeAlgebra.val_inv_unitT_mul_self {R : Type u_1} [CommRing R] {q : Rˣ} (i : ℕ) :
            ↑(unitT q i)⁻¹ * ↑(unitT q i)⁻¹ = -(↑q - ↑q⁻¹) • ↑(unitT q i)⁻¹ + 1

            The inverse of a generator satisfies the quadratic relation with parameter q⁻¹.

            source
            theorem TauCeti.InfiniteTypeAHeckeAlgebra.isUnit_T {R : Type u_1} [CommRing R] {q : Rˣ} (i : ℕ) :
            IsUnit (T q i)

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

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

            The universal property of the infinite type-A Hecke presentation: a sequence in an R-algebra satisfying the quadratic relation, the braid relation for adjacent indices and commutation for distant indices extends to an algebra map out of InfiniteTypeAHeckeAlgebra R q.

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

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

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

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

              source
              theorem TauCeti.InfiniteTypeAHeckeAlgebra.hom_ext_iff {R : Type u_1} [CommRing R] {q : Rˣ} {A : Type u_2} [Semiring A] [Algebra R A] {F G : InfiniteTypeAHeckeAlgebra R q →ₐ[R] A} :
              F = G ↔ ∀ (i : ℕ), F (T q i) = G (T q i)
              source
              theorem TauCeti.InfiniteTypeAHeckeAlgebra.adjoin_range_T {R : Type u_1} [CommRing R] {q : Rˣ} :
              Algebra.adjoin R (Set.range (T q)) = ⊤

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

              source
              def TauCeti.InfiniteTypeAHeckeAlgebra.stage (R : Type u_1) [CommRing R] (q : Rˣ) (n : ℕ) :
              Subalgebra R (InfiniteTypeAHeckeAlgebra R q)

              The stage of the first n strands: the subalgebra generated by the generators T 0, …, T (n - 2) that cross two of the strands 0, …, n - 1. It is the image of the type-A Hecke algebra on n strands.

              Instances For
                source
                theorem TauCeti.InfiniteTypeAHeckeAlgebra.T_mem_stage {R : Type u_1} [CommRing R] {q : Rˣ} {i n : ℕ} (h : i + 1 < n) :
                T q i ∈ stage R q n

                A generator crossing two of the first n strands lies in the stage n.

                source
                theorem TauCeti.InfiniteTypeAHeckeAlgebra.isUnit_mk_T {R : Type u_1} [CommRing R] {q : Rˣ} {i n : ℕ} (h : i + 1 < n) :
                IsUnit ⟨T q i, ⋯⟩

                A generator crossing two of the first n strands is a unit of the stage n: its inverse T i - (q - q⁻¹) lies in the same stage.

                source
                theorem TauCeti.InfiniteTypeAHeckeAlgebra.stage_le_iff {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {S : Subalgebra R (InfiniteTypeAHeckeAlgebra R q)} :
                stage R q n ≤ S ↔ ∀ (i : ℕ), i + 1 < n → T q i ∈ S

                The stage n is contained in a subalgebra exactly when every generator crossing two of the first n strands is.

                source
                theorem TauCeti.InfiniteTypeAHeckeAlgebra.stage_mono {R : Type u_1} [CommRing R] {q : Rˣ} :
                Monotone (stage R q)

                The stages increase with the number of strands.

                source
                theorem TauCeti.InfiniteTypeAHeckeAlgebra.stage_eq_bot_of_le_one {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (h : n ≤ 1) :
                stage R q n = ⊥

                On at most one strand there are no generators, so the stage consists of the scalars.

                source
                theorem TauCeti.InfiniteTypeAHeckeAlgebra.iSup_stage {R : Type u_1} [CommRing R] {q : Rˣ} :
                ⨆ (n : ℕ), stage R q n = ⊤

                The stages exhaust the infinite type-A Hecke algebra.

                source
                theorem TauCeti.InfiniteTypeAHeckeAlgebra.exists_mem_stage {R : Type u_1} [CommRing R] {q : Rˣ} (x : InfiniteTypeAHeckeAlgebra R q) :
                ∃ (n : ℕ), x ∈ stage R q n

                Every element of the infinite type-A Hecke algebra lies in some finite stage.

                source
                theorem TauCeti.InfiniteTypeAHeckeAlgebra.commute_T_of_mem_stage {R : Type u_1} [CommRing R] {q : Rˣ} {i n : ℕ} (h : n ≤ i) {x : InfiniteTypeAHeckeAlgebra R q} (hx : x ∈ stage R q n) :
                Commute (T q i) x

                A generator commutes with the stage of the first n strands when it crosses none of them.

                source
                theorem TauCeti.InfiniteTypeAHeckeAlgebra.exists_mem_stage_and_mem_stage {R : Type u_1} [CommRing R] {q : Rˣ} (x y : InfiniteTypeAHeckeAlgebra R q) :
                ∃ (n : ℕ), x ∈ stage R q (n + 1) ∧ y ∈ stage R q (n + 1)

                Any two elements of the infinite type-A Hecke algebra lie in a common stage with at least one strand.

                source
                theorem TauCeti.InfiniteTypeAHeckeAlgebra.commute_of_mem_stage_two {R : Type u_1} [CommRing R] {q : Rˣ} {x y : InfiniteTypeAHeckeAlgebra R q} (hx : x ∈ stage R q 2) (hy : y ∈ stage R q 2) :
                Commute x y

                The stage of the first two strands is commutative: it is generated by T 0.

                The decomposition Hₙ₊₂ = Hₙ₊₁ + Hₙ₊₁ Tₙ Hₙ₊₁ of the stages #

                source
                theorem TauCeti.InfiniteTypeAHeckeAlgebra.toSubmodule_stage_add_two {R : Type u_1} [CommRing R] {q : Rˣ} (n : ℕ) :
                Subalgebra.toSubmodule (stage R q (n + 2)) = Subalgebra.toSubmodule (stage R q (n + 1)) ⊔ Subalgebra.toSubmodule (stage R q (n + 1)) * (R ∙ T q n) * Subalgebra.toSubmodule (stage R q (n + 1))

                The bimodule decomposition of the stages. As a submodule, the stage of the first n + 2 strands is Hₙ₊₁ + Hₙ₊₁ Tₙ Hₙ₊₁: it is spanned by the stage Hₙ₊₁ of the first n + 1 strands together with the products a * T n * b of the last generator with elements a, b of Hₙ₊₁. This is the decomposition along which Markov traces are determined recursively.

                source
                theorem TauCeti.InfiniteTypeAHeckeAlgebra.toSubmodule_stage_add_two_le_iff {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {P : Submodule R (InfiniteTypeAHeckeAlgebra R q)} :
                Subalgebra.toSubmodule (stage R q (n + 2)) ≤ P ↔ Subalgebra.toSubmodule (stage R q (n + 1)) ≤ P ∧ ∀ a ∈ stage R q (n + 1), ∀ b ∈ stage R q (n + 1), a * T q n * b ∈ P

                To show that the stage of the first n + 2 strands lies in a submodule, it suffices to check the stage of the first n + 1 strands and the products a * T n * b with a, b in it.

                source
                theorem TauCeti.InfiniteTypeAHeckeAlgebra.stage_linearMap_ext {R : Type u_1} [CommRing R] {q : Rˣ} {M : Type u_2} [AddCommMonoid M] [Module R M] {n : ℕ} {f g : ↥(stage R q (n + 2)) →ₗ[R] M} (h₁ : ∀ (b : ↥(stage R q (n + 1))), f ((Subalgebra.inclusion ⋯) b) = g ((Subalgebra.inclusion ⋯) b)) (h₂ : ∀ (a b : ↥(stage R q (n + 1))), f ((Subalgebra.inclusion ⋯) a * ⟨T q n, ⋯⟩ * (Subalgebra.inclusion ⋯) b) = g ((Subalgebra.inclusion ⋯) a * ⟨T q n, ⋯⟩ * (Subalgebra.inclusion ⋯) b)) :
                f = g

                Two linear maps on the stage of the first n + 2 strands agree when they agree on the stage of the first n + 1 strands and on the products a * T n * b with a, b in it.

                source
                theorem TauCeti.InfiniteTypeAHeckeAlgebra.eq_top_of_algebraMap_mem_of_mul_T_mul_mem {R : Type u_1} [CommRing R] {q : Rˣ} {P : Submodule R (InfiniteTypeAHeckeAlgebra R q)} (h₀ : ∀ (r : R), (algebraMap R (InfiniteTypeAHeckeAlgebra R q)) r ∈ P) (h : ∀ (n : ℕ), Subalgebra.toSubmodule (stage R q (n + 1)) ≤ P → ∀ a ∈ stage R q (n + 1), ∀ b ∈ stage R q (n + 1), a * T q n * b ∈ P) :
                P = ⊤

                Induction along the stages. A submodule of the infinite type-A Hecke algebra is everything as soon as it contains the scalars and, whenever it contains the stage of the first n + 1 strands, it contains the products a * T n * b with a, b in that stage.

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

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

                Instances For
                  source
                  @[simp]
                  theorem TauCeti.InfiniteTypeAHeckeAlgebra.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.

                  source
                  theorem TauCeti.InfiniteTypeAHeckeAlgebra.map_braidHom_conj {R : Type u_1} [CommRing R] {q : Rˣ} {τ : InfiniteTypeAHeckeAlgebra R q →ₗ[R] R} (htr : ∀ (x y : InfiniteTypeAHeckeAlgebra R q), τ (x * y) = τ (y * x)) {n : ℕ} (b c : BraidGroup n) :
                  τ ↑((braidHom R q n) (c * b * c⁻¹)) = τ ↑((braidHom R q n) b)

                  Conjugation of a braid does not change its Hecke trace for a tracial linear functional.

                  source
                  theorem LinearMap.map_braidHom_skein {R : Type u_1} [CommRing R] {q : Rˣ} (τ : TauCeti.InfiniteTypeAHeckeAlgebra R q →ₗ[R] R) {n : ℕ} (b c : TauCeti.BraidGroup (n + 1)) (i : Fin n) :
                  τ ↑((TauCeti.InfiniteTypeAHeckeAlgebra.braidHom R q (n + 1)) (b * TauCeti.BraidGroup.sigma i * c)) - τ ↑((TauCeti.InfiniteTypeAHeckeAlgebra.braidHom R q (n + 1)) (b * (TauCeti.BraidGroup.sigma i)⁻¹ * c)) = (↑q - ↑q⁻¹) * τ ↑((TauCeti.InfiniteTypeAHeckeAlgebra.braidHom R q (n + 1)) (b * c))

                  The Hecke skein identity holds for every linear functional, without a trace hypothesis, and in an arbitrary braid context.

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

                  Adding an uncrossed last strand does not change the image of a braid: the braid homomorphisms are compatible with the strand inclusions of the braid groups.

                  source
                  theorem TauCeti.InfiniteTypeAHeckeAlgebra.braidHom_mem_stage {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (b : BraidGroup n) :
                  ↑((braidHom R q n) b) ∈ stage R q n

                  The image of a braid on n strands lies in the stage n.

                  source
                  theorem TauCeti.InfiniteTypeAHeckeAlgebra.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)) = Subalgebra.toSubmodule (stage R q n)

                  The images of the braids on n strands span the stage n as an R-module.

                  source
                  def TauCeti.InfiniteTypeAHeckeAlgebra.shift (R : Type u_1) [CommRing R] (q : Rˣ) (k : ℕ) :
                  InfiniteTypeAHeckeAlgebra R q →ₐ[R] InfiniteTypeAHeckeAlgebra R q

                  The strand shift by k: the algebra endomorphism T i ↦ T (i + k) that moves every braid k strands to the right.

                  Instances For
                    source
                    @[simp]
                    theorem TauCeti.InfiniteTypeAHeckeAlgebra.shift_T {R : Type u_1} [CommRing R] {q : Rˣ} (k i : ℕ) :
                    (shift R q k) (T q i) = T q (i + k)

                    The strand shift by k sends T i to T (i + k).

                    source
                    @[simp]
                    theorem TauCeti.InfiniteTypeAHeckeAlgebra.shift_zero {R : Type u_1} [CommRing R] {q : Rˣ} :
                    shift R q 0 = AlgHom.id R (InfiniteTypeAHeckeAlgebra R q)

                    The strand shift by 0 is the identity.

                    source
                    @[simp]
                    theorem TauCeti.InfiniteTypeAHeckeAlgebra.shift_shift {R : Type u_1} [CommRing R] {q : Rˣ} (a b : ℕ) (x : InfiniteTypeAHeckeAlgebra R q) :
                    (shift R q a) ((shift R q b) x) = (shift R q (a + b)) x

                    Shifting by b and then by a is shifting by a + b.

                    source
                    theorem TauCeti.InfiniteTypeAHeckeAlgebra.shift_mem_stage {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (k : ℕ) {x : InfiniteTypeAHeckeAlgebra R q} (hx : x ∈ stage R q n) :
                    (shift R q k) x ∈ stage R q (n + k)

                    The strand shift by k moves the stage n into the stage n + k.

                    source
                    theorem TauCeti.InfiniteTypeAHeckeAlgebra.isUnit_mk_shift {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (k : ℕ) {x : InfiniteTypeAHeckeAlgebra R q} {hx : x ∈ stage R q n} (h : IsUnit ⟨x, hx⟩) :
                    IsUnit ⟨(shift R q k) x, ⋯⟩

                    The strand shift by k carries a unit of the stage n to a unit of the stage n + k: it is the image under the shift, restricted to an algebra map between the stages.

                    source
                    theorem TauCeti.InfiniteTypeAHeckeAlgebra.shift_mem_adjoin {R : Type u_1} [CommRing R] {q : Rˣ} (k : ℕ) (x : InfiniteTypeAHeckeAlgebra R q) :
                    (shift R q k) x ∈ Algebra.adjoin R (Set.range fun (i : ℕ) => T q (i + k))

                    The image of the strand shift by k is generated by the generators T (i + k).

                    source
                    theorem TauCeti.InfiniteTypeAHeckeAlgebra.commute_shift_of_mem_stage {R : Type u_1} [CommRing R] {q : Rˣ} {a : ℕ} {x : InfiniteTypeAHeckeAlgebra R q} (hx : x ∈ stage R q a) (y : InfiniteTypeAHeckeAlgebra R q) :
                    Commute x ((shift R q a) y)

                    Disjoint blocks commute. An element of the stage a, living on the first a strands, commutes with the shift by a of any element, which lives on the strands from a on.

                    source
                    def TauCeti.InfiniteTypeAHeckeAlgebra.blockIncl (R : Type u_1) [CommRing R] (q : Rˣ) (a b : ℕ) :
                    TensorProduct R ↥(stage R q a) ↥(stage R q b) →ₐ[R] ↥(stage R q (a + b))

                    The disjoint block map: the algebra map from the tensor product of the stages a and b to the stage a + b that places the first factor on the first a strands and the second factor, shifted by a, on the next b strands. It is injective by TauCeti.InfiniteTypeAHeckeAlgebra.blockIncl_injective, proved in TauCeti.Algebra.TypeAHeckeAlgebra.Block.

                    Instances For
                      source
                      @[simp]
                      theorem TauCeti.InfiniteTypeAHeckeAlgebra.coe_blockIncl_tmul {R : Type u_1} [CommRing R] {q : Rˣ} {a b : ℕ} (x : ↥(stage R q a)) (y : ↥(stage R q b)) :
                      ↑((blockIncl R q a b) (x ⊗ₜ[R] y)) = ↑x * (shift R q a) ↑y

                      The disjoint block map multiplies the first factor by the shift of the second.

                      source
                      def TauCeti.InfiniteTypeAHeckeAlgebra.indexCharacter (R : Type u_1) [CommRing R] (q : Rˣ) :
                      InfiniteTypeAHeckeAlgebra R q →ₐ[R] R

                      The index character of the infinite type-A Hecke algebra, the algebra map to the base ring sending every generator to the eigenvalue q.

                      Instances For
                        source
                        def TauCeti.InfiniteTypeAHeckeAlgebra.signCharacter (R : Type u_1) [CommRing R] (q : Rˣ) :
                        InfiniteTypeAHeckeAlgebra R q →ₐ[R] R

                        The sign character of the infinite type-A Hecke algebra, the algebra map to the base ring sending every generator to the eigenvalue -q⁻¹.

                        Instances For
                          source
                          @[simp]
                          theorem TauCeti.InfiniteTypeAHeckeAlgebra.indexCharacter_T {R : Type u_1} [CommRing R] {q : Rˣ} (i : ℕ) :
                          (indexCharacter R q) (T q i) = ↑q

                          The index character sends each generator to q.

                          source
                          @[simp]
                          theorem TauCeti.InfiniteTypeAHeckeAlgebra.signCharacter_T {R : Type u_1} [CommRing R] {q : Rˣ} (i : ℕ) :
                          (signCharacter R q) (T q i) = -↑q⁻¹

                          The sign character sends each generator to -q⁻¹.

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

                          The base ring embeds into the infinite type-A Hecke algebra.

                          source
                          instance TauCeti.InfiniteTypeAHeckeAlgebra.instNontrivial {R : Type u_1} [CommRing R] {q : Rˣ} [Nontrivial R] :
                          Nontrivial (InfiniteTypeAHeckeAlgebra R q)
                          source
                          theorem TauCeti.InfiniteTypeAHeckeAlgebra.T_ne_algebraMap {R : Type u_1} [CommRing R] {q : Rˣ} (hq : ↑q ≠ -↑q⁻¹) (i : ℕ) (r : R) :
                          T q i ≠ (algebraMap R (InfiniteTypeAHeckeAlgebra R q)) r

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