LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-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.

The type-A quantum presentation admits its displayed antipode

Statement

Let $F = Q (q)$ , let $N \geq 1$ , and let $U_{N}$ be the presented algebra and bialgebra of The type-A quantum algebra and its tensor-action formulas and The type-A quantum presentation descends to its coproduct tensor action. The candidate $\tilde{S}$ of The candidate antipode for the type-A quantum algebra descends to a well-defined $F$ -linear map $S : U_{N} \to U_{N}$ satisfying $S (x y) = S (y) S (x)$ . It obeys

$m (S \otimes id) Δ = u ϵ = m (id \otimes S) Δ .$

Here a Hopf algebra means a unital associative algebra with the coassociative coproduct and counit of a bialgebra and a linear map satisfying these two identities; no bijectivity of $S$ is asserted. Thus $U_{N}$ is a Hopf algebra in this sense.

Facts & Assumptions

Given: $F = Q (q)$ , $N \geq 1$ , the generators and relations of $U_{N}$ , its coproduct and counit, and the candidate $\tilde{S}$ . In step 5.1, $Δ (a) = \sum a_{(1)} \otimes a_{(2)}$ denotes a finite expression for the actual tensor $Δ (a)$ ; each displayed sum is a contraction induced by the algebra multiplication and the specified linear maps, so it does not depend on that expression.

[F1]

The $L_{j}$ commute and $L_{j} L_{j}^{- 1} = L_{j}^{- 1} L_{j} = 1$ (The type-A quantum algebra and its tensor-action formulas).

[F2]

The weights are $L_{j} E_{i} L_{j}^{- 1} = q^{δ_{j, i} - δ_{j, i + 1}} E_{i}$ and $L_{j} F_{i} L_{j}^{- 1} = q^{- δ_{j, i} + δ_{j, i + 1}} F_{i}$ (The type-A quantum algebra and its tensor-action formulas).

[F3]

The mixed commutator relation is $[E_{i}, F_{j}] = δ_{i j} (K_{i} - K_{i}^{- 1}) / (q - q^{- 1})$ (The type-A quantum algebra and its tensor-action formulas).

[F4]

For $∣ i - j ∣ > 1$ the $E_{i}, E_{j}$ and $F_{i}, F_{j}$ commute, and for $∣ i - j ∣ = 1$ both families satisfy the displayed quantum Serre relation (The type-A quantum algebra and its tensor-action formulas).

[F5]

The candidate reverses words and sends $L_{j} \mapsto L_{j}^{- 1}$ , $L_{j}^{- 1} \mapsto L_{j}$ , $E_{i} \mapsto - E_{i} K_{i}^{- 1}$ , and $F_{i} \mapsto - K_{i} F_{i}$ , where $K_{i} = L_{i} L_{i + 1}^{- 1}$ (The candidate antipode for the type-A quantum algebra).

[F6]

A map from the free associative algebra descends through a presentation when it preserves the two-sided ideal generated by the displayed relations; that ideal consists of finite sums $a r b$ with $r$ a defining relation (The free associative R-algebra on a set and descent of relations).

[F7]

The displayed coproduct and counit descend to algebra homomorphisms, the coproduct is coassociative, and both counit identities hold (The type-A quantum presentation descends to its coproduct tensor action).

Proof

Given: The data in [F1]–[F7].

1.1givenF1F2F5algebra

Put $a_{r s} = 2 δ_{r s} - δ_{r, s + 1} - δ_{r + 1, s}$ for $1 \leq r, s < N$ . Multiplying the two $L$ -weight formulas in [F2], and using that the $L_{j}$ commute by [F1], gives $K_{r} E_{s} K_{r}^{- 1} = q^{a_{r s}} E_{s}$ and $K_{r} F_{s} K_{r}^{- 1} = q^{- a_{r s}} F_{s}$ . In particular $a_{r r} = 2$ , $a_{r s} = a_{s r}$ , adjacent distinct indices have $a_{r s} = - 1$ , and nonadjacent distinct indices have $a_{r s} = 0$ . Reversing the words $K_{r} = L_{r} L_{r + 1}^{- 1}$ and $K_{r}^{- 1} = L_{r + 1} L_{r}^{- 1}$ gives $\tilde{S} (K_{r}) = K_{r}^{- 1}$ and $\tilde{S} (K_{r}^{- 1}) = K_{r}$ .

2.1givenF1F2F5step 1.1algebra

The inverse relations map to $L_{j} L_{j}^{- 1} = L_{j}^{- 1} L_{j} = 1$ , and each commutator $L_{j} L_{k} - L_{k} L_{j}$ maps to $L_{k}^{- 1} L_{j}^{- 1} - L_{j}^{- 1} L_{k}^{- 1} = 0$ by [F1]. For $w = δ_{j, i} - δ_{j, i + 1}$ , the positive weight relation maps to $L_{j} (- E_{i} K_{i}^{- 1}) L_{j}^{- 1} - q^{w} (- E_{i} K_{i}^{- 1}) = 0$ , since $L_{j}$ commutes with $K_{i}$ and [F2] gives $L_{j} E_{i} L_{j}^{- 1} = q^{w} E_{i}$ . The negative weight relation maps to $L_{j} (- K_{i} F_{i}) L_{j}^{- 1} - q^{- w} (- K_{i} F_{i}) = 0$ by the same commutation and [F2].

2.2givenF2F3F5step 1.1algebra

Write $C_{i} = (K_{i} - K_{i}^{- 1}) / (q - q^{- 1})$ . By [F5], $S (C_{i}) = - C_{i}$ , so the image of $E_{i} F_{j} - F_{j} E_{i} - δ_{i j} C_{i}$ is $K_{j} F_{j} E_{i} K_{i}^{- 1} - E_{i} K_{i}^{- 1} K_{j} F_{j} + δ_{i j} C_{i}$ . If $i \neq j$ , [F3] gives $F_{j} E_{i} = E_{i} F_{j}$ ; the two first terms become respectively $q^{a_{j i}} E_{i} K_{j} F_{j} K_{i}^{- 1}$ and $q^{a_{i j}} E_{i} K_{j} F_{j} K_{i}^{- 1}$ , which are equal by $a_{i j} = a_{j i}$ . If $i = j$ , then $K_{i} F_{i} E_{i} K_{i}^{- 1} = (K_{i} F_{i} K_{i}^{- 1}) (K_{i} E_{i} K_{i}^{- 1}) = F_{i} E_{i}$ , so the first two terms equal $F_{i} E_{i} - E_{i} F_{i} = - C_{i}$ by [F3] and cancel $+ C_{i}$ . Thus every mixed commutator relation is preserved.

2.3givenF2F4F5step 1.1algebra

If $∣ i - j ∣ > 1$ , then $a_{i j} = a_{j i} = 0$ . Hence $K_{i}, K_{j}$ commute with the opposite-index $E$ and $F$ generators; [F4] gives that the original $E_{i}, E_{j}$ and $F_{i}, F_{j}$ commute. The formulas in [F5] therefore show directly that the images of both distant commutators are zero.

2.4givenF2F4F5step 1.1algebra

Let $γ = q + q^{- 1}$ and take adjacent $i, j$ . Set $X_{r} = E_{r} K_{r}^{- 1}$ and $Y_{r} = K_{r} F_{r}$ . Moving the Cartan factors with the weights from step 1.1 gives $X_{i}^{2} X_{j} = E_{i}^{2} E_{j} K_{i}^{- 2} K_{j}^{- 1}$ , $X_{i} X_{j} X_{i} = E_{i} E_{j} E_{i} K_{i}^{- 2} K_{j}^{- 1}$ , and $X_{j} X_{i}^{2} = E_{j} E_{i}^{2} K_{i}^{- 2} K_{j}^{- 1}$ ; hence the $X$ -Serre polynomial is the original $E$ -Serre polynomial followed by $K_{i}^{- 2} K_{j}^{- 1}$ . The same weight moves give $Y_{i}^{2} Y_{j} = K_{i}^{2} K_{j} F_{i}^{2} F_{j}$ , $Y_{i} Y_{j} Y_{i} = K_{i}^{2} K_{j} F_{i} F_{j} F_{i}$ , and $Y_{j} Y_{i}^{2} = K_{i}^{2} K_{j} F_{j} F_{i}^{2}$ , so the $Y$ -Serre polynomial is $K_{i}^{2} K_{j}$ followed by the original $F$ -Serre polynomial. Both vanish by [F4]. Reversing each cubic word and accounting for its three minus signs gives $\tilde{S} (E_{i}^{2} E_{j} - γ E_{i} E_{j} E_{i} + E_{j} E_{i}^{2}) = - (X_{i}^{2} X_{j} - γ X_{i} X_{j} X_{i} + X_{j} X_{i}^{2})$ and the analogous equality with $F, Y$ ; thus both Serre relations are preserved.

3.1givenF5F6step 2.1step 2.2step 2.3step 2.4algebra

Steps 2.1–2.4 show that the image of every defining relation under $\tilde{S}$ lies in the defining ideal. By [F6] every element of that ideal is a finite sum of terms $a r b$ ; reversal sends each such term to $\tilde{S} (b) \tilde{S} (r) \tilde{S} (a)$ , which remains in the ideal. Therefore $S (a + I) : = \tilde{S} (a) + I$ is well-defined on the quotient and is an anti-algebra map. The empty word maps to $1$ , so $S (1) = 1$ .

4.1givenF5F7step 3.1algebra

On $L_{j}^{\pm 1}$ , both products $S (x_{(1)}) x_{(2)}$ and $x_{(1)} S (x_{(2)})$ equal $1 = ϵ (x) 1$ . On $E_{i}$ , the two products from [F7] are $S (E_{i}) K_{i} + E_{i} = 0$ and $E_{i} S (K_{i}) + S (E_{i}) = 0$ . On $F_{i}$ , they are $S (F_{i}) + S (K_{i}^{- 1}) F_{i} = 0$ and $F_{i} + K_{i}^{- 1} S (F_{i}) = 0$ . Thus both antipode identities hold on every algebra generator and its inverse.

5.1givenF7step 4.1algebra∎

For products $a b$ , anti-multiplicativity and the fact that $Δ, ϵ$ are algebra homomorphisms [F7] give $\sum S (a_{(1)} b_{(1)}) a_{(2)} b_{(2)} = \sum S (b_{(1)}) (S (a_{(1)}) a_{(2)}) b_{(2)} = ϵ (a) ϵ (b) 1$ whenever the left identity holds for $a, b$ ; likewise $\sum a_{(1)} b_{(1)} S (a_{(2)} b_{(2)}) = \sum a_{(1)} (b_{(1)} S (b_{(2)})) S (a_{(2)}) = ϵ (a) ϵ (b) 1$ for the right identity. Induction extends both identities from the generators in step 4.1 to every word, and $F$ -linearity extends them to all of $U_{N}$ . If $N = 1$ , there are no $E_{i}, F_{i}$ or Serre relations, and the same generator checks on $L_{1}^{\pm 1}$ prove the claim.

Depends on

Used by

Nothing in the library uses this result yet.

Cited to discharge well-definedness by The candidate antipode for the type-A quantum algebra.

Dependency tree · two levels

32 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

Pavel Etingof and Mykola Semenyakin, A brief introduction to quantum groups (standard reference, not scraped)