ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generated

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.

Group-graded vector spaces as comodules over the group-like coalgebra

Example

Let $G$ be a group and let $C = k G$ denote the vector space with basis symbols $e_{g}$ for $g \in G$ , with the group-coalgebra structure $Δ (e_{g}) = e_{g} \otimes e_{g}$ and $ε (e_{g}) = 1$ . The group multiplication is not used by this coalgebra structure. A $G$ -grading on $V$ means a family of subspaces $V_{g} \subseteq V$ with $V = ⨁_{g \in G} V_{g}$ , so each vector has a unique finite decomposition. Right $C$ -comodules are exactly these $G$ -graded vector spaces.

Facts & Assumptions

Given: A field $k$ , a group $G$ , its basis-indexed vector space $C = k G$ , and either a $G$ -graded vector space $V = ⨁_{g \in G} V_{g}$ or a right $C$ -comodule $(M, ρ)$ .

[F1]

A right comodule is a vector space with $ρ : M \to M \otimes C$ satisfying coassociativity and counitality. (Right comodules, comodule maps, and subcomodules)

[F2]

A coalgebra is a vector space with coassociative $Δ : C \to C \otimes C$ and a two-sided counit $ε : C \to k$ ; a coalgebra map preserves both. (Coalgebra and coalgebra map over a field)

[F3]

Every tensor is a finite sum of elementary tensors, and the coordinate functional $δ_{g}$ on $k G$ is defined by $δ_{g} (e_{h}) = δ_{g, h}$ and linear extension. (Scalars, tensor powers, the empty tensor, opposite algebras and finite sums, Linear map between vector spaces over the same field)

Verification

Given: The structures in the Example.

1.1givenF2constructalgebra

Define $Δ (e_{g}) = e_{g} \otimes e_{g}$ and $ε (e_{g}) = 1$ on the basis and extend linearly. For every $g$ , $(Δ \otimes id) Δ (e_{g}) = e_{g} \otimes e_{g} \otimes e_{g} = (id \otimes Δ) Δ (e_{g})$ and $(ε \otimes id) Δ (e_{g}) = e_{g} = (id \otimes ε) Δ (e_{g})$ . Both sides are linear, so $C$ is a coalgebra.

1.2givenF3construct

A grading $V = ⨁_{g} V_{g}$ means every $v \in V$ has a unique finite decomposition $v = \sum_{g} v_{g}$ with $v_{g} \in V_{g}$ . Define $ρ (v) = \sum_{g} v_{g} \otimes e_{g}$ . Uniqueness of the finite decomposition makes $ρ$ well-defined, and adding or scaling decompositions shows it is linear.

1.3givenF1F3construct

Conversely, define $M_{g} : = {m \in M : ρ (m) = m \otimes e_{g}}$ for each $g \in G$ . Each $M_{g}$ is a subspace: it contains $0$ , and if $m, n \in M_{g}$ and $a, b \in k$ , linearity of $ρ$ gives $ρ (a m + b n) = a m \otimes e_{g} + b n \otimes e_{g} = (a m + b n) \otimes e_{g}$ . Fix $m \in M$ and collect equal basis terms in its finite tensor expansion as $ρ (m) = \sum_{i = 1}^{r} m_{i} \otimes e_{g_{i}}$ with distinct $g_{i}$ . Coassociativity gives $\sum_{i} ρ (m_{i}) \otimes e_{g_{i}} = \sum_{i} m_{i} \otimes e_{g_{i}} \otimes e_{g_{i}}$ . Apply ${id}_{M} \otimes {id}_{C} \otimes δ_{g_{j}}$ for a fixed $j$ . Distinctness of the $g_{i}$ makes the left side $ρ (m_{j})$ and the right side $m_{j} \otimes e_{g_{j}}$ , so $m_{j} \in M_{g_{j}}$ .

2.1F1step 1.1step 1.2algebra

For homogeneous $v_{g} \in V_{g}$ , $(ρ \otimes id) ρ (v_{g}) = v_{g} \otimes e_{g} \otimes e_{g} = (id \otimes Δ) ρ (v_{g})$ and $(id \otimes ε) ρ (v_{g}) = v_{g}$ . Homogeneous vectors span the direct sum, so linearity extends both identities to every $v$ ; hence $V$ is a right $C$ -comodule.

2.2F1F3step 1.3

The counit identity gives $m = \sum_{i} m_{i}$ with each $m_{i} \in M_{g_{i}}$ by step 1.3, so the subspaces $M_{g}$ span $M$ and every vector has finite support. If a finite sum $\sum_{g \in F} u_{g} = 0$ has $u_{g} \in M_{g}$ , applying $ρ$ gives $\sum_{g \in F} u_{g} \otimes e_{g} = 0$ ; then ${id}_{M} \otimes δ_{h}$ gives $u_{h} = 0$ for each $h \in F$ . Thus the sum is direct and the recovered grading is unique.

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

Steps 1.2 and 2.1 construct a comodule from every $G$ -grading, and steps 1.3 and 2.2 recover a unique such grading from every right $k G$ -comodule. The coalgebra axioms for this $k G$ structure were checked in step 1.1.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

15 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

Daniel Kongsgaard and UCSD Math 207A, Hopf Algebras Lecture Notes, Spring 2020 (standard reference, not scraped)
William Chin, A Brief Introduction to Coalgebra Representation Theory (standard reference, not scraped)