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.

Finite abelian categories admit finite-dimensional module models

Statement

Let $C$ be a finite $k$ -linear abelian category, let $S_{1}, \dots, S_{n}$ be representatives of its simple objects with chosen projective covers $Q_{i} ↠ S_{i}$ , and put $P = ⨁_{i} Q_{i}$ and $A = {End}_{C} (P)^{o p}$ . Then $A$ is a finite-dimensional unital $k$ -algebra and $H = C (P, -) : C \to A - m o d$ is a fully faithful, essentially surjective $k$ -linear functor, where $A - m o d$ is the category of finite-dimensional left $A$ -modules: $H$ is faithful, full and exact, and every finite-dimensional left $A$ -module is isomorphic to $H (X)$ for some object $X$ of $C$ , with the preimage exhibited by the finite-presentation construction in the proof. If a splitting of essential surjectivity is additionally supplied — an object $X_{V}$ and an isomorphism $H (X_{V}) \to V$ for every target module $V$ — then $H$ is a $k$ -linear equivalence in the specified-quasi-inverse sense of Equivalence, quasi-inverse, and adjoint equivalence of categories. Conversely any such $k$ -linear equivalence from a finite-dimensional module category transfers the intrinsic finiteness conditions, so the usual equivalence formulation holds when these splitting data are supplied. Fullness, faithfulness, exactness and objectwise essential surjectivity use only finite choices. Selecting finite presentations separately for each $V$ does not itself supply a simultaneous splitting; no choice-free existence of that splitting is asserted.

Facts & Assumptions

Given: A field $k$ , a finite $k$ -linear abelian category $C$ , simple representatives $S_{1}, \dots, S_{n}$ for its simple objects, chosen projective covers $Q_{i} ↠ S_{i}$ , and the objects $P = ⨁_{i} Q_{i}$ , $A = {End}_{C} (P)^{o p}$ and functor $H = C (P, -)$ .

[F1]

$C$ is locally finite: every object has finite length and every hom-space is finite-dimensional over $k$ ; $C$ is additive, so hom-sets are abelian groups with bilinear composition (Finite k-linear abelian categories, Locally finite k-linear abelian categories, k-linear categories and k-linear functors, Abelian category).

[F2]

A finite biproduct is at once a product and a coproduct: morphisms out of $⨁_{j} A_{j}$ are determined by their components, morphisms into it by their components, ${p r}_{i} {i n j}_{j} = δ_{i j}$ , and every morphism $h : A \to ⨁_{j} A_{j}$ equals $\sum_{j} {i n j}_{j} \circ ({p r}_{j} \circ h)$ (Biproduct, The direct sum of an indexed family of modules).

[F3]

$P$ is projective and a generator (separating); consequently $H = C (P, -)$ is exact and faithful, and every object $X$ of $C$ admits an epimorphism $P^{r} ↠ X$ for some $r \geq 0$ (Intrinsic finite category hypotheses give a finite projective generator, Projective object characterisations, Generator and cogenerator of a category, Projective object, Projective epimorphisms onto the simples generate every finite-length object).

[F4]

$A$ is a finite-dimensional unital $k$ -algebra, $H$ takes values in finite-dimensional left $A$ -modules, and the action of $a \in A$ on $h \in H (X)$ is $a \cdot h = h \circ a$ ; the component map $H (P^{m}) \to A^{m}$ , $h \mapsto ({p r}_{j} \circ h)_{j \leq m}$ , is an isomorphism of left $A$ -modules, because the left action of $A$ on ${End}_{C} (P)$ is $(a \cdot b) = b \circ a$ and $A$ acts componentwise on $A^{m}$ (Intrinsic finite category hypotheses give a finite projective generator, Endomorphisms of an object of a preadditive category form a ring, k-linear categories and k-linear functors).

[F5]

A sequence $P^{s} \overset{d}{\to} P^{r} \overset{q}{\to} X \to 0$ in an abelian category is exact exactly when $q$ is a cokernel of $d$ ; the cokernel universal property says that a morphism $g$ with $g d = 0$ factors uniquely as $g = u q$ (Kernels and cokernels in a category with zero morphisms as equalizers and coequalizers, Exact sequences and short exact sequences of modules, The quotient of an object by a subobject, Image and coimage in a category with kernels and cokernels).

[F6]

For a left module $M$ over a unital ring, the universal property of the direct sum identifies ${Hom}_{R} (R^{r}, M)$ with $M^{r}$ : an $R$ -linear map $R^{r} \to M$ is determined by, and may be prescribed arbitrarily on, the standard generators, and the correspondence is additive in the family (no pointwise left $R$ -module structure on ${Hom}_{R} (R^{r}, M)$ is asserted) (Universal property of a direct sum of modules, Generated submodule, cyclic and finitely generated modules, module basis and free module, Every module is a quotient of a free module).

[F7]

A finite-dimensional left $A$ -module $V$ is finitely generated: a finite $k$ -basis generates it, giving an epimorphism $A^{t} ↠ V$ ; its kernel is a submodule of the finite-dimensional $k$ -space $A^{t}$ , hence finite-dimensional and again finitely generated, so $V$ admits a finite presentation $A^{u} \to A^{t} \to V \to 0$ (Generated submodule, cyclic and finitely generated modules, module basis and free module, Every module is a quotient of a free module, Module homomorphism and isomorphism, kernel, image and cokernel, Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis).

[F8]

A functor is an equivalence exactly when it is fully faithful and split essentially surjective, the splitting being supplied data (A functor is an equivalence exactly when it is fully faithful and split essentially surjective, without Choice, Faithful, full, fully faithful, essentially surjective, and split essentially surjective functors, Equivalence, quasi-inverse, and adjoint equivalence of categories).

[F9]

An equivalence of categories preserves and reflects every existing limit and colimit, hence the zero object, kernels, cokernels, images and finite biproducts; a fully faithful functor reflects isomorphisms (Equivalences preserve, reflect, and create limits and colimits in the isomorphism-invariant sense, Every fully faithful functor reflects isomorphisms, Initial object, terminal object, and zero object, Biproduct).

[F10]

In an abelian category a morphism is monic if and only if its kernel is zero and epic if and only if its cokernel is zero; the subobjects of an object are its monomorphisms modulo mutual factorisation, and the join of subobjects represented by $b : B ↣ A$ and $c : C ↣ A$ is the image inclusion of the map $[b, c] : B \oplus C \to A$ (In an abelian category, monic means zero kernel and epic means zero cokernel, Subobject and quotient object as mutual-factorisation classes of monomorphisms and epimorphisms, The join of two subobjects in an abelian category, Image and coimage in a category with kernels and cokernels).

Proof

technique · direct

1.1F1F2F4given

(H is a $k$ -linear functor into $A - m o d$ .) The functor $H = C (P, -)$ sends an object $X$ to the hom-group $C (P, X)$ , which by [F1] is a finite-dimensional $k$ -vector space, and the action $a \cdot h = h \circ a$ of [F4] makes it a left $A$ -module; for a morphism $u : X \to Y$ , $H (u) = u \circ (-)$ is additive and $k$ -linear by [F1] and $A$ -linear because $u \circ (h \circ a) = (u \circ h) \circ a$ . Hence $H$ is a $k$ -linear functor $C \to A - m o d$ . Moreover for each $m$ the component map identifies $H (P^{m}) = C (P, P^{m})$ with $A^{m}$ as a left $A$ -module: it is a bijection by the product universal property of the biproduct [F2], and it is $A$ -linear since $(a \cdot h)_{j} = {p r}_{j} \circ h \circ a = a \cdot ({p r}_{j} \circ h)$ for the componentwise action on $A^{m}$ [F4].

1.2F3given

(Exactness and faithfulness.) By [F3] the object $P$ is projective, so $H = C (P, -)$ preserves kernels and cokernels of short exact sequences, that is, $H$ is exact; and $P$ is separating, which by [F3] says exactly that $H$ is injective on every hom-set, so $H$ is faithful.

1.3F9F10given

(The locally finite conditions transfer along the equivalence.) Let $D$ be a $k$ -linear abelian category and $E : A - m o d \to D$ a $k$ -linear equivalence, with quasi-inverse $E^{'}$ and unit and counit isomorphisms. By [F9] the functor $E$ preserves and reflects kernels, cokernels, images, finite biproducts and the zero object, and being fully faithful it reflects isomorphisms; by [F10] it therefore preserves and reflects monomorphisms and epimorphisms, and it carries a factor $M / N = coker (N ↣ M)$ to $E (M) / E (N) = coker (E (N) ↣ E (M))$ . The subobjects of $M$ are the monomorphisms into $M$ modulo mutual factorisation, so $E$ induces an order-preserving bijection between the subobjects of $M$ and of $E (M)$ , and since simplicity says that the only subobjects are the zero subobject and the identity, simplicity is preserved and reflected as well. Hence for $X \in D$ , written as $X ≅ E (M)$ with $M = E^{'} (X)$ via the counit, a composition series $0 = M_{0} < \dots < M_{ℓ} = M$ of $M$ , which exists because $M$ is a finite-dimensional left $A$ -module and $A - m o d$ is intrinsically finite (Finite-dimensional module categories satisfy the intrinsic finiteness conditions), maps to a strictly increasing chain $0 ≅ E (M_{0}) < \dots < E (M_{ℓ}) ≅ X$ whose successive factors $E (M_{i + 1}) / E (M_{i}) ≅ E (M_{i + 1} / M_{i})$ are simple, so $X$ has finite length in $D$ . Finally ${Hom}_{D} (E (M), E (N)) ≅ {Hom}_{A} (M, N)$ is a $k$ -linear bijection because $E$ is fully faithful, so every hom-space of $D$ is finite-dimensional.

2.1F2F5F6step 1.1step 1.2chooseconstruct

(Fullness.) Let $X, Y \in C$ and let $φ : H (X) \to H (Y)$ be $A$ -linear. By [F3] choose an epimorphism $q : P^{r} ↠ X$ and then an epimorphism $P^{s} ↠ \ker q$ , and let $d : P^{s} \to P^{r}$ be the composite with the inclusion $\ker q ↣ P^{r}$ , so that $P^{s} \overset{d}{\to} P^{r} \overset{q}{\to} X \to 0$ is exact and $q$ is a cokernel of $d$ by [F5]. Since $H$ is exact by step 1.2, $H (q) : H (P^{r}) \to H (X)$ is the cokernel of $H (d)$ and in particular an epimorphism, and $ψ : = φ \circ H (q) : H (P^{r}) \to H (Y)$ is $A$ -linear. Under the identification $H (P^{r}) ≅ A^{r}$ of step 1.1 the free-module universal property [F6] presents $ψ$ by the $r$ -tuple $y_{j} : = ψ ({i n j}_{j}) : P \to Y$ , and by the coproduct universal property of $P^{r} = ⨁_{j} P$ [F2] there is $g : P^{r} \to Y$ with $g \circ {i n j}_{j} = y_{j}$ . Then $ψ = H (g)$ : for $h : P \to P^{r}$ with components $a_{j} : = {p r}_{j} \circ h \in A$ , step 1.1 gives $h = \sum_{j} {i n j}_{j} \circ a_{j} = \sum_{j} a_{j} \cdot {i n j}_{j}$ , so $ψ (h) = \sum_{j} a_{j} \cdot ψ ({i n j}_{j}) = \sum_{j} y_{j} \circ a_{j} = g \circ h$ by $A$ -linearity and additivity of $ψ$ . Now $ψ \circ H (d) = φ \circ H (q) \circ H (d) = φ \circ H (q \circ d) = 0$ because $q \circ d = 0$ , that is $H (g \circ d) = 0$ , and $H$ is faithful by step 1.2, so $g \circ d = 0$ . By the cokernel universal property [F5] for $X = coker (d)$ there is $u : X \to Y$ with $g = u \circ q$ , and then $H (u) \circ H (q) = H (u \circ q) = H (g) = ψ = φ \circ H (q)$ ; since $H (q)$ is an epimorphism, $H (u) = φ$ . Hence every $A$ -linear map $H (X) \to H (Y)$ is $H (u)$ for some $u : X \to Y$ , so $H$ is full.

2.2F9F10step 1.3

(Simple classes and projective covers transfer.) Keep the equivalence $E : A - m o d \to D$ of step 1.3. Since $E$ is full, faithful and essentially surjective it induces a bijection between the isomorphism classes of objects of the two categories, and by step 1.3 it preserves and reflects simplicity, so $D$ has exactly as many isomorphism classes of simple objects as $A - m o d$ , namely finitely many by Finite-dimensional module categories satisfy the intrinsic finiteness conditions. For enough projectives let $S$ be a simple object of $D$ and write $S ≅ E (M)$ with $M$ simple by step 1.3; the finite-dimensional $A$ -module $M$ has a projective cover $π : Q ↠ M$ by Finite-dimensional module categories satisfy the intrinsic finiteness conditions, that is, an essential epimorphism with $Q$ projective in $A - m o d$ . The object $E (Q)$ is projective in $D$ : a lifting problem $f : E (Q) \to Z$ against an epimorphism $q : Y ↠ Z$ transports under the quasi-inverse $E^{'}$ — which preserves epimorphisms by [F9] — to a lifting problem for the projective $Q$ , and the lift transports back along $E$ using the naturality of the counit. Moreover $\ker E (π) ≅ E (\ker π)$ because $E$ preserves kernels, and $E (\ker π)$ is a superfluous subobject of $E (Q)$ : subobjects correspond bijectively under $E$ by step 1.3, $E$ preserves joins because a join is the image of a map out of a finite biproduct [F10], and the superfluity condition of Superfluous subobjects and projective covers in an abelian category is therefore carried across, so $E (π)$ is an essential epimorphism with projective source, a projective cover of $E (M) ≅ S$ .

3.1F5F7step 1.1step 2.1given

(Essential surjectivity.) Let $V$ be a finite-dimensional left $A$ -module. By [F7] $V$ admits a finite presentation $A^{u} \overset{δ}{\to} A^{t} \overset{ε}{\to} V \to 0$ with $V ≅ coker (δ)$ . By step 2.1 the functor $H$ is full and faithful, so it is bijective on hom-sets and, under the identification $H (P^{m}) ≅ A^{m}$ of step 1.1, the map ${Hom}_{C} (P^{u}, P^{t}) \to {Hom}_{A} (A^{u}, A^{t})$ , $d \mapsto H (d)$ , is a bijection; let $d : P^{u} \to P^{t}$ be the morphism with $H (d) = δ$ and put $X : = coker (d)$ , which exists because $C$ is abelian. Exactness of $H$ (step 1.2) gives $H (X) ≅ coker (H (d)) = coker (δ) ≅ V$ , so every finite-dimensional left $A$ -module is isomorphic to $H (X)$ for some $X \in C$ .

4.1F8step 1.1step 1.2step 2.1step 3.1givenconstruct

(Conclusion of the equivalence.) Steps 1.1, 1.2, 2.1 and 3.1 prove that $H$ is $k$ -linear, exact, fully faithful and essentially surjective, with $A$ finite-dimensional. For the further equivalence assertion assume supplied objects $X_{V}$ and isomorphisms $ε_{V} : H (X_{V}) \to V$ for every target module $V$ . Put $G (V) = X_{V}$ ; for $f : V \to W$ , fullness and faithfulness give a unique $G (f)$ satisfying $H (G (f)) = ε_{W}^{- 1} f ε_{V}$ . Uniqueness proves functoriality and $k$ -linearity, and [F8] gives the unit isomorphism and hence the equivalence. Step 3.1 establishes each witness separately; it does not choose this entire family.

5.1step 4.1step 1.3step 2.2F8F9F10given∎

(Conclusion.) Steps 1.3 and 2.2 show that a $k$ -linear equivalence from $A - m o d$ transfers local finiteness, finitely many simple classes and projective covers, hence intrinsic finiteness. In the other direction step 4.1 gives the equivalence when splitting data are supplied, and unconditionally gives the fully faithful, essentially surjective module-model functor. The objectwise arguments choose only finite bases, presentations, covers and lifts. The simultaneous splitting is additional data, not a consequence of finite choice.

Depends on

Used by

Dependency tree · two levels

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