ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generated

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 Frobenius pairing on the four-dimensional Sweedler algebra

Example

Assume $char (k) \neq 2$ and identify the four-dimensional Sweedler Hopf algebra $H_{4}$ with $T_{2}$ using $ζ = - 1$ . Let $λ : H_{4} \to k$ extract the coefficient of $g x$ in the basis $(1, g, x, g x)$ . Then $(a, b) \mapsto λ (a b)$ is an associative nondegenerate pairing, so $H_{4}$ is Frobenius.

Facts & Assumptions

Given: A field $k$ of characteristic different from $2$ , $H_{4} = T_{2}$ with basis $(1, g, x, g x)$ , and $λ$ equal to the $g x$ -coordinate functional.

[F1]

The Taft algebra: PBW basis and Hopf structure: for $N = 2$ and $ζ = - 1$ , $g^{2} = 1$ , $x^{2} = 0$ , $g x = - x g$ , and $(1, g, x, g x)$ is a basis of the Taft algebra.

[F2]

Frobenius functionals and associative pairings: a functional is Frobenius when $(a, b) \mapsto λ (a b)$ is associative and nondegenerate in both variables.

Verification

1.1F1givenalgebra

Using [F1] and the definition of $λ$ , the matrix of $β (a, b) = λ (a b)$ in the ordered basis $(1, g, x, g x)$ in both variables is $M = (\begin{array}{cccc} 0 & 0 & 0 & 1 \\ 0 & 0 & 1 & 0 \\ 0 & - 1 & 0 & 0 \\ 1 & 0 & 0 & 0 \end{array})$ . Indeed the only products with a nonzero $g x$ -coefficient are $1 \cdot g x = g x$ , $g \cdot x = g x$ , $x \cdot g = - g x$ , and $g x \cdot 1 = g x$ .

2.1step 1.1algebra

The displayed matrix is antidiagonal with nonzero antidiagonal entries, so it is invertible; hence both maps $a \mapsto β (a, -)$ and $b \mapsto β (-, b)$ are isomorphisms. The form is associative because $β (a b, c) = λ ((a b) c) = λ (a (b c)) = β (a, b c)$ by associativity in $H_{4}$ .

3.1step 2.1F2∎

By [F2], $λ$ is a Frobenius functional and $H_{4}$ is Frobenius.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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