ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck pass

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.

A two-dimensional module and its Taft-algebra dual

Example

Let $N > 1$ , let $k$ be a field with $char (k) ∤ N$ , and fix a primitive $N$ th root of unity $ζ \in k$ . Use the Taft Hopf algebra $T_{N} (k, ζ)$ with generators $g, x$ , relations $g^{N} = 1$ , $x^{N} = 0$ , $g x = ζ x g$ , coproduct $Δ (g) = g \otimes g$ , $Δ (x) = 1 \otimes x + x \otimes g$ , counit $ε (g) = 1$ , $ε (x) = 0$ , and antipode $S (g) = g^{- 1}$ , $S (x) = - x g^{- 1}$ . The example checks a two-dimensional module and computes its left-dual action.

Facts & Assumptions

Given: $N, k, ζ$ and the displayed Taft Hopf algebra structure, a vector space $V = k v_{0} \oplus k v_{1}$ , and the algebraic dual basis $v^{0}, v^{1}$ .

[F1]

The module category of a bialgebra and its tensor action: a left $H$ -module is unital, and tensor products use the coproduct action.

[F2]

The left dual of a finite-dimensional Hopf module: the candidate dual action is $(h \cdot f) (v) = f (S (h) v)$ .

[F3]

Evaluation, coevaluation, and triangle identities for left duals: for finite-dimensional modules, evaluation, coevaluation, and both triangle maps are $H$ -linear/identities.

[F4]

Linear functionals and the algebraic dual $V^{*} = L (V, F)$ defines $V^{*}$ as the space of linear functionals. Here the dual coordinates are $v^{0} (a v_{0} + b v_{1}) = a$ and $v^{1} (a v_{0} + b v_{1}) = b$ , so $v^{i} (v_{j}) = δ_{i j}$ . Linearity gives $f = f (v_{0}) v^{0} + f (v_{1}) v^{1}$ for every $f \in V^{*}$ , so these functionals span $V^{*}$ .

[A1]

The Taft algebra has exactly the displayed generator relations and structural maps; in particular $S (x) = - x g^{- 1}$ .

Verification

Given: The data in Facts & Assumptions.

1.1A1F1givenalgebra

Define $g v_{0} = v_{0}$ , $g v_{1} = ζ^{- 1} v_{1}$ , $x v_{0} = 0$ , and $x v_{1} = v_{0}$ . Since $ζ^{N} = 1$ , $g^{N}$ fixes both basis vectors; since $x^{2} = 0$ and $N > 1$ , $x^{N} = 0$ . On $v_{0}$ , both $g x$ and $ζ x g$ vanish; on $v_{1}$ , $g x v_{1} = g v_{0} = v_{0}$ and $ζ x g v_{1} = ζ x (ζ^{- 1} v_{1}) = v_{0}$ . Thus all defining algebra relations hold, so $V$ is a left $T_{N} (k, ζ)$ -module under the supplied presentation [A1].

2.1A1F2F4step 1.1

The dual action gives $g \cdot v^{0} = v^{0}$ and $g \cdot v^{1} = ζ v^{1}$ , since $S (g) = g^{- 1}$ . Also $x \cdot v^{0} = - ζ v^{1}$ : evaluated on $v_{1}$ it is $v^{0} (S (x) v_{1}) = v^{0} (- x g^{- 1} v_{1}) = - ζ$ , and on $v_{0}$ it is zero. The functional $x \cdot v^{1}$ vanishes on both basis vectors, so $x \cdot v^{1} = 0$ .

3.1A1F3step 2.1algebra

On $v^{0}, v^{1}$ , the dual action satisfies $g^{N} = 1$ and $x^{N} = 0$ . For the cross relation, on $v^{0}$ both $g x$ and $ζ x g$ give $- ζ^{2} v^{1}$ , and on $v^{1}$ both give zero. Hence the displayed action is a left $T_{N} (k, ζ)$ -module action. The module is finite-dimensional, so its evaluation and coevaluation maps satisfy the identities in [F3]; explicitly the coevaluation is $v_{0} \otimes v^{0} + v_{1} \otimes v^{1}$ .

4.1F3F4step 2.1step 3.1∎

Theorem [F3] applies to this finite-dimensional Hopf module and proves the evaluation and coevaluation maps are $H$ -linear. The triangle maps send $v_{j}$ to $\sum_{i} v_{i} v^{i} (v_{j}) = v_{j}$ and $v^{j}$ to $\sum_{i} v^{j} (v_{i}) v^{i} = v^{j}$ by [F4]. Thus the computed dual has the specified evaluation, coevaluation, and triangle identities.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

18 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.