LemmaStatement: Literature-sourcedProof: 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.

Right duals and the antipode twist on biduals

Statement

Let $H$ be a Hopf algebra over a field $k$ with antipode $S$ , and assume for the right-dual construction that $S$ is bijective. Let $V$ be a finite-dimensional left $H$ -module and let $V^{*} = {Hom}_{k} (V, k)$ be its algebraic dual. In this page's convention, define the right-dual action on $V^{*}$ by

$(h \cdot f) (v) : = f (S^{- 1} (h) \cdot v),$

with evaluation $\overset{}{ev} : V \otimes V^{*} \to k$ , $v \otimes f \mapsto f (v)$ , and coevaluation $\overset{}{coev} : k \to V^{*} \otimes V$ , $1 \mapsto \sum_{i} e^{i} \otimes e_{i}$ . These maps are $H$ -linear and satisfy the two right-dual triangle identities. The bijectivity hypothesis is used only for this $S^{- 1}$ construction; the left-dual construction earlier on the page needs no such hypothesis.

Let $j_{V} : V \to V^{* *}$ be the ordinary vector-space bidual map, $j_{V} (v) (f) = f (v)$ , where $V^{* *}$ has the twice-applied left-dual action. Then

$h \cdot j_{V} (v) = j_{V} (S^{2} (h) \cdot v) .$

For a fixed finite-dimensional module $V$ , $j_{V}$ is $H$ -linear exactly when $h$ and $S^{2} (h)$ act identically on $V$ for every $h$ . Thus $S^{2} = {i d}_{H}$ is sufficient for $j_{V}$ to be $H$ -linear on every finite-dimensional module. If $H$ itself is finite-dimensional, the converse follows by taking its regular module. If an invertible group-like element $p$ satisfies $S^{2} (h) = p h p^{- 1}$ , then $j_{p, V} (v) : = j_{V} (p \cdot v)$ is a natural monoidal $H$ -module isomorphism $V \to V^{* *}$ on finite-dimensional modules.

Facts & Assumptions

Given: A field $k$ , a Hopf algebra $H$ with antipode $S$ , a bijective $S$ , a finite-dimensional left $H$ -module $V$ , and, for the final assertion, an invertible group-like $p \in H$ with $S^{2} (h) = p h p^{- 1}$ .

[F1]

Evaluation, coevaluation, and triangle identities for left duals: for the left-dual action $h \cdot f (v) = f (S (h) v)$ , $S$ is antimultiplicative, evaluation and coevaluation are $H$ -linear, and the two left-dual triangle identities hold without assuming $S$ bijective.

[F2]

The module category of a bialgebra and its tensor action: tensor products carry the diagonal action from $Δ$ , and the unit module carries the action from $ε$ .

[F3]

Finite tensor duality and basis-independent coevaluation: finite dual bases give canonical tensors corresponding to identity maps, and the vector-space evaluation and coevaluation maps satisfy the two triangle identities.

[F4]

Universal property of the tensor product for balanced maps into abelian groups: bilinear pairings define linear evaluation maps on algebraic tensor products.

[F5]

Linear functionals and the algebraic dual $V^{*} = L (V, F)$ : $V^{*} = {Hom}_{k} (V, k)$ is the space of all $k$ -linear functionals, with pointwise operations.

[A1]

The antipode equations are $\sum S (h_{(1)}) h_{(2)} = ε (h) 1_{H} = \sum h_{(1)} S (h_{(2)})$ , and $S$ is bijective.

[A2]

In the pivot branch, $Δ (p) = p \otimes p$ , $ε (p) = 1$ , $p$ is invertible, and $S^{2} (h) = p h p^{- 1}$ for every $h$ .

Proof

technique · direct

1.1A1F1algebra

Since $S$ is antimultiplicative by [F1] and bijective by [A1], $S^{- 1}$ is also antimultiplicative: applying $S$ to $S^{- 1} (g) S^{- 1} (h)$ gives $h g$ , so injectivity gives $S^{- 1} (h g) = S^{- 1} (g) S^{- 1} (h)$ . Also $S^{- 1} (1_{H}) = 1_{H}$ .

1.2F1F3algebra

For $h \in H$ , $f \in V^{*}$ , $h \cdot j_{V} (v) (f) = j_{V} (v) (S (h) \cdot f) = (S (h) \cdot f) (v) = f (S^{2} (h) v) = j_{V} (S^{2} (h) v) (f)$ . Thus the bidual formula holds. For finite-dimensional $V$ , $j_{V}$ is a vector-space isomorphism by [F3], so it is $H$ -linear exactly when $S^{2} (h) v = h v$ for all $h, v$ . In particular $S^{2} = {i d}_{H}$ suffices for all finite-dimensional modules. If $H$ is finite-dimensional and this condition holds for every finite-dimensional module, apply it to the regular module $H$ and $v = 1_{H}$ to get $S^{2} (h) = h$ .

2.1A1F5step 1.1

For $h, g \in H$ , $v \in V$ , and $f \in V^{*}$ , $1_{H} \cdot f = f$ and $(h \cdot (g \cdot f)) (v) = f (S^{- 1} (g) S^{- 1} (h) v) = f (S^{- 1} (h g) v) = ((h g) \cdot f) (v)$ by step 1.1. Linearity follows from linearity of $S^{- 1}$ , the action on $V$ , and the algebraic dual operations [F5]. Thus $V^{*}$ is a left $H$ -module.

2.2A1step 1.1algebra

Applying $S^{- 1}$ to the two antipode equations in [A1], and using antimultiplicativity of $S^{- 1}$ from step 1.1, yields $\sum S^{- 1} (h_{(2)}) h_{(1)} = ε (h) 1_{H}$ and $\sum h_{(2)} S^{- 1} (h_{(1)}) = ε (h) 1_{H}$ .

2.3A2F2F3step 1.2

Under [A2], $h \cdot j_{p, V} (v) = j_{V} (S^{2} (h) p v) = j_{V} (p h p^{- 1} p v) = j_{V} (p h v) = j_{p, V} (h \cdot v)$ , and $j_{p, V}$ is bijective because both $j_{V}$ and multiplication by $p$ on $V$ are bijective. If $f : V \to W$ is $H$ -linear, then $f (p v) = p f (v)$ , so $j_{p}$ is natural. Finally $p$ acts on $V \otimes W$ by $p \otimes p$ because it is group-like; therefore $j_{p, V \otimes W} (v \otimes w)$ corresponds to $j_{p, V} (v) \otimes j_{p, W} (w)$ under the canonical finite tensor-dual identification [F3]. Since $ε (p) = 1$ , the same compatibility holds on the unit object. Thus $j_{p}$ is monoidal.

3.1F2F4step 2.2

For $v \in V$ and $f \in V^{*}$ , $\overset{}{ev} (h \cdot (v \otimes f)) = \sum f (S^{- 1} (h_{(2)}) h_{(1)} v) = ε (h) f (v) = h \cdot \overset{}{ev} (v \otimes f)$ by the first identity in step 2.2. The bilinear evaluation descends to $V \otimes V^{*}$ by [F4], so it is $H$ -linear.

3.2A1F2F3step 2.2

Let $Θ : V^{*} \otimes V \to {End}_{k} (V)$ send $f \otimes v$ to $[x \mapsto f (x) v]$ . By [F3], $\sum_{i} e^{i} \otimes e_{i}$ corresponds to ${i d}_{V}$ . For $x \in V$ , the image under $Θ$ of $h \cdot \sum_{i} e^{i} \otimes e_{i}$ is $\sum_{i} (h_{(1)} \cdot e^{i}) (x) h_{(2)} e_{i} = \sum h_{(2)} S^{- 1} (h_{(1)}) x = ε (h) x$ by step 2.2 and the dual-basis identity. Hence $h \cdot \overset{}{coev} (1) = ε (h) \overset{}{coev} (1) = \overset{}{coev} (h \cdot 1)$ ; coevaluation is $H$ -linear.

4.1F3step 3.1step 3.2

On $v \in V$ , the first triangle composite gives $\sum_{i} e^{i} (v) e_{i} = v$ ; on $f \in V^{*}$ , the second gives $\sum_{i} f (e_{i}) e^{i} = f$ . These dual-basis expansions prove the two right-dual triangle identities.

5.1A1A2step 4.1step 1.2step 2.3∎

If $V = 0$ , all dual spaces and coevaluation tensors are zero and the identities above are the unique maps on zero spaces. If $V$ is one-dimensional, the dual-basis sums have one term and the same computations apply. Choosing a basis of the given finite-dimensional space uses no arbitrary-index choice. The involutive-antipode implication is proved in step 1.2; its converse is stated only when $H$ is finite-dimensional.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

30 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

P. Etingof, S. Gelaki, D. Nikshych, and V. Ostrik, Tensor Categories (MIT 18.769 full course lecture notes, 2009) (standard reference, not scraped)
Christoph Schweigert, Hopf algebras, quantum groups and topological field theory (Hamburg University full lecture notes, 2025) (standard reference, not scraped)