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 two standard bialgebra compatibility formulations are equivalent

Statement

Let $H$ be a $k$ -vector space with a unital associative algebra structure $(m, u)$ and a counital coassociative coalgebra structure $(Δ, ε)$ . Give $H \otimes H$ the tensor-product coalgebra structure of The tensor product of two coalgebras is a coalgebra, and give $k$ its coalgebra structure $Δ_{k} (λ) = λ (1 \otimes 1)$ , $ε_{k} (λ) = λ$ . Then the following are equivalent:

$Δ : H \to H \otimes H$ and $ε : H \to k$ are unital algebra homomorphisms, where $H \otimes H$ has multiplication $(a \otimes b) (c \otimes d) = a c \otimes b d$ .
$m : H \otimes H \to H$ and $u : k \to H$ are coalgebra maps.

This equivalence is valid over every field and uses no dimension assumption.

Facts & Assumptions

Given: The algebra and coalgebra structure maps above, the tensor-product coalgebra formula, and the tensor-product algebra formula.

[F1]

A coalgebra map $f : C \to D$ is linear and satisfies $Δ_{D} f = (f \otimes f) Δ_{C}$ and $ε_{D} f = ε_{C}$ (Coalgebra and coalgebra map over a field).

[F2]

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

[F3]

A bialgebra over $k$ requires $Δ$ and $ε$ to be unital algebra homomorphisms, using the tensor-product algebra multiplication (Bialgebras and bialgebra maps).

[F4]

The tensor-product coalgebra has $Δ_{H \otimes H} (a \otimes b) = \sum (a_{(1)} \otimes b_{(1)}) \otimes (a_{(2)} \otimes b_{(2)})$ and $ε_{H \otimes H} (a \otimes b) = ε (a) ε (b)$ (The tensor product of two coalgebras is a coalgebra).

[F5]

The tensor-product algebra multiplication satisfies $(a \otimes b) (c \otimes d) = a c \otimes b d$ with unit $1 \otimes 1$ (The tensor product of $R$ -algebras has multiplication $(a \otimes b) (a^{'} \otimes b^{'}) = a a^{'} \otimes b b^{'}$ ).

[F6]

The unit isomorphism $k \otimes k \to 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$ ).

[F7]

The associator on iterated tensor products is coherent (Associator naturality, pentagon, unit triangle and symmetry hexagons on elementary tensors).

[F8]

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

Proof

technique · direct

1.1givenF6F7F8algebra

The stated maps make $k$ a coalgebra: for $r \in k$ , both iterated coproducts of $Δ_{k} (r) = r (1 \otimes 1)$ equal $r (1 \otimes 1 \otimes 1)$ under the coherent associator [F7], and either counit contraction equals $r$ under the unit isomorphism [F6]. The induced tensor maps are well-defined by [F8].

1.2givenF3F5algebra

The maps in condition 1 are unital algebra homomorphisms exactly when they preserve products and units, as required in the bialgebra definition [F3]. With the tensor-product algebra [F5], these requirements are precisely $Δ (a b) = Δ (a) Δ (b)$ , $Δ (1) = 1 \otimes 1$ , $ε (a b) = ε (a) ε (b)$ , and $ε (1) = 1$ .

1.3givenF1F2F4F5F8algebra

The comultiplication equation for $m$ to be a coalgebra map [F1], evaluated on $a \otimes b$ , is $Δ (m (a \otimes b)) = (m \otimes m) Δ_{H \otimes H} (a \otimes b) = \sum a_{(1)} b_{(1)} \otimes a_{(2)} b_{(2)}$ . By [F4]–[F5], this is exactly $Δ (a b) = Δ (a) Δ (b)$ . Both sides are linear in $a \otimes b$ and elementary tensors span $H \otimes H$ by [F2], while $m \otimes m$ is well-defined by [F8]. Thus the map equation holds exactly when that multiplicativity equation holds for all $a, b$ .

1.4givenF1F2F4

The counit equation for $m$ to be a coalgebra map [F1] is $ε (m (a \otimes b)) = ε_{H \otimes H} (a \otimes b)$ , which by [F4] is $ε (a b) = ε (a) ε (b)$ . Since elementary tensors span [F2], equality on all of them is equivalent to equality of the linear maps.

2.1givenF1F8step 1.1step 1.2step 1.3step 1.4∎

For $u : k \to H$ , the coalgebra-map equations [F1] at $λ \in k$ are $Δ (u (λ)) = (u \otimes u) Δ_{k} (λ)$ and $ε (u (λ)) = ε_{k} (λ)$ . By linearity and the formulas in the Statement, these become $λ Δ (1) = λ (1 \otimes 1)$ and $λ ε (1) = λ$ , using the source coalgebra established in step 1.1. They hold for every $λ$ exactly when $Δ (1) = 1 \otimes 1$ and $ε (1) = 1$ . Steps 1.3–1.4 show that $m$ is a coalgebra map exactly when the two product equations hold; the two unit equations supply the remaining equations in step 1.2. Therefore condition 2 holds exactly when condition 1 holds.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

20 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)
Thomas Rüd, Hopf Algebras and rooted trees, Practical work in mathematics (standard reference, not scraped)