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 coinvariant projection of a right-right Hopf module

Statement

Let $M$ be a right-right Hopf module over a Hopf algebra $H$ over a field $k$ . Define

P : M \to M, P (m) : = \sum m_{0} S (m_{1}) .

Then $P$ is a linear map with image in $M^{co H}$ , it fixes every coinvariant, and hence $P^{2} = P$ . No bijectivity of $S$ is assumed.

Facts & Assumptions

Given: A field $k$ , a Hopf algebra $H$ over $k$ , and a right-right Hopf module $M$ .

[F1]

The coaction is $ρ (m) = \sum m_{0} \otimes m_{1}$ and compatibility is $ρ (m h) = \sum m_{0} h_{1} \otimes m_{1} h_{2}$ (Right-right Hopf modules and coinvariants).

[F2]

The antipode is anti-comultiplicative, $Δ (S (h)) = \sum S (h_{2}) \otimes S (h_{1})$ (Uniqueness and anti-multiplicativity and anti-comultiplicativity of the antipode).

[F3]

The antipode equations are $\sum S (h_{1}) h_{2} = ε (h) 1_{H} = \sum h_{1} S (h_{2})$ and they imply $S (1_{H}) = 1_{H}$ (Hopf algebras and antipodes).

[F4]

Coinvariants are those $n$ with $ρ (n) = n \otimes 1_{H}$ , and they form a $k$ -subspace (Right-right Hopf modules and coinvariants, The coinvariants of a right-right Hopf module form a subspace).

Proof

1.1givenF1F2construct

The map $P$ is the composite of the linear map $ρ$ , the linear map ${id}_{M} \otimes S$ , and the linear action map $M \otimes H \to M$ ; hence it is linear. By [F1] and anti-comultiplicativity in [F2], coassociativity of $ρ$ gives $ρ (P (m)) = \sum m_{0} S (m_{3}) \otimes m_{1} S (m_{2})$ ; the reversed order in the two $S$ factors is exactly $Δ S = (S \otimes S) τ Δ$ .

2.1F2F3step 1.1algebra

For every $h \in H$ , the antipode equation in [F3] and coassociativity give $\sum h_{1} S (h_{2}) \otimes h_{3} = 1_{H} \otimes h$ . Flipping the factors and applying $S$ to the first factor yields $\sum S (h_{3}) \otimes h_{1} S (h_{2}) = S (h) \otimes 1_{H}$ . Applying the linear action of the first coaction component to this tensor identity reduces the expression in step 1.1 to $ρ (P (m)) = \sum m_{0} S (m_{1}) \otimes 1_{H} = P (m) \otimes 1_{H}$ .

3.1F3F4step 2.1algebra∎

Thus $P (m) \in M^{co H}$ for every $m$ , by [F4]. If $n \in M^{co H}$ , then $P (n) = n S (1_{H}) = n$ : the first equality uses $ρ (n) = n \otimes 1_{H}$ , and $S (1_{H}) = 1_{H}$ is in [F3]. Therefore $P$ fixes its image, so $P^{2} = P$ .

Depends on

Used by

The free Hopf module over a group algebra Example
The free Hopf module over the polynomial Hopf algebra Example
The regular Hopf module and its projection Example
The fundamental theorem of right-right Hopf modules Theorem

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.

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)