TheoremStatement: 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.

Coideal quotients, coalgebra-map kernels, and sums of subcoalgebras

Statement

Let $C$ be a coalgebra over a field $k$ , and assume the Axiom of Choice. For every coideal $I \subseteq C$ , the quotient vector space $C / I$ has a unique coalgebra structure making $q : C \to C / I$ a coalgebra map, given by

\overline{Δ} (c + I) = (q \otimes q) Δ (c), \overline{ε} (c + I) = ε_{C} (c) .

This quotient has the universal property that every coalgebra map $f : C \to D$ with $I \subseteq \ker f$ factors uniquely through $q$ by a coalgebra map. Also, the kernel of every coalgebra map is a coideal, and the sum of any family of subcoalgebras of $C$ is a subcoalgebra.

Facts & Assumptions

Given: A field $k$ , a coalgebra $C$ , and the Axiom of Choice.

[A1]

The Axiom of Choice says every family of nonempty sets has a choice function (The Axiom of Choice).

[F1]

A coideal $I$ satisfies $ε_{C} (I) = 0$ and $Δ_{C} (I) \subseteq I \otimes C + C \otimes I$ ; a subcoalgebra is a subspace with its inclusion a coalgebra map (Subcoalgebras, coideals, and quotient coalgebras).

[F2]

For subspaces $U \subseteq V$ and $Z \subseteq W$ , with quotient maps $p : V \to V / U$ and $r : W \to W / Z$ , $\ker (p \otimes r) = U \otimes W + V \otimes Z$ . Tensoring an injective linear map with an identity map is injective (Tensoring injections and the kernel of a tensor product of quotient maps over a field).

[F3]

The quotient $C / I$ consists of additive cosets, with the quotient map linear and surjective; for a vector space the scalar action on cosets is well-defined (Quotient module $M / N$ with scalar multiplication on additive cosets, The quotient action is well defined and makes $M / N$ a module).

[F4]

Linear maps induce tensor maps, preserve composition, and are determined by their values on elementary tensors (Module homomorphisms induce tensor-product homomorphisms functorially).

[F5]

The associator and symmetry are natural, and the unit isomorphisms are natural as well (Associator naturality, pentagon, unit triangle and symmetry hexagons on elementary tensors).

[F6]

Coalgebra maps preserve comultiplication and counit, and the coalgebra identities use the associator and unit isomorphisms of [F5] (Coalgebra and coalgebra map over a field).

Proof

1.1givenA1F1F2F3F4construct

Let $q : C \to C / I$ be the quotient map. By [F2], $\ker (q \otimes q) = I \otimes C + C \otimes I$ , so $(q \otimes q) Δ (x) = 0$ for every $x \in I$ by [F1]; also $ε_{C} (x) = 0$ for $x \in I$ . If $c + I = c^{'} + I$ , then $c - c^{'} \in I$ by the coset description [F3], and these two vanishing facts give $(q \otimes q) Δ (c) = (q \otimes q) Δ (c^{'})$ and $ε_{C} (c) = ε_{C} (c^{'})$ . Hence the displayed formulas are well-defined on cosets; their linearity follows from linearity of $Δ$ , $ε_{C}$ , and $q \otimes q$ together with the quotient operations of [F3]. They define maps $\overline{Δ}$ and $\overline{ε}$ with $\overline{Δ} q = (q \otimes q) Δ$ and $\overline{ε} q = ε_{C}$ . The map $q \otimes q$ is surjective: each element of $(C / I) \otimes (C / I)$ is a finite sum of elementary tensors, and each factor of each elementary tensor has a preimage under $q$ .

1.2givenA1F1F2F3F5F6algebra

Let $f : C \to D$ be a coalgebra map and $K = \ker f$ . Then $ε_{C} (K) = 0$ by [F6]. Let $q_{K} : C \to C / K$ be the quotient map and define $\tilde{f} : C / K \to D$ by $\tilde{f} (c + K) = f (c)$ . This is well-defined and linear by the coset description [F3], and it is injective because $\tilde{f} (c + K) = 0$ implies $c \in K$ . For $x \in K$ , $(\tilde{f} \otimes \tilde{f}) (q_{K} \otimes q_{K}) Δ (x) = (f \otimes f) Δ (x) = Δ_{D} (f (x)) = 0$ . The tensor map $\tilde{f} \otimes \tilde{f}$ is injective by [A1] and [F2], applying the injection assertion twice and using the symmetry in [F5]; hence $(q_{K} \otimes q_{K}) Δ (x) = 0$ . The quotient-kernel formula [F2] now gives $Δ (x) \in K \otimes C + C \otimes K$ , so $K$ is a coideal by [F1].

1.3givenA1F1F2F4construct

Let $(D_{α})_{α \in Λ}$ be any family of subcoalgebras and set $S = \sum_{α \in Λ} D_{α}$ , where the sum consists of finite sums of elements of the $D_{α}$ . For $s \in S$ , write $s = \sum_{j = 1}^{r} d_{j}$ with each $d_{j}$ in some $D_{α_{j}}$ . Since each inclusion $D_{α_{j}} \to C$ is a coalgebra map, $Δ_{C} (d_{j})$ lies in the image of $D_{α_{j}} \otimes D_{α_{j}}$ , which factors through $S \otimes S$ . Thus $Δ_{C} (S)$ lies in the image of $S \otimes S \to C \otimes C$ . This last map is injective by [A1] and [F2], so it gives a unique linear $Δ_{S} : S \to S \otimes S$ with $(j_{S} \otimes j_{S}) Δ_{S} = Δ_{C} j_{S}$ ; put $ε_{S} = ε_{C} ∣_{S}$ .

2.1step 1.1F4F5F6algebra

The coassociativity composites, after precomposition with $q$ , satisfy $α_{C / I, C / I, C / I} (\overline{Δ} \otimes i d) \overline{Δ} q = (q \otimes (q \otimes q)) α_{C, C, C} (Δ \otimes i d) Δ = (q \otimes (q \otimes q)) (i d \otimes Δ) Δ = (i d \otimes \overline{Δ}) \overline{Δ} q$ , where the middle equality is coassociativity in $C$ and the outer equalities use functoriality and associator naturality [F4, F5, F6]. Since $q$ is surjective, the composites on $C / I$ are equal. Likewise $λ_{C / I} (\overline{ε} \otimes i d) \overline{Δ} q = λ_{C / I} (ε_{C} \otimes q) Δ = q λ_{C} (ε_{C} \otimes i d) Δ = q$ and $ρ_{C / I} (i d \otimes \overline{ε}) \overline{Δ} q = ρ_{C / I} (q \otimes ε_{C}) Δ = q ρ_{C} (i d \otimes ε_{C}) Δ = q$ ; unit naturality and the counit equations give the last equalities, and surjectivity of $q$ proves both counit identities on $C / I$ .

2.2step 1.3A1F2F5F6algebra

The map $j_{S} \otimes j_{S} \otimes j_{S}$ is injective by applying [F2] repeatedly, with associators from [F5]. Composing the two coassociativity composites for $Δ_{S}$ with this injection gives the corresponding composites for $Δ_{C} j_{S}$ , which agree by [F6]; therefore the composites for $Δ_{S}$ agree. Composing either counit composite with $j_{S}$ gives the corresponding counit composite in $C$ followed by $j_{S}$ , hence $j_{S}$ by [F6]; since $j_{S}$ is injective, each counit composite on $S$ is ${i d}_{S}$ . Thus $S$ is a subcoalgebra. If $Λ$ is empty, $S = 0$ and the unique zero structure maps satisfy the coalgebra identities on the zero space.

3.1step 1.1step 2.1F3F4F6

Any coalgebra structure on $C / I$ making $q$ a coalgebra map must satisfy $\overline{Δ} q = (q \otimes q) Δ$ and $\overline{ε} q = ε_{C}$ . Surjectivity of $q$ uniquely determines each map, so the displayed quotient structure is unique. If a coalgebra map $f : C \to D$ kills $I$ , define $\overline{f} (c + I) = f (c)$ . This is well-defined and linear by [F3]. The equations $ε_{D} \overline{f} q = ε_{C} = \overline{ε} q$ and $Δ_{D} \overline{f} q = (f \otimes f) Δ = (\overline{f} \otimes \overline{f}) (q \otimes q) Δ = (\overline{f} \otimes \overline{f}) \overline{Δ} q$ show, by surjectivity of $q$ , that $\overline{f}$ is a coalgebra map; any factorization is this map on cosets, so it is unique.

4.1step 1.1step 2.1step 3.1step 1.2step 1.3step 2.2∎

Steps 1.1 and 2.1 establish the quotient coalgebra, and step 3.1 proves its uniqueness and universal property. Step 1.2 establishes the kernel coideal claim; steps 1.3 and 2.2 establish closure under arbitrary sums of subcoalgebras.

Depends on

Used by

The fundamental theorem of coalgebras Theorem

Dependency tree · two levels

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