ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Inducing the rank-one Hecke module into type A2

Example

Let $W = S_{3} = ⟨ s_{1}, s_{2} ∣ s_{1}^{2} = s_{2}^{2} = 1, s_{1} s_{2} s_{1} = s_{2} s_{1} s_{2} ⟩$ , let $J = {s_{1}}$ , and let $R = Z [v^{\pm 1}]$ with equal parameter $v$ . Write $a = v - v^{- 1}$ and let $H$ be the generic Hecke algebra with $T_{i}^{2} = a T_{i} + 1$ and $T_{1} T_{2} T_{1} = T_{2} T_{1} T_{2}$ . Let $M = R m$ be the rank-one left $H_{J}$ -module with $T_{1} m = v m$ .

The two coset conventions give different displayed representative sets. The right cosets $W_{J} d$ have minimal representatives $D_{R} (J) = {1, s_{2}, s_{2} s_{1}}$ , and the left cosets $d W_{J}$ have minimal representatives $D_{L} (J) = {1, s_{2}, s_{1} s_{2}}$ . Accordingly,

H = H_{J} \oplus H_{J} T_{2} \oplus H_{J} T_{2} T_{1} as a left H_{J} -module .

H = H_{J} \oplus T_{2} H_{J} \oplus T_{1} T_{2} H_{J} as a right H_{J} -module .

For $H \otimes_{H_{J}} M$ , use the right-module basis and put

b_{0} = 1 \otimes m, b_{1} = T_{2} \otimes m, b_{2} = T_{1} T_{2} \otimes m .

The induced left $H$ -action has matrices, in the ordered basis $(b_{0}, b_{1}, b_{2})$ ,

[T_{1}] = (\begin{array}{ccc} v & 0 & 0 \\ 0 & 0 & 1 \\ 0 & 1 & a \end{array}), [T_{2}] = (\begin{array}{ccc} 0 & 1 & 0 \\ 1 & a & 0 \\ 0 & 0 & v \end{array}) .

Facts & Assumptions

Given: The type-A2 Coxeter system and universal equal-parameter ring above, the rank-one parabolic $J = {s_{1}}$ , and the left $H_{J}$ -module $M = R m$ with $T_{1} m = v m$ .

[F1]

$H_{J}$ is the embedded subalgebra generated by $T_{1}$ , and induction is the balanced tensor product $H \otimes_{H_{J}} M$ . (Parabolic Hecke subalgebras, induction, and restriction)

[F2]

For the right $H_{J}$ -module decomposition, the induced basis is ${T_{d} \otimes m : d \in D_{L} (J)}$ when $M$ has basis ${m}$ . (Parabolic freeness and bases of induced Hecke modules)

[F3]

The Hecke generators satisfy $T_{i}^{2} = (v - v^{- 1}) T_{i} + 1$ and the type-A2 braid relation $T_{1} T_{2} T_{1} = T_{2} T_{1} T_{2}$ . (Universal parameters, the generic Coxeter Hecke algebra and generator conjugacy)

[F4]

The elements $T_{w}$ form an $R$ -basis of $H$ , indexed by $w \in W$ . (The standard basis of the generic Hecke algebra and base change)

Verification

Given: The data in Facts & Assumptions.

1.1F2F4

The six elements of $S_{3}$ are $1, s_{1}, s_{2}, s_{1} s_{2}, s_{2} s_{1}, w_{0} = s_{1} s_{2} s_{1} = s_{2} s_{1} s_{2}$ , with lengths $0, 1, 1, 2, 2, 3$ . Multiplication by $s_{1}$ groups them into the right cosets $W_{J}$ , $W_{J} s_{2}$ , $W_{J} s_{2} s_{1}$ , so the right-coset minimal representatives are $D_{R} (J) = {1, s_{2}, s_{2} s_{1}}$ . Multiplication on the right by $s_{1}$ groups them into the left cosets $W_{J}$ , $s_{2} W_{J}$ , $s_{1} s_{2} W_{J}$ , so the left-coset minimal representatives are $D_{L} (J) = {1, s_{2}, s_{1} s_{2}}$ . The two direct sums in the Example follow from the two sides of [F2].

1.2F1F2F3algebra

The action $T_{1} m = v m$ is well defined because $(v - v) (v + v^{- 1}) m = 0$ . By [F2], $H \otimes_{H_{J}} M$ has basis $(b_{0}, b_{1}, b_{2})$ . The balanced relation moves $T_{1}$ from the first tensor factor to $M$ , so $T_{1} b_{0} = v b_{0}$ ; also $T_{1} b_{1} = b_{2}$ and $T_{1} b_{2} = T_{1}^{2} T_{2} \otimes m = b_{1} + a b_{2}$ by [F3]. For the other generator, $T_{2} b_{0} = b_{1}$ , $T_{2} b_{1} = T_{2}^{2} \otimes m = b_{0} + a b_{1}$ , and $T_{2} b_{2} = T_{2} T_{1} T_{2} \otimes m = T_{1} T_{2} T_{1} \otimes m = v b_{2}$ , using the braid relation and the same balance. These six images give exactly the two displayed matrices.

2.1F3step 1.2algebra

The non-scalar $2 \times 2$ block in each matrix is $C = (\begin{array}{cc} 0 & 1 \\ 1 & a \end{array})$ . Direct multiplication gives $C^{2} = I + a C$ , while the scalar block $v$ satisfies $v^{2} = 1 + a v$ because $a = v - v^{- 1}$ . Hence both matrices satisfy $T_{i}^{2} = 1 + a T_{i}$ .

3.1F3step 1.2algebra∎

On $b_{0}$ , both $T_{1} T_{2} T_{1}$ and $T_{2} T_{1} T_{2}$ give $v b_{2}$ ; on $b_{1}$ , both give $v b_{1} + a v b_{2}$ . On $b_{2}$ , the first gives $v b_{0} + a v b_{1} + (a + a^{2} v) b_{2}$ , while the second gives $v b_{0} + a v b_{1} + a v^{2} b_{2}$ . These agree because $a + a^{2} v = a (1 + a v) = a v^{2}$ . Thus the matrices satisfy the braid relation on a basis, confirming the calculated action.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

21 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Christoph Schönnenbeck, Representations of Iwahori-Hecke Algebras Induced from Parabolic Subalgebras (RWTH Aachen Master's thesis, 2016) (standard reference, not scraped)
Andrew Mathas, Iwahori-Hecke Algebras and Schur Algebras of the Symmetric Group (self-contained notes, 1998; complete 79-page text) (standard reference, not scraped)