LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-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 right-right Hopf module on a vector space

Statement

Let $k$ be a field, $H$ a Hopf algebra over $k$ , and $V$ any $k$ -vector space. On $V \otimes H$ define

(v \otimes h) g : = v \otimes h g, ρ (v \otimes h) : = \sum (v \otimes h_{1}) \otimes h_{2} .

These maps make $V \otimes H$ a right-right Hopf module. No finite-dimensionality or choice of basis for $V$ is needed.

Facts & Assumptions

Given: A field $k$ , a Hopf algebra $H$ over $k$ , and a $k$ -vector space $V$ .

[F1]

A bialgebra has a unital associative algebra structure and a counital coassociative coalgebra structure (Bialgebras and bialgebra maps).

[F2]

The coproduct and counit are unital algebra homomorphisms, so $Δ (h g) = \sum h_{1} g_{1} \otimes h_{2} g_{2}$ (Bialgebras and bialgebra maps).

[F3]

Tensor products are algebraic; their elements are finite sums of elementary tensors and multilinear formulas define linear maps on them (Scalars, tensor powers, the empty tensor, opposite algebras and finite sums).

[F4]

A right-right Hopf module is a right module and right comodule satisfying $ρ (x g) = \sum x_{0} g_{1} \otimes x_{1} g_{2}$ (Right-right Hopf modules and coinvariants).

Proof

1.1givenF1F3construct

For each $g \in H$ , the formula $(v \otimes h) g = v \otimes h g$ extends linearly to $V \otimes H$ , since multiplication by $g$ is linear in $h$ ; it is bilinear in $(v \otimes h, g)$ . Associativity of $H$ gives $((v \otimes h) g) t = v \otimes (h g) t = v \otimes h (g t) = (v \otimes h) (g t)$ , and its unit gives $(v \otimes h) 1_{H} = v \otimes h$ . Thus it is a right module action.

1.2givenF1F3

The formula $ρ = {id}_{V} \otimes Δ$ is linear. Coassociativity of $Δ$ gives $(ρ \otimes id) ρ (v \otimes h) = \sum (v \otimes h_{1}) \otimes h_{2} \otimes h_{3} = (id \otimes Δ) ρ (v \otimes h)$ , and the counit equation gives $({id}_{V \otimes H} \otimes ε) ρ (v \otimes h) = \sum v \otimes h_{1} ε (h_{2}) = v \otimes h$ under the tensor-unit identification. Hence $ρ$ is a right coaction.

2.1givenF2F4step 1.1step 1.2algebra

For $v \otimes h$ and $g \in H$ , multiplicativity of $Δ$ gives $ρ ((v \otimes h) g) = \sum (v \otimes h_{1} g_{1}) \otimes h_{2} g_{2}$ . On the other side, $\sum (v \otimes h)_{0} g_{1} \otimes (v \otimes h)_{1} g_{2} = \sum ((v \otimes h_{1}) g_{1}) \otimes h_{2} g_{2}$ , which is the same tensor by the action definition. Thus the compatibility in [F4] holds on elementary tensors.

3.1step 2.1F3algebra∎

Both compatibility sides are linear in the $V \otimes H$ input and in $g$ , and elementary tensors span the tensor product by [F3]. Therefore the equality of step 2.1 holds for every element, proving the Hopf-module compatibility.

Depends on

Used by

Right-right Hopf modules are equivalent to vector spaces Corollary
The free Hopf module over a group algebra Example
The free Hopf module over the polynomial Hopf algebra Example
Coinvariants of a free right-right Hopf module Lemma
The fundamental theorem of right-right Hopf modules Theorem

Dependency tree · two levels

17 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

Hans-Juergen Schneider, Lectures on Hopf Algebras, notes by Sonia Natale, Trabajos de Matematica 31/95 (standard reference, not scraped)
D. S. Drogalski, Chapter 3: Hopf Algebras, UC San Diego 207A lecture notes (standard reference, not scraped)