TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

Intrinsic finite category hypotheses give a finite projective generator

Statement

Let $C$ be a finite $k$ -linear abelian category, with simple representatives $S_{1}, \dots, S_{n}$ and chosen projective covers $Q_{i} ↠ S_{i}$ , and put $P = ⨁_{i = 1}^{n} Q_{i}$ and $A = {End}_{C} (P)^{o p}$ . Then: (i) $P$ is projective; (ii) $P$ is a generator of $C$ , that is, ${P}$ is separating; (iii) $A$ is a finite-dimensional unital $k$ -algebra; (iv) $C (P, -)$ is exact and faithful; and (v) every object of $C$ is a quotient of a finite direct sum of copies of $P$ . The proof uses only that each $Q_{i} ↠ S_{i}$ is a projective epimorphism, never the superfluity of its kernel, so the same conclusions hold if "enough projectives" is read as "every simple object admits a projective epimorphism onto it"; for the finite module categories of Finite-dimensional module categories satisfy the intrinsic finiteness conditions the two readings coincide. Only the finitely many covers $Q_{i}$ are selected; no further choice is used.

Facts & Assumptions

Given: A field $k$ , a finite $k$ -linear abelian category $C$ in the sense of Finite k-linear abelian categories, simple representatives $S_{1}, \dots, S_{n}$ for all isomorphism classes of simple objects, and chosen projective epimorphisms $Q_{i} ↠ S_{i}$ , $i = 1, \dots, n$ . Put $P = ⨁_{i = 1}^{n} Q_{i}$ and $A = {End}_{C} (P)^{o p}$ .

[F1]

For an object $P$ of an abelian category the following are equivalent: $P$ is projective; the functor $C (P, -)$ carries every short exact sequence to a short exact sequence; and every epimorphism onto $P$ splits (Projective object characterisations, Projective object).

[F2]

A biproduct $⨁_{i} Q_{i}$ is a coproduct with injections ${i n j}_{i}$ and a product with projections ${p r}_{i}$ satisfying ${p r}_{i} {i n j}_{i} = 1_{Q_{i}}$ ; the projections are split epimorphisms, hence epimorphisms, and morphisms out of a coproduct are determined by their composites with the injections (Biproduct, Identities and composites of monomorphisms or epimorphisms retain cancellation; split monomorphisms are monic and split epimorphisms are epic).

[F3]

Composites of epimorphisms are epimorphisms; if $π h \neq 0$ then $h \neq 0$ ; a monomorphism composed with a nonzero morphism is nonzero; and if $e$ is epic and $f e = 0$ then $f = 0$ (Identities and composites of monomorphisms or epimorphisms retain cancellation; split monomorphisms are monic and split epimorphisms are epic, Monomorphism and epimorphism by left and right cancellation).

[F4]

Every morphism $f : X \to Y$ of an abelian category factors as $f = m \circ e$ with $e$ an epimorphism and $m$ a monomorphism, with $m$ representing $im f$ ; in particular $f \neq 0$ exactly when $im f \neq 0$ (Every morphism factors as an epimorphism followed by a monomorphism, uniquely up to unique isomorphism, Image and coimage in a category with kernels and cokernels).

[F5]

Every nonzero object of finite length has a composition series whose last factor $Z ↠ S$ is a simple quotient, and every simple object of $C$ is isomorphic to one of $S_{1}, \dots, S_{n}$ (Composition series and composition factors of an object, Simple object, given).

[F6]

An object $G$ is a generator when the singleton ${G}$ is separating, that is, when for every pair of distinct parallel morphisms $u \neq v : X \to Y$ there is $g : G \to X$ with $u g \neq v g$ (Separating and coseparating sets of objects, Generator and cogenerator of a category).

[F7]

A functor is faithful when it is injective on every hom-set; for $C (P, -)$ this means that $u \neq v : X \to Y$ yields $u \circ - \neq v \circ -$ , that is, some $g : P \to X$ has $u g \neq v g$ (Faithful, full, fully faithful, essentially surjective, and split essentially surjective functors).

[F8]

Under the hypotheses of the statement, every object of finite length, in particular every object of $C$ , admits an epimorphism $P^{m} ↠ X$ for some $m \geq 0$ , using only that the $Q_{i} ↠ S_{i}$ are projective epimorphisms (Projective epimorphisms onto the simples generate every finite-length object, Locally finite k-linear abelian categories).

[F9]

For an object $P$ of a preadditive category, ${End}_{C} (P) = C (P, P)$ with addition from the hom-group and multiplication given by composition is a unital ring with identity $1_{P}$ , composition is bilinear in both variables, and reversing the multiplication gives the opposite ring (Endomorphisms of an object of a preadditive category form a ring, The opposite ring $R^{o p}$ ).

[F10]

A finite $k$ -linear abelian category is locally finite: every object has finite length and every hom-space is finite-dimensional over $k$ (Finite k-linear abelian categories, Locally finite k-linear abelian categories, Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis). A $k$ -algebra is a unital ring with a central unital structure map $k \to A$ , equivalently a $k$ -vector space with a bilinear unital multiplication (Algebras over a commutative ring, central structure maps, and algebra homomorphisms, k-linear categories and k-linear functors).

[F11]

For the finite module categories of Finite-dimensional module categories satisfy the intrinsic finiteness conditions the stronger reading holds: the published cover theorem gives every simple module a projective cover (Every finite-dimensional module has a projective cover, unique up to isomorphism over the target).

Proof

technique · direct

1.1F1F2givenchooseconstruct

(i) $P$ is projective. Let $q : E ↠ P$ be an epimorphism. Projectivity of each $Q_{i}$ gives a lift $s_{i} : Q_{i} \to E$ of the injection ${i n j}_{i} : Q_{i} \to P$ , so $q s_{i} = {i n j}_{i}$ . The coproduct property [F2] gives $s : P \to E$ with $s {i n j}_{i} = s_{i}$ . Thus $q s {i n j}_{i} = {i n j}_{i}$ for every $i$ , and equality on all injections implies $q s = 1_{P}$ . Hence every epimorphism onto $P$ splits, so $P$ is projective by [F1].

1.2F1F2F3F4F5F6given

(ii) $P$ is separating. Let $u \neq v : X \to Y$ and put $f = u - v \neq 0$ , using that $C$ is additive. By [F4] $f$ factors as $f = m \circ e$ with $e : X ↠ Z$ epic, $m : Z ↣ Y$ monic and $Z = im f \neq 0$ ; by [F5] the nonzero object $Z$ of finite length has a simple quotient $π : Z ↠ S$ , and $S ≅ S_{i}$ for some $i$ by [F5]. Composing the chosen epimorphism $Q_{i} ↠ S_{i}$ with an isomorphism $S_{i} ≅ S$ gives an epimorphism $Q_{i} ↠ S$ , which by projectivity of $Q_{i}$ and [F1] lifts along $π$ to $h : Q_{i} \to Z$ with $π h$ epic; then $h \neq 0$ because $π h$ is an epimorphism onto the nonzero simple $S$ . Since $e$ is epic and $Q_{i}$ projective, $h$ lifts further along $e$ to $\tilde{h} : Q_{i} \to X$ with $e \tilde{h} = h$ . Then $m h = m e \tilde{h} = f \tilde{h}$ , and $m h \neq 0$ by [F3] because $m$ is monic and $h \neq 0$ ; so $f \tilde{h} \neq 0$ , and composing with the split epimorphism ${p r}_{i} : P ↠ Q_{i}$ of [F2] gives $g : = \tilde{h} {p r}_{i} : P \to X$ with $f g \neq 0$ , again by [F3]. Hence $u g \neq v g$ for the distinct morphisms $u, v$ , so ${P}$ is separating and $P$ is a generator by [F6].

1.3F9F10given

(iii) $A$ is a finite-dimensional unital $k$ -algebra. By [F9] the endomorphism set ${End}_{C} (P) = C (P, P)$ is a unital ring under composition with identity $1_{P}$ , and reversing the multiplication gives the opposite ring $A$ ; by [F10] the hom-space is finite-dimensional over $k$ and composition is $k$ -bilinear, so both ${End}_{C} (P)$ and its opposite $A$ are $k$ -vector spaces with bilinear unital multiplication. The structure map $η : k \to A$ , $η (c) = c \cdot 1_{P}$ , is a unital ring homomorphism whose image is central, because multiplication by scalars commutes with composition by $k$ -bilinearity; hence $A$ is a unital $k$ -algebra by [F10], finite-dimensional over $k$ since $C (P, P)$ is.

1.4F8F10

(v) Every object is a quotient of $P^{m}$ for some $m \geq 0$ : by [F10] every object of $C$ has finite length, so [F8] supplies an epimorphism $P^{m} ↠ X$ for some $m$ , whose target $X$ is therefore a quotient of $P^{m}$ .

2.1F1F7step 1.1step 1.2

(iv) $C (P, -)$ is exact and faithful. Exactness is condition 2 of [F1] applied to the projective object $P$ of step 1.1. For faithfulness, let $u \neq v : X \to Y$ ; by step 1.2 there is $g : P \to X$ with $u g \neq v g$ , so the induced maps on hom-sets differ and $C (P, -)$ is injective on this hom-set; since $u, v$ were arbitrary, $C (P, -)$ is faithful in the sense of [F7].

3.1step 1.1step 1.2step 1.3step 2.1step 1.4F8F11given∎

The claims (i), (ii), (iii), (iv) and (v) are steps 1.1, 1.2, 1.3, 2.1 and 1.4. Inspecting these steps and the covering lemma [F8], the only properties of the maps $Q_{i} ↠ S_{i}$ that were used are that they are epimorphisms and that their sources are projective; the superfluity of their kernels was never used, so replacing the covers by arbitrary projective epimorphisms onto the simples does not change the argument, which proves the stated reading-independence. For the finite module categories of Finite-dimensional module categories satisfy the intrinsic finiteness conditions the stronger reading is available in any case, since by [F11] every simple module there has a projective cover, so the two readings coincide there. The proof selects only the finitely many supplied maps $Q_{i} ↠ S_{i}$ and finitely many biproduct and lifting data inside finite-dimensional hom-spaces, so no choice principle is used beyond them.

Depends on

Used by

Finite abelian categories admit finite-dimensional module models Theorem

Dependency tree · two levels

82 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

Etingof, Gelaki, Nikshych, Ostrik, Tensor Categories, §1.8 (Definitions 1.8.1–1.8.6, Proposition 1.8.10, Corollary 1.8.11, Remark 1.8.7), printed pp.9–11 (standard reference, not scraped)
Fuchs, Schaumann, Schweigert, Eilenberg–Watts calculus for finite categories and a bimodule Radford S^4 theorem, arXiv:1612.04561v3, §2.1 (Lemma 2.1, Lemma 2.2, Corollary 2.3, equation (2.1)) (standard reference, not scraped)