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.

A tensor product Hopf algebra from a group and a primitive element

Example

Let $G$ be a group, let $k G$ have its group-algebra Hopf structure, and let $k [x]$ have primitive generator $x$ . The tensor product $T = k G \otimes k [x]$ is a Hopf algebra. For $g, h \in G$ and $i, j, n \geq 0$ , $(g \otimes x^{i}) (h \otimes x^{j}) = g h \otimes x^{i + j}, Δ (g \otimes x^{n}) = \sum_{r = 0}^{n} (\binom{n}{r}) (g \otimes x^{r}) \otimes (g \otimes x^{n - r}), S (g \otimes x^{n}) = g^{- 1} \otimes (- x)^{n} .$ Its counit is $ε (g \otimes x^{n}) = 1$ for $n = 0$ and $0$ for $n > 0$ . In particular $g \otimes 1$ is group-like, $1 \otimes x$ is primitive, and the two tensor factors commute inside $T$ .

Verification

Given: A group $G$ , a field $k$ , the group-algebra Hopf structure on $k G$ , the primitive polynomial Hopf structure on $k [x]$ , and the tensor-product Hopf construction proved on the A page.

[F1] Hopf quotients, kernels of Hopf maps, and tensor products: for Hopf algebras $H, K$ , the coproduct on $H \otimes K$ is $(i d \otimes τ \otimes i d) (Δ_{H} \otimes Δ_{K})$ , the antipode is $S_{H} \otimes S_{K}$ , and both antipode identities hold.

[F2] Group algebras, finite-group function algebras, and polynomial Hopf algebras: group algebras have group-like basis elements and antipode inversion, while $k [x]$ has primitive generator $x$ and antipode $S (x) = - x$ .

1.1givenF1F2algebra

Applying [F1] to these two Hopf algebras gives the tensor-product Hopf structure. The tensor algebra multiplication yields $(g \otimes x^{i}) (h \otimes x^{j}) = g h \otimes x^{i + j}$ , and it also shows that $g \otimes 1$ commutes with $1 \otimes x$ .

2.1step 1.1F1F2algebra

Since $Δ (x) = 1 \otimes x + x \otimes 1$ and the two summands commute in $k [x] \otimes k [x]$ , the binomial theorem gives $Δ (x^{n}) = \sum_{r = 0}^{n} (\binom{n}{r}) x^{r} \otimes x^{n - r}$ . Combining this with $Δ (g) = g \otimes g$ and the flipped middle factors in [F1] gives the displayed formula for $Δ (g \otimes x^{n})$ .

3.1step 1.1step 2.1F1algebra

The tensor antipode in [F1] gives $S (g \otimes x^{n}) = g^{- 1} \otimes (- x)^{n}$ . Directly, for the left antipode product on a basis tensor, $\sum_{r = 0}^{n} (\binom{n}{r}) (g^{- 1} \otimes (- x)^{r}) (g \otimes x^{n - r}) = (1 \otimes x^{n}) \sum_{r = 0}^{n} (\binom{n}{r}) (- 1)^{r},$ which is $1 \otimes 1$ for $n = 0$ and $0$ for $n > 0$ . The right product is $(1 \otimes x^{n}) \sum_{r = 0}^{n} (\binom{n}{r}) (- 1)^{n - r}$ , with the same values. Thus the explicit formulas agree with both antipode equations from [F1].

4.1step 1.1F1F2algebra∎

By [F1], the tensor-product counit is $ε_{k G} \otimes ε_{k [x]}$ . The group-algebra counit has $ε_{k G} (g) = 1$ , while the polynomial counit is a unital algebra map with $ε_{k [x]} (x) = 0$ by [F2], so it takes $1 = x^{0}$ to $1$ and $x^{n}$ to $0$ for $n > 0$ . Therefore $ε (g \otimes x^{n}) = 1$ for $n = 0$ and $0$ for $n > 0$ , as claimed.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

22 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

Kalle Kytölä, Introduction to Hopf algebras and representations, Exercise 28 (standard reference, not scraped)