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 tensor product of two coalgebras is a coalgebra

Statement

Let $k$ be a field and let $(C, Δ_{C}, ε_{C})$ and $(D, Δ_{D}, ε_{D})$ be $k$ -coalgebras in the sense of Coalgebra and coalgebra map over a field. Thus $Δ_{C} : C \to C \otimes C$ and $ε_{C} : C \to k$ are linear and satisfy coassociativity and both counit equations from that definition, with the corresponding equations for $D$ . Equip $C \otimes D$ with

$Δ_{C \otimes D} (c \otimes d) = \sum (c_{(1)} \otimes d_{(1)}) \otimes (c_{(2)} \otimes d_{(2)}), ε_{C \otimes D} (c \otimes d) = ε_{C} (c) ε_{D} (d) .$

Here the sums are the finite tensor expressions for $Δ_{C} (c)$ and $Δ_{D} (d)$ , and the formula for $Δ_{C \otimes D}$ is obtained by applying $Δ_{C} \otimes Δ_{D}$ and then flipping the two middle factors. These formulas define linear maps and make $C \otimes D$ a coalgebra. No finite-dimensionality assumption is used.

Facts & Assumptions

Given: $k$ is a field, and the linear maps for $C$ and $D$ satisfy the coassociativity and counit equations stated in the Statement.

[F1]

Every element of $V \otimes W$ is a finite sum of elementary tensors, and tensor powers are associated using the displayed canonical associators (Scalars, tensor powers, the empty tensor, opposite algebras and finite sums).

[F2]

Linear maps induce tensor-product linear maps by $(f \otimes g) (v \otimes w) = f (v) \otimes g (w)$ , uniquely and functorially (Module homomorphisms induce tensor-product homomorphisms functorially).

[F3]

The canonical associators and flips are coherent linear isomorphisms on iterated tensor products (Associator naturality, pentagon, unit triangle and symmetry hexagons on elementary tensors).

[F4]

The canonical unit isomorphism $k \otimes k ≅ k$ sends $r \otimes s$ to $r s$ (The regular module is a tensor unit: $R \otimes_{R} N ≅ N$ and $M \otimes_{R} R ≅ M$ ).

[F5]

A coalgebra's coassociativity and counit identities use the canonical associator and tensor-unit maps (Coalgebra and coalgebra map over a field).

Proof

technique · direct

1.1givenF1F2F3F4construct

The map $C \otimes D \to (C \otimes D) \otimes (C \otimes D)$ is the composite of the tensor maps induced by $Δ_{C}, Δ_{D}$ and the middle-factor flip from [F2]–[F3]; the counit map is $ε_{C} \otimes ε_{D}$ followed by the unit isomorphism [F4]. Thus both formulas are well-defined linear maps, and on any elementary tensor they have the stated values.

1.2givenF3F5algebra

On $c \otimes d$ , either iterated coproduct first applies the corresponding threefold coproducts to $c$ and $d$ and then interleaves their factors in the order $C, D, C, D, C, D$ . Coassociativity of $Δ_{C}$ and $Δ_{D}$ from [F5] makes these threefold coproducts equal for the two parenthesizations, and the coherent associators and flips in [F3] give the same interleaving; therefore $(Δ_{C \otimes D} \otimes i d) Δ_{C \otimes D} = (i d \otimes Δ_{C \otimes D}) Δ_{C \otimes D}$ on elementary tensors.

1.3givenF5algebra

Applying the left counit to the displayed coproduct gives $\sum ε_{C} (c_{(1)}) ε_{D} (d_{(1)}) (c_{(2)} \otimes d_{(2)}) = c \otimes d$ by the two left counit equations in [F5]; applying the right counit gives $\sum ε_{C} (c_{(2)}) ε_{D} (d_{(2)}) (c_{(1)} \otimes d_{(1)}) = c \otimes d$ by the two right counit equations.

2.1step 1.2step 1.3F1∎

Both sides of every identity in steps 1.2–1.3 are linear maps, and elementary tensors span each tensor product by [F1]. The identities therefore hold on all of their domains, proving that the stated maps make $C \otimes D$ a coalgebra.

Depends on

Used by

Dependency tree · two levels

16 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-Jürgen Schneider, Lectures on Hopf algebras, notes by Sonia Natale (standard reference, not scraped)
Pavel Etingof and Mykola Semenyakin, A brief introduction to quantum groups (standard reference, not scraped)