LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

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.

Finite comatrix coalgebras exist

Statement

For a field $k$ and an integer $n \geq 1$ , let $E_{n}$ be the vector space with basis $c_{i j}$ for $1 \leq i, j \leq n$ . The linear maps defined on this basis by $Δ (c_{i j}) = \sum_{ℓ = 1}^{n} c_{i ℓ} \otimes c_{ℓ j}, ε (c_{i j}) = δ_{i j}$ make $E_{n}$ a coalgebra. In particular, the one-dimensional space with basis $c$ and maps $Δ (c) = c \otimes c$ , $ε (c) = 1$ is a nonzero coalgebra.

Facts & Assumptions

Given: A field $k$ , an integer $n \geq 1$ , and the vector space $E_{n}$ with the stated basis.

[F1]

The coalgebra axioms are coassociativity and the two counit identities, with the associator and unit maps specified in the definition (Coalgebra and coalgebra map over a field).

[F2]

Tensors are algebraic finite sums over $k$ (Scalars, tensor powers, the empty tensor, opposite algebras and finite sums).

[F3]

The tensor associator identifies $(E_{n} \otimes E_{n}) \otimes E_{n}$ with $E_{n} \otimes (E_{n} \otimes E_{n})$ (Associator naturality, pentagon, unit triangle and symmetry hexagons on elementary tensors).

[F4]

A set map from a free basis extends uniquely to a linear map (Universal property of the free module on a set).

[F5]

Tensoring linear maps gives well-defined linear maps, with $(f \otimes g) (x \otimes y) = f (x) \otimes g (y)$ (Module homomorphisms induce tensor-product homomorphisms functorially).

Proof

1.1givenF4construct

The displayed assignments on the basis extend uniquely to linear maps $Δ : E_{n} \to E_{n} \otimes E_{n}$ and $ε : E_{n} \to k$ by [F4].

2.1givenstep 1.1F1F2F3F5algebra

On a basis vector, the left side of coassociativity in $E_{n} \otimes (E_{n} \otimes E_{n})$ is $α ((Δ \otimes i d) Δ (c_{i j})) = \sum_{m, ℓ} c_{i m} \otimes (c_{m ℓ} \otimes c_{ℓ j})$ , while the right side is $(i d \otimes Δ) Δ (c_{i j}) = \sum_{ℓ, m} c_{i ℓ} \otimes (c_{ℓ m} \otimes c_{m j})$ . Interchanging the dummy indices $m$ and $ℓ$ in the finite right-hand sum makes the sums identical. Since both sides are linear and the $c_{i j}$ form a basis, coassociativity holds on $E_{n}$ .

2.2givenstep 1.1F1F5algebra

For every $i, j$ , $λ (ε \otimes i d) Δ (c_{i j}) = \sum_{ℓ} δ_{i ℓ} c_{ℓ j} = c_{i j}$ and $ρ (i d \otimes ε) Δ (c_{i j}) = \sum_{ℓ} c_{i ℓ} δ_{ℓ j} = c_{i j}$ . Linearity extends both identities from the basis to $E_{n}$ .

3.1step 2.1step 2.2F1given∎

Steps 2.1 and 2.2 verify the coalgebra axioms of [F1]. At $n = 1$ the displayed formulas give $Δ (c) = c \otimes c$ and $ε (c) = 1$ ; because $c$ is a basis vector it is nonzero.

Depends on

Used by

Dependency tree · two levels

18 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

UCSD Math 207A, Hopf Algebras lecture notes, Spring 2020 (standard reference, not scraped)
Benedikt Stufler, Hopf Algebras lecture notes, University of Zurich course, 2018 (standard reference, not scraped)