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.

Coinvariants of a free right-right Hopf module

Statement

Let $V$ be any $k$ -vector space and $H$ a Hopf algebra over $k$ . For the free Hopf module $V \otimes H$ with coaction on the $H$ factor,

(V \otimes H)^{co H} = {v \otimes 1_{H} : v \in V} .

The map $i : V \to (V \otimes H)^{co H}$ , $i (v) = v \otimes 1_{H}$ , is an isomorphism with inverse the restriction of $q : = {id}_{V} \otimes ε$ .

Facts & Assumptions

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

[F1]

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

[F2]

Coinvariants are exactly $x$ satisfying $ρ (x) = x \otimes 1_{H}$ (Right-right Hopf modules and coinvariants).

[F3]

The counit identities are $λ_{H} (ε \otimes {id}_{H}) Δ = {id}_{H} = ρ_{H} ({id}_{H} \otimes ε) Δ$ (Coalgebra and coalgebra map over a field).

[F4]

The coproduct is a unital algebra map, so $Δ (1_{H}) = 1_{H} \otimes 1_{H}$ , and the counit is unital, so $ε (1_{H}) = 1$ (Bialgebras and bialgebra maps).

Proof

1.1givenF1F4

The map $i (v) = v \otimes 1_{H}$ has image in the coinvariants: by [F1], $ρ (i (v)) = \sum (v \otimes 1_{H}) \otimes 1_{H} = i (v) \otimes 1_{H}$ , since $Δ (1_{H}) = 1_{H} \otimes 1_{H}$ by [F4]. The counit map $q = {id}_{V} \otimes ε$ satisfies $q (i (v)) = v ε (1_{H}) = v$ by [F4].

2.1F1F2F3construct∎

If $x \in (V \otimes H)^{co H}$ , then [F1]-[F2] say $({id}_{V} \otimes Δ) (x) = x \otimes 1_{H}$ . Apply ${id}_{V} \otimes ε \otimes {id}_{H}$ to both sides. The counit identity in [F3] gives $x = q (x) \otimes 1_{H} = i (q (x))$ . Thus every coinvariant lies in the image of $i$ , and $q$ is its inverse there. No basis or choice principle is used.

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

Dependency tree · two levels

12 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)