ExampleConstruction: Literature-sourcedVerification: 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.

Sweedler's four-dimensional Hopf algebra

Example

Let $k$ be a field with $char (k) \neq 2$ . Sweedler's algebra $H_{4}$ has basis $1, g, x, g x$ , relations $g^{2} = 1$ , $x^{2} = 0$ , $g x = - x g$ , and Hopf structure

Δ (g) = g \otimes g, Δ (x) = 1 \otimes x + x \otimes g, ε (g) = 1, ε (x) = 0, S (g) = g, S (x) = - x g = g x .

It is neither commutative nor cocommutative.

Verification

Given: A field $k$ of characteristic different from $2$ .

[F1] The Taft algebra: PBW basis and Hopf structure: for $N > 1$ and a primitive $N$ -th root $ζ$ , the basis $g^{i} x^{j}$ and the stated Hopf maps define the Taft algebra.

[F2] The elementary tensors of two bases form the product basis of the tensor product: if $(b_{i})$ is a basis of $V$ , the tensors $b_{i} \otimes b_{j}$ form a basis of $V \otimes V$ .

1.1givenF1algebra

Take $N = 2$ and $ζ = - 1$ . Since $char (k) \neq 2$ , $- 1$ has order $2$ , so [F1] applies and gives basis $1, g, x, g x$ , relations $g^{2} = 1$ , $x^{2} = 0$ , $g x = - x g$ , and the displayed maps. The relation gives $- x g = g x$ , so the stated value of $S (x)$ has both forms.

2.1step 1.1F1algebra

The algebra is not commutative: $g x$ is a nonzero basis element by [F1], and $g x = - x g$ ; equality $g x = x g$ would imply $2 g x = 0$ , impossible because $2 \neq 0$ and $g x \neq 0$ .

3.1step 1.1F2algebra∎

The coproduct is not cocommutative: $Δ (x) = 1 \otimes x + x \otimes g$ , while its flip is $x \otimes 1 + g \otimes x$ . In the tensor-product basis from [F2], the coefficient of $1 \otimes x$ is $1$ in $Δ (x)$ and $0$ in its flip, so these tensors differ.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

19 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

Andrew Baker, Hopf algebras over fields: an introduction, §3.12 (standard reference, not scraped)