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 a group algebra

Example

Let $G$ be any group, $k$ a field, and $V$ a $k$ -vector space. Write $k G$ for the vector space of finite formal sums of elements of $G$ , with multiplication extended from $G$ . Give it the Hopf structure $Δ (g) = g \otimes g$ , $ε (g) = 1$ , and $S (g) = g^{- 1}$ on each $g \in G$ . On $V \otimes k G$ use the free action and coaction. Then its coinvariants are $V \otimes 1$ , $P (v \otimes g) = v \otimes 1$ , and the inverse decomposition sends $v \otimes g$ to $(v \otimes 1) \otimes g$ .

Facts & Assumptions

Given: A group $G$ , a field $k$ , and a $k$ -vector space $V$ .

[F1]

A right-right Hopf module has compatibility $ρ (x h) = \sum x_{0} h_{1} \otimes x_{1} h_{2}$ and coinvariants $ρ (x) = x \otimes 1$ (Right-right Hopf modules and coinvariants).

[F2]

The free structure on $V \otimes H$ is $(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).

[F3]

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

Verification

1.1givenalgebra

Multiplication on $k G$ is associative and unital because the group multiplication is; on each basis element, $Δ (g h) = g h \otimes g h = (g \otimes g) (h \otimes h)$ and $ε (g h) = 1 = ε (g) ε (h)$ . Coassociativity and both counit identities hold on $g$ since $Δ (g) = g \otimes g$ and $ε (g) = 1$ . Finally, $g S (g) = g g^{- 1} = 1 = S (g) g$ , so both antipode equations hold on each basis vector. All structure identities extend by linearity or bilinearity to finite sums, making $k G$ a Hopf algebra.

1.2F1F2algebra

Every $z \in V \otimes k G$ has finite support and can be written $z = \sum_{g} v_{g} \otimes g$ ; the coefficients are unique because applying ${id}_{V} \otimes δ_{g}$ , where $δ_{g}$ extracts the $g$ -coefficient, recovers $v_{g}$ . If $z$ is coinvariant, then $\sum_{g} v_{g} \otimes g \otimes g = \sum_{g} v_{g} \otimes g \otimes e$ . Applying ${id}_{V} \otimes δ_{g} \otimes δ_{g}$ shows $v_{g} = 0$ for $g \neq e$ . Conversely $v \otimes e$ is coinvariant, so the coinvariants are exactly $V \otimes e$ .

2.1F1F2step 1.1

For $v \in V$ and $g, a \in G$ , the free structure gives $ρ ((v \otimes g) a) = ρ (v \otimes g a) = (v \otimes g a) \otimes g a$ , while the compatibility right side is $(v \otimes g) a \otimes g a = (v \otimes g a) \otimes g a$ . Bilinearity extends this equality to every $h \in k G$ , so the pair is a Hopf module.

3.1F2F3step 1.2step 2.1∎

For a basis tensor $v \otimes g$ , $P (v \otimes g) = (v \otimes g) g^{- 1} = v \otimes e$ . Hence $β (v \otimes g) = (v \otimes e) \otimes g$ and $α ((v \otimes e) \otimes g) = v \otimes g$ . Finite-sum linearity gives the formulas on every element; these are the projection and inverse decomposition from [F3].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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