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.

The free Hopf module over the polynomial Hopf algebra

Example

Let $k$ be any field and let $H = k [x]$ have the primitive Hopf structure $Δ (x) = x \otimes 1 + 1 \otimes x$ , $ε (x) = 0$ , and $S (x) = - x$ . For any vector space $V$ , give $V \otimes H$ the free right-right Hopf-module structure. Then $ρ (v \otimes x^{n}) = \sum_{i = 0}^{n} (\binom{n}{i}) (v \otimes x^{i}) \otimes x^{n - i}, P (v \otimes x^{n}) = {\begin{cases} v \otimes 1 & n = 0, \\ 0 & n > 0, \end{cases}$ and $β (v \otimes x^{n}) = (v \otimes 1) \otimes x^{n}$ . The coinvariants are $V \otimes 1$ , in every characteristic.

Facts & Assumptions

Given: A field $k$ , the polynomial algebra $k [x]$ , and a $k$ -vector space $V$ .

[F1]

The free action and coaction are $(v \otimes h) g = v \otimes h g$ and $ρ (v \otimes h) = \sum (v \otimes h_{1}) \otimes h_{2}$ (The free right-right Hopf module on a vector space).

[F2]

The coinvariant projection is $P (m) = \sum m_{0} S (m_{1})$ , and the inverse map is $β (m) = \sum P (m_{0}) \otimes m_{1}$ (The coinvariant projection of a right-right Hopf module, The fundamental theorem of right-right Hopf modules).

[F3]

The Hopf structure uses $ε (x) = 0$ , $ε (1) = 1$ , and the counit identities (Hopf algebras and antipodes); coinvariants in $V \otimes H$ are the range of $v \mapsto v \otimes 1$ (Coinvariants of a free right-right Hopf module).

Verification

1.1givenF3algebra

Define $Δ$ as the algebra map sending $x$ to $x \otimes 1 + 1 \otimes x$ , define $ε$ by $x \mapsto 0$ , and define $S$ by $x \mapsto - x$ . Coassociativity and the counit equations hold on $1$ and $x$ by direct substitution; since both sides are algebra maps from $k [x]$ , the identities hold on all polynomials. Thus the algebra and coalgebra structures satisfy the bialgebra axioms.

2.1F3step 1.1algebra

The binomial theorem gives $Δ (x^{n}) = \sum_{i = 0}^{n} (\binom{n}{i}) x^{i} \otimes x^{n - i}$ . Hence $\sum_{i} (\binom{n}{i}) S (x^{i}) x^{n - i} = (\sum_{i} (\binom{n}{i}) (- 1)^{i}) x^{n}$ and $\sum_{i} (\binom{n}{i}) x^{i} S (x^{n - i}) = (\sum_{i} (\binom{n}{i}) (- 1)^{n - i}) x^{n}$ . Each coefficient is $1$ for $n = 0$ and $0$ for $n > 0$ by $(1 - 1)^{n}$ . These are the two antipode equations on the monomial basis; by linearity they hold on all polynomials, so $k [x]$ is a Hopf algebra in every characteristic.

3.1F1step 2.1

Applying the free coaction in [F1] to the coproduct from step 2.1 yields $ρ (v \otimes x^{n}) = \sum_{i = 0}^{n} (\binom{n}{i}) (v \otimes x^{i}) \otimes x^{n - i}$ .

4.1F3step 3.1

If $z \in (V \otimes k [x])^{co H}$ , apply ${id}_{V} \otimes ε \otimes {id}_{H}$ to $ρ (z) = z \otimes 1$ ; the counit identity gives $z = ({id}_{V} \otimes ε) (z) \otimes 1$ . Conversely every $v \otimes 1$ is coinvariant. Thus the coinvariants equal $V \otimes 1$ , as also recorded by [F3].

4.2F1F2step 3.1algebra

For a monomial, [F2] and step 3.1 give $P (v \otimes x^{n}) = \sum_{i = 0}^{n} (\binom{n}{i}) (v \otimes x^{i}) S (x^{n - i}) = (\sum_{i = 0}^{n} (\binom{n}{i}) (- 1)^{n - i}) v \otimes x^{n}$ . The parenthesized integer is $1$ for $n = 0$ and $0$ for $n > 0$ , proving the stated formula even when $k$ has positive characteristic.

5.1F2step 4.2algebra∎

In $β (v \otimes x^{n}) = \sum_{i} (\binom{n}{i}) P (v \otimes x^{i}) \otimes x^{n - i}$ , step 4.2 makes every term vanish except $i = 0$ , leaving $(v \otimes 1) \otimes x^{n}$ . Applying $α$ gives $v \otimes x^{n}$ . By linearity these formulas hold on finite sums and verify the decomposition.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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