Type-A Hecke algebras, braid traces, and positive quotients
The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.
TheoremSplit semisimplicity separates the Jucys–Murphy eigenvalues#
Over a commutative ring
without zero divisors, if the unit Q is not 1 and the product ∏_{d=1}^{n} [d]_Q of the
Q-integers [d]_Q = 1 + Q + ⋯ + Q ^ (d - 1) is nonzero, then on every Young diagram of size
less than n the powers Q ^ content c of distinct addable cells are distinct.
YoungDiagram.injOn_zpow_cellContent_of_prod_geom_sum_ne_zero.{u_1} {μ : YoungDiagram} {R : Type u_1}
[CommRing R] [NoZeroDivisors R] {Q : Rˣ} {n : ℕ} (hQ : ↑Q ≠ 1)
(hprod : ∏ d ∈ Finset.Icc 1 n, ∑ i ∈ Finset.range d, ↑Q ^ i ≠ 0) (hμ : μ.card < n) :
Set.InjOn (fun c => ↑(Q ^ YoungDiagram.cellContent c)) {c | μ.IsAddable c}
Lean
Formalized in Tau Ceti as YoungDiagram.injOn_zpow_cellContent_of_prod_geom_sum_ne_zero.
Sources
- Tau Ceti documentation:
YoungDiagram.injOn_zpow_cellContent_of_prod_geom_sum_ne_zero - Source of
YoungDiagram.injOn_zpow_cellContent_of_prod_geom_sum_ne_zeroin TauCeti/Algebra/TypeAHeckeAlgebra/ContentSeparation.lean - Tau Ceti roadmap status: Type-A Hecke algebras, braid traces, and positive quotients
TheoremThe separation criterion is sharp#
The powers Q ^ content c separate the addable cells
of every Young diagram of size less than n if and only if Q ^ d ≠ 1 for 2 ≤ d ≤ n.
YoungDiagram.injOn_zpow_cellContent_iff.{u_1} {G : Type u_1} [Group G] {Q : G} {n : ℕ} :
(∀ (μ : YoungDiagram),
μ.card < n → Set.InjOn (fun c => Q ^ YoungDiagram.cellContent c) {c | μ.IsAddable c}) ↔
∀ (d : ℕ), 2 ≤ d → d ≤ n → Q ^ d ≠ 1
TheoremTauCeti.signedCheckedR_braid#
The braid relation for signed checked R-matrices on two pairs of strands sharing the strand
k, the Yang-Baxter equation for the signed checked R-matrix.
TauCeti.signedCheckedR_braid.{u_1, u_2} {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι]
(pos : ι → Prop) [DecidablePred pos] {n : ℕ} (s : R) {j k l : Fin n} (hjk : j ≠ k) (hkl : k ≠ l)
(hjl : j ≠ l) :
TauCeti.signedCheckedR pos s j k * TauCeti.signedCheckedR pos s k l *
TauCeti.signedCheckedR pos s j k =
TauCeti.signedCheckedR pos s k l * TauCeti.signedCheckedR pos s j k *
TauCeti.signedCheckedR pos s k l
Used by 1
TheoremComparison with the Jimbo R-matrix#
If every letter is positive, the signed checked
R-matrix is the Jimbo R-matrix at the parameter -s, rescaled by -s, on the alphabet with the
reversed order: it is the conjugate of (-s) • T_{-s} on (Fin n → ιᵒᵈ) →₀ R by the relabelling
of words along ι ≃ ιᵒᵈ.
TauCeti.signedCheckedR_eq_jimboGenerator.{u_1, u_2} {R : Type u_1} [CommRing R] {ι : Type u_2}
[LinearOrder ι] (pos : ι → Prop) [DecidablePred pos] {n : ℕ} (s : Rˣ) (hpos : ∀ (a : ι), pos a)
(j k : Fin n) :
TauCeti.signedCheckedR pos (↑s) j k =
(Finsupp.domLCongr ((Equiv.refl (Fin n)).arrowCongr OrderDual.toDual)).symm.conj
(-↑s • TauCeti.KnotTheory.jimboGenerator (-s) j k)
DefinitionThe power-sum basis#
over a ℚ-algebra and in an alphabet of at least n letters, the
power-sum products p_μ of the partitions μ of n form a basis of the symmetric polynomials of
degree n.
TauCeti.psumPartBasis.{u_1, u_2} (σ : Type u_1) [Fintype σ] (R : Type u_2) [CommRing R]
[Algebra ℚ R] {n : ℕ} (hn : n ≤ Fintype.card σ) :
Module.Basis n.Partition R ↥(TauCeti.symmetricHomogeneousSubmodule σ R n)
Uses 1
DefinitionTauCeti.InfiniteTypeAHeckeAlgebra#
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.
TauCeti.InfiniteTypeAHeckeAlgebra.{u_1} (R : Type u_1) [CommRing R] (q : Rˣ) : Type u_1
DefinitionTauCeti.InfiniteTypeAHeckeAlgebra.stage#
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.
TauCeti.InfiniteTypeAHeckeAlgebra.stage.{u_1} (R : Type u_1) [CommRing R] (q : Rˣ) (n : ℕ) :
Subalgebra R (TauCeti.InfiniteTypeAHeckeAlgebra R q)
Uses 1 · Used by 2
DefinitionTauCeti.InfiniteTypeAHeckeAlgebra.shift#
The strand shift by k: the algebra endomorphism T i ↦ T (i + k) that moves every braid
k strands to the right.
TauCeti.InfiniteTypeAHeckeAlgebra.shift.{u_1} (R : Type u_1) [CommRing R] (q : Rˣ) (k : ℕ) :
TauCeti.InfiniteTypeAHeckeAlgebra R q →ₐ[R] TauCeti.InfiniteTypeAHeckeAlgebra R q
Uses 1 · Used by 1
DefinitionTauCeti.InfiniteTypeAHeckeAlgebra.blockIncl#
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. Its injectivity, which would make it an embedding,
needs the basis theorem and is not proved here.
TauCeti.InfiniteTypeAHeckeAlgebra.blockIncl.{u_1} (R : Type u_1) [CommRing R] (q : Rˣ) (a b : ℕ) :
TensorProduct R ↥(TauCeti.InfiniteTypeAHeckeAlgebra.stage R q a)
↥(TauCeti.InfiniteTypeAHeckeAlgebra.stage R q b) →ₐ[R]
↥(TauCeti.InfiniteTypeAHeckeAlgebra.stage R q (a + b))
DefinitionTauCeti.signedCheckedRep#
The signed checked representation of the braid group on the word space (Fin n → ι) →₀ R:
the elementary braid σ i acts by the signed checked R-matrix on the strands i and i + 1.
TauCeti.signedCheckedRep.{u_1, u_2} {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι]
(pos : ι → Prop) [DecidablePred pos] {n : ℕ} (s : Rˣ) :
TauCeti.BraidGroup n →* (Module.End R ((Fin n → ι) →₀ R))ˣ
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.