LemmaStatement: 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-support families of finite-dimensional vector spaces are locally finite but not finite

Statement

Let $k$ be a field and let $C$ be the category whose objects are the families $(V_{n})_{n \in N}$ of finite-dimensional $k$ -vector spaces with $V_{n} = 0$ for all but finitely many $n$ , and whose morphisms $(V_{n}) \to (W_{n})$ are the families $(f_{n} : V_{n} \to W_{n})$ of $k$ -linear maps, with componentwise identities and composition. Then $C$ is a $k$ -linear abelian category in which kernels, cokernels and finite biproducts are computed componentwise; every hom-space is finite-dimensional over $k$ ; every object has finite length; every object is projective, hence every simple object has a projective cover; and the objects $S_{m}$ with $(S_{m})_{m} = k$ and $(S_{m})_{n} = 0$ for $n \neq m$ are pairwise non-isomorphic simple objects. Consequently $C$ is locally finite and has enough projectives, but it has infinitely many isomorphism classes of simple objects and no object of $C$ is a generator, so $C$ is not a finite $k$ -linear abelian category. No choice is used.

Facts & Assumptions

Given: A field $k$ , the category $k - M o d$ of $k$ -vector spaces, the product category $P = \prod_{n \in N} k - M o d$ (Product category and its projection functors), and its full subcategory $C$ on the families $(V_{n})$ with every $V_{n}$ finite-dimensional and $V_{n} = 0$ for all but finitely many $n$ . For an object $V$ write $supp V = {n : V_{n} \neq 0}$ , a finite set by hypothesis, and write $d (V) = \sum_{n} \dim_{k} V_{n}$ .

[F1]

$k - M o d$ is the category of modules over the field $k$ and is abelian (Modules over a ring form an abelian category).

[F2]

Every set-indexed product of abelian categories is abelian, with the zero object, finite biproducts, kernels and cokernels computed componentwise (A small product of abelian categories is abelian, Product category and its projection functors).

[F3]

For a homomorphism $f : M \to N$ of $k$ -modules, $\ker f$ is a submodule of $M$ , $im f$ is a submodule of $N$ , and $f$ is injective if and only if $\ker f = {0_{M}}$ ; the cokernel is $coker f = N / im f$ (Module homomorphism and isomorphism, kernel, image and cokernel, Kernels and images of module homomorphisms are submodules, and injectivity is equivalent to trivial kernel).

[F4]

In an abelian category a morphism is monic exactly when its kernel is zero, and epic exactly when its cokernel is zero (In an abelian category, monic means zero kernel and epic means zero cokernel).

[F5]

A linear subspace of a finite-dimensional space is finite-dimensional, and $\dim_{F} V = \dim_{F} (\ker T) + \dim_{F} (im T)$ for a linear $T$ on a finite-dimensional $V$ (If $\dim_{F} V = n$ and $U$ is a linear subspace of $V$ , then $U$ is finite-dimensional, $\dim_{F} U \leq n$ , and $\dim_{F} U = n$ if and only if $U = V$ , Rank-nullity: $\dim_{F} V = nullity T + rank T$ ).

[F6]

A finite-dimensional $k$ -vector space has a finite ordered basis, and a $k$ -linear map on such a space is uniquely determined by, and may be prescribed arbitrarily on, the elements of an ordered basis (Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis, A finite list $v : n \to V$ is an ordered basis if and only if every $x \in V$ equals $\sum_{i < n} λ_{i} v_{i}$ for exactly one $λ : n \to F$ ; those scalars are the coordinates of $x$ in that ordered basis).

[F7]

For finite-dimensional $k$ -vector spaces $V, W$ one has $\dim_{k} L (V, W) = (\dim_{k} V) (\dim_{k} W)$ , and the dimension of a finite internal direct sum is the sum of the dimensions of its summands ( $\dim_{F} M_{m \times n} (F) = m n$ and $\dim_{F} L (V, W) = (\dim_{F} V) (\dim_{F} W)$ for finite-dimensional $V, W$ , If $V = ⨁_{i < n} U_{i}$ with every $U_{i}$ finite-dimensional, then $V$ is finite-dimensional and $\dim_{F} V = \sum_{i < n} \dim_{F} U_{i}$ ; in particular $\dim_{F} (U \oplus W) = \dim_{F} U + \dim_{F} W$ ).

[F8]

A subcategory is full when it contains every morphism between its objects that exists in the ambient category (Subcategory and full subcategory).

Proof

technique · direct

1.1F1F2F8given

The category $k - M o d$ is abelian by [F1], so the product category $P = \prod_{n \in N} k - M o d$ is abelian by [F2], with zero object, finite biproducts, kernels and cokernels computed componentwise; $C$ is by definition the full subcategory of $P$ on the families that are finite-dimensional in every degree and zero in all but finitely many degrees.

1.2F7givenalgebra

The family of zero spaces is an object of $C$ and is the zero object of $P$ , and if $V, W \in C$ then the componentwise family $(V_{n} \oplus W_{n})$ lies in $C$ , because $supp (V \oplus W) \subseteq supp V \cup supp W$ is finite and $\dim_{k} (V_{n} \oplus W_{n}) = \dim_{k} V_{n} + \dim_{k} W_{n}$ by [F7] is finite in every degree; the biproduct morphisms of $P$ are the componentwise ones, so $C$ contains the zero object and is closed under finite biproducts computed in $P$ .

1.3F2F3F5givenalgebra

Let $f : V \to W$ be a morphism in $C$ . Its kernel in $P$ is the family $(\ker f_{n})$ of [F3] with the canonical inclusions, whose support lies in the finite set $supp V$ , and $\ker f_{n}$ is a subspace of the finite-dimensional space $V_{n}$ , hence finite-dimensional by [F5]; its cokernel in $P$ is the family $(coker f_{n}) = (W_{n} / im f_{n})$ of [F3], whose support lies in the finite set $supp W$ , and $\dim_{k} (W_{n} / im f_{n}) = \dim_{k} W_{n} - \dim_{k} (im f_{n}) < \infty$ by rank-nullity [F5]. Hence both the kernel and the cokernel in $P$ of a morphism of $C$ are objects of $C$ with their canonical maps, so $C$ is closed under kernels and cokernels of its morphisms computed in $P$ .

1.4F7given

For $V, W \in C$ the set ${Hom}_{C} (V, W)$ is the product $\prod_{n \in N} L (V_{n}, W_{n})$ , which is a finite product over the finite set $supp V \cup supp W$ because $L (0, X)$ and $L (X, 0)$ are the zero space; identified with the finite direct sum $⨁_{n \in supp V \cup supp W} L (V_{n}, W_{n})$ it is a finite-dimensional $k$ -vector space with $\dim_{k} {Hom}_{C} (V, W) = \sum_{n} (\dim_{k} V_{n}) (\dim_{k} W_{n})$ by [F7]. Composition is componentwise, hence $k$ -bilinear, so $C$ is a locally small $k$ -linear category in which every hom-space is finite-dimensional over $k$ .

1.5F8givenconstruct

A family $(u_{n}) : (V_{n}) \to (W_{n})$ of linear maps is an isomorphism in $C$ exactly when every $u_{n}$ is a linear isomorphism, and then $(u_{n}^{- 1})$ is its inverse; for $m \in N$ let $S_{m}$ be the object with $(S_{m})_{m} = k$ and $(S_{m})_{n} = 0$ for $n \neq m$ , so that $S_{m} \neq 0$ .

2.1F8step 1.1step 1.2step 1.3algebra

By steps 1.1, 1.2 and 1.3 the full subcategory $C$ of the abelian category $P$ contains the zero object and is closed under finite biproducts, kernels and cokernels computed in $P$ , so it is an abelian subcategory of $P$ in the sense of Abelian subcategory and exact embedding. Consequently it is itself abelian: hom-sets are abelian groups with bilinear composition inherited from $P$ , the zero object and finite biproducts of $C$ are those of $P$ , every morphism of $C$ has its $P$ -kernel and $P$ -cokernel in $C$ , and its image and coimage, being built from those kernels and cokernels (Image and coimage in a category with kernels and cokernels), are also objects of $C$ , with the canonical comparison an isomorphism in $P$ whose inverse is a morphism of $C$ by fullness [F8]; this is exactly additivity with invertible image-coimage comparison, so $C$ is abelian (Abelian category).

3.1F3F4step 2.1algebra

In the abelian category $C$ the kernel and cokernel of a morphism are computed componentwise, as in step 1.3; by [F4] a morphism $u : V \to W$ of $C$ is monic if and only if $\ker u = 0$ , that is if and only if $\ker u_{n} = 0$ for every $n$ , which by [F3] holds exactly when every $u_{n}$ is injective; and $u$ is epic if and only if $coker u = 0$ , that is if and only if $W_{n} = im u_{n}$ for every $n$ , which holds exactly when every $u_{n}$ is surjective.

4.1F6step 3.1chooseconstructalgebra

Every object $V$ of $C$ is projective (Projective object): let $q : E \to M$ be an epimorphism and $f : V \to M$ a morphism in $C$ ; by step 3.1 each $q_{n} : E_{n} \to M_{n}$ is surjective. For each $n \in supp V$ choose an ordered basis $(v_{n, 1}, \dots, v_{n, d_{n}})$ of $V_{n}$ (possible since $V_{n}$ is finite-dimensional) and for each $j \leq d_{n}$ choose $e_{n, j} \in E_{n}$ with $q_{n} (e_{n, j}) = f_{n} (v_{n, j})$ ; finitely many such choices are made. By [F6] there is for each such $n$ a unique linear $g_{n} : V_{n} \to E_{n}$ with $g_{n} (v_{n, j}) = e_{n, j}$ , and set $g_{n} = 0$ for the remaining $n$ ; then $q_{n} g_{n} = f_{n}$ for $n \in supp V$ because both sides agree on the basis $(v_{n, j})$ , and for the remaining $n$ both sides are zero, so the family $(g_{n})$ is a morphism of $C$ with $q \circ g = f$ . Thus every morphism into $M$ lifts along every epimorphism $q$ , so $V$ is projective.

4.2F5step 1.5step 3.1algebra

For every $m$ the object $S_{m}$ of step 1.5 is simple (Simple object): it is nonzero, and if $u : T \to S_{m}$ is a monomorphism in $C$ then every $u_{n}$ is injective by step 3.1; for $n \neq m$ the target $(S_{m})_{n}$ is zero, so an injective map into it has zero domain and $T_{n} = 0$ , while a nonzero subobject has $T \neq 0$ , hence $T_{m} \neq 0$ ; then $u_{m} : T_{m} \to k$ is an injective linear map with nonzero finite-dimensional domain, so $\dim_{k} T_{m} \leq 1$ and $\dim_{k} T_{m} \geq 1$ , whence $u_{m}$ is an isomorphism and so is $u$ by step 1.5. Therefore the only subobjects of $S_{m}$ are the zero subobject and $1_{S_{m}}$ , so $S_{m}$ is simple.

5.1step 4.2algebra

Conversely, if $V \in C$ is simple, then $V \neq 0$ gives $V_{m} \neq 0$ for some $m$ , and a nonzero vector of $V_{m}$ spans a line $L \subseteq V_{m}$ ; the object $S$ with $S_{m} = L$ and $S_{n} = 0$ for $n \neq m$ is a nonzero subobject of $V$ isomorphic to $S_{m}$ , so by simplicity the subobject $S$ equals $V$ and $V ≅ S_{m}$ . Moreover $S_{m} ≅ S_{n}$ forces $k = (S_{m})_{m} ≅ (S_{n})_{m}$ , so $(S_{n})_{m} \neq 0$ and $m = n$ . Hence the objects $S_{m}$ , $m \in N$ , form a complete set of pairwise non-isomorphic simple objects, so $C$ has infinitely many isomorphism classes of simple objects.

5.2F5step 2.1step 4.2induction

Every object $V$ of $C$ has finite length (Object of finite length): induct on the natural number $d (V) = \sum_{n} \dim_{k} V_{n}$ from step 1.4. If $d (V) = 0$ then every $V_{n} = 0$ , so $V = 0$ and the empty composition series exhibits finite length. If $d (V) > 0$ , choose $n \in supp V$ and a line $L \subseteq V_{n}$ ; the object $S$ with $S_{n} = L$ and $S_{k} = 0$ for $k \neq n$ is a simple subobject of $V$ , and the quotient $V / S$ (The quotient of an object by a subobject) is the family with $(V / S)_{n} = V_{n} / L$ and $(V / S)_{j} = V_{j}$ for $j \neq n$ , of total dimension $d (V) - 1$ ; by the induction hypothesis $V / S$ has finite length, and $S ≅ S_{n}$ has the one-step composition series $0 < S$ because it is simple by step 4.2, so the additivity theorem for lengths along a subobject (Length is additive along a subobject) gives that $V$ has finite length and $ℓ (V) = 1 + ℓ (V / S)$ .

5.3step 4.1algebra

Every simple object of $C$ has a projective cover (Superfluous subobjects and projective covers in an abelian category): if $S$ is simple then its identity $1_{S} : S \to S$ is an epimorphism whose source $S$ is projective by step 4.1, and its kernel is the zero subobject, which is superfluous because $[0] \lor [m] = [m]$ for every subobject $[m]$ , so the condition $[0] \lor [m] = [1_{S}]$ forces $[m] = [1_{S}]$ ; hence $1_{S}$ is essential and is a projective cover of $S$ .

5.4step 1.4step 4.2algebra

No object $P$ of $C$ is a generator (Generator and cogenerator of a category): choose $m \notin supp P$ , possible because $supp P$ is finite; then ${Hom}_{C} (P, S_{m}) = \prod_{n} L (P_{n}, (S_{m})_{n}) = 0$ by step 1.4, since the $m$ -th factor is $L (0, k) = 0$ . The two distinct parallel morphisms $1_{S_{m}}, 0 : S_{m} \to S_{m}$ therefore cannot be separated by any morphism $P \to S_{m}$ , so the singleton ${P}$ is not separating in the sense of Separating and coseparating sets of objects, and $P$ is not a generator.

6.1step 1.4step 2.1step 4.1step 5.1step 5.2step 5.3step 5.4given∎

By step 2.1 the category $C$ is abelian, by step 1.4 it is locally small, $k$ -linear with finite-dimensional hom-spaces, and by step 5.2 every object has finite length; hence $C$ is a locally finite $k$ -linear abelian category (Locally finite k-linear abelian categories). By step 4.1 every object is projective, hence by step 5.3 every simple object has a projective cover, so $C$ has enough projectives; by step 5.1 it has infinitely many isomorphism classes of simple objects and by step 5.4 no object is a generator, so the finiteness conditions of Finite k-linear abelian categories fail and $C$ is not a finite $k$ -linear abelian category. All bases chosen lie in finite-dimensional spaces, the hom-space products and objectwise sums reduce to finite ones; the ambient countable product uses the explicit componentwise module constructions, and no element is selected from an infinite family, so no choice is used.

Depends on

Used by

Finite length and finite Hom do not imply a finite category Counterexample

Dependency tree · two levels

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