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.

Degreewise direct sums and homogeneous free covers in graded modules

Statement

Let $k$ be a commutative ring and $A$ a graded $k$ -algebra (Associative graded algebras, bimodules, and internal shifts).

For every family $(X_{i})_{i \in I}$ of graded left $A$ -modules the degreewise direct sum, defined by $(⨁_{i \in I} X_{i})_{d} : = ⨁_{i \in I} (X_{i})_{d}$ with componentwise action, is a graded left $A$ -module and is the coproduct of the family in ${GrMod}_{0} (A)$ : the coordinate inclusions are degree-zero $A$ -linear and every family of degree-zero $A$ -linear maps $X_{i} \to Y$ assembles to a unique degree-zero $A$ -linear map $⨁_{i} X_{i} \to Y$ . In particular ${GrMod}_{0} (A)$ has all small coproducts, computed degreewise and agreeing with the finite biproducts of Graded modules with degree-zero maps form an abelian category; for $I = \emptyset$ the coproduct is the zero module. No choice is used.
For every $d \in Z$ the shifted regular module $A {d}$ is free on the homogeneous generator $1_{A} \in (A {d})_{d}$ : for every graded left $A$ -module $X$ and every $x \in X_{d}$ there is a unique degree-zero $A$ -linear map $ℓ_{x} : A {d} \to X$ with $ℓ_{x} (1_{A}) = x$ , namely $ℓ_{x} (a) = a x$ .
Consequently every graded left $A$ -module $X$ has a canonical homogeneous free cover: let $H_{X}$ be the set of nonzero homogeneous elements of $X$ , so that each $x \in H_{X}$ has a unique degree $\deg x$ with $x \in X_{\deg x}$ , and put $P_{X} : = ⨁_{x \in H_{X}} A {\deg x} .$ The degree-zero $A$ -linear map $q_{X} : P_{X} ⟶ X, q_{X} (e_{x}) = x,$ is an epimorphism, its kernel $K_{X} = \ker q_{X}$ is a graded submodule and hence a graded left $A$ -module, and applying the same construction to $K_{X}$ gives an exact sequence $Free (K_{X}) \overset{d}{\to} P_{X} \overset{q_{X}}{\to} X ⟶ 0$ in ${GrMod}_{0} (A)$ whose first map is not asserted to be monic. The cover is indexed by the actual nonzero homogeneous elements of $X$ , so no generator, basis or resolution is chosen.

Facts & Assumptions

Given: A commutative ring $k$ , a graded $k$ -algebra $A$ , a family $(X_{i})_{i \in I}$ of graded left $A$ -modules, a graded left $A$ -module $Y$ , an integer $d$ and an element $x \in X_{d}$ .

[L1]

Graded $k$ -algebras, graded modules with $X = ⨁_{d} X_{d}$ and $A_{i} X_{d} \subseteq X_{i + d}$ , degree-zero maps, graded submodules with pieces $S_{d} = S \cap M_{d}$ , and the internal shift $(M {r})_{e} = M_{e - r}$ are defined in Associative graded algebras, bimodules, and internal shifts.

[L2]

The direct sum of a family of left modules is the submodule of the product consisting of the finitely supported families, it carries the coordinate inclusions $ȷ_{i}$ , and for the empty index set both the product and the direct sum are the zero module (The direct sum of an indexed family of modules).

[L3]

A family of homomorphisms $f_{i} : M_{i} \to N$ out of the summands of a direct sum has a unique assembly $f$ with $f \circ ȷ_{i} = f_{i}$ , given by $f ((m_{i})) = \sum_{i} f_{i} (m_{i})$ (Universal property of a direct sum of modules).

[L4]

For a unital ring $R$ and a set $X$ the free left $R$ -module on $X$ is $R^{(X)} = ⨁_{x \in X} R$ , with standard basis inclusion $x \mapsto e_{x}$ , and a family $(b_{x})$ is a basis when every element is uniquely a finite $R$ -linear combination of the $b_{x}$ (The free module on a set and its standard basis).

[L5]

Every set map $u : X \to M$ into a left $R$ -module extends uniquely to an $R$ -module homomorphism $\overset{ˉ}{u} : R^{(X)} \to M$ with $\overset{ˉ}{u} (e_{x}) = u (x)$ (Universal property of the free module on a set).

[L6]

In ${GrMod}_{0} (A)$ kernels, images, cokernels and finite biproducts are computed in each homogeneous degree: for a degree-zero $f$ one has $\ker f = ⨁_{d} \ker (f_{d})$ and $im f = ⨁_{d} im (f_{d})$ , the binary biproduct is the graded module with pieces $M_{d} \oplus N_{d}$ , exactness is equivalent to exactness degreewise, and the category is abelian (Graded modules with degree-zero maps form an abelian category).

[L7]

For a module homomorphism $f$ its kernel is ${m : f (m) = 0}$ and its image is ${f (m)}$ , and the cokernel is the quotient by the image (Module homomorphism and isomorphism, kernel, image and cokernel).

[L8]

An abelian category is an additive category, that is, a preadditive category with all finite biproducts, in which every morphism has a kernel and a cokernel and the canonical comparison from the coimage to the image is an isomorphism (Abelian category).

Proof

technique · direct

1.1L1L2algebra

Give the direct sum $X : = ⨁_{i \in I} X_{i}$ of the underlying left $A$ -modules its componentwise action $a \cdot (x_{i})_{i \in I} : = (a x_{i})_{i \in I}$ ; this is a left $A$ -module structure preserving finite supports, and with $X_{d} : = ⨁_{i \in I} (X_{i})_{d}$ one has $X = ⨁_{d \in Z} X_{d}$ : every element of $X$ is a finite sum of elements of the subgroups $X_{d}$ , and if $\sum_{d} x^{(d)} = 0$ with $x^{(d)} \in X_{d}$ then in each coordinate $\sum_{d} x_{i}^{(d)} = 0$ with $x_{i}^{(d)} \in (X_{i})_{d}$ , so $x_{i}^{(d)} = 0$ for all $i, d$ by the directness of each $X_{i} = ⨁_{d} (X_{i})_{d}$ .

1.2L1L4L5algebra

The shifted regular module $A {d}$ has the same underlying left $A$ -module as $A$ , which is free on the single standard basis element $1_{A}$ , and a left $A$ -module map out of it is uniquely determined by the image of $1_{A}$ ; for every $e$ the map $ℓ_{x} (a) : = a x$ sends $(A {d})_{e} = A_{e - d}$ into $X_{e}$ because $A_{e - d} x \subseteq X_{e}$ , so it is degree-zero $A$ -linear with $ℓ_{x} (1_{A}) = x$ , and every degree-zero $A$ -linear $φ : A {d} \to X$ with $φ (1_{A}) = x$ satisfies $φ (a) = a φ (1_{A}) = a x$ .

2.1step 1.1L3

Every family of degree-zero $A$ -linear maps $f_{i} : X_{i} \to Y$ assembles by [L3] to the unique $A$ -linear $f : X \to Y$ with $f \circ ȷ_{i} = f_{i}$ , namely $f ((x_{i})_{i \in I}) = \sum_{i} f_{i} (x_{i})$ ; it is degree-zero because for $x = (x_{i}) \in X_{d}$ all components satisfy $x_{i} \in (X_{i})_{d}$ , whence $f_{i} (x_{i}) \in Y_{d}$ and $f (x) \in Y_{d}$ , and it is the unique degree-zero $A$ -linear map with the prescribed composites, so $X$ is the coproduct of the family.

2.2step 1.1L1

Since $A_{i} (X_{j})_{d} \subseteq (X_{j})_{i + d}$ for all $i, d, j$ , the componentwise action satisfies $A_{i} X_{d} \subseteq X_{i + d}$ , so $X$ is a graded left $A$ -module; the coordinate inclusion $ȷ_{j} : X_{j} \to X$ maps $(X_{j})_{d}$ into $X_{d}$ , so it is degree-zero $A$ -linear.

3.1step 2.1L2L8

For $I = \emptyset$ the direct sum is the zero module by [L2], and the unique map from a zero module to $Y$ is $A$ -linear and degree-zero, so the zero module is initial and is the coproduct of the empty family; together with step 2.1 this shows that the degreewise direct sum is the coproduct of every family, so ${GrMod}_{0} (A)$ has all small coproducts.

3.2step 1.1step 2.2L6L8

Suppose $I$ is finite. Then $X$ is also the product of the family: given degree-zero $A$ -linear maps $g_{i} : Y \to X_{i}$ , the elementwise map $g (y) : = (g_{i} (y))_{i \in I}$ has finite support in $X$ , is $A$ -linear and degree-zero, and is the unique such map with $π_{i} \circ g = g_{i}$ for the coordinate projections $π_{i}$ ; for two summands $X$ has pieces $X_{d} = (X_{1})_{d} \oplus (X_{2})_{d}$ with the same coordinate inclusions and projections as the binary biproduct of [L6], and the finite case follows by iterating that identification, so the coproducts here agree with the finite biproducts computed in [L6].

3.3step 1.2step 2.1step 2.2L1

Let $H_{X}$ be the set of nonzero homogeneous elements of $X$ ; each $x \in H_{X}$ has a unique degree $\deg x$ with $x \in X_{\deg x}$ , since $x \in X_{d} \cap X_{e}$ with $x \neq 0$ and $d \neq e$ would exhibit $x$ as two different finite decompositions of one element. Hence $P_{X} : = ⨁_{x \in H_{X}} A {\deg x}$ is a graded left $A$ -module by steps 1.1 and 2.2, and by step 2.1 and step 1.2 the maps $ℓ_{x} : A {\deg x} \to X$ assemble to the unique degree-zero $A$ -linear $q_{X} : P_{X} \to X$ with $q_{X} (e_{x}) = x$ for each $x \in H_{X}$ .

4.1step 3.3algebra

The map $q_{X}$ is surjective, hence an epimorphism: every $x^{'} \in X$ is the finite sum of its nonzero homogeneous components $x^{(d)} \in H_{X}$ , and $q_{X} (e_{x^{(d)}}) = x^{(d)}$ ; and two degree-zero $A$ -linear maps out of $X$ agreeing after composition with a surjection agree everywhere.

5.1step 3.3step 4.1L1L6L7

The kernel $K_{X} = \ker q_{X}$ is $⨁_{d} \ker ((q_{X})_{d})$ by [L6], hence a graded submodule of $P_{X}$ and therefore a graded left $A$ -module with pieces $K_{X} \cap (P_{X})_{d}$ ; applying the construction of steps 3.3 and 4.1 to $K_{X}$ produces $Free (K_{X}) : = P_{K_{X}}$ and a degree-zero $A$ -linear epimorphism $q_{K_{X}} : P_{K_{X}} \to K_{X}$ , whose composite $d$ with the inclusion $K_{X} \to P_{X}$ is degree-zero $A$ -linear with image $K_{X}$ .

6.1step 3.1step 3.2step 5.1L7∎

Therefore $im d = K_{X} = \ker q_{X}$ while $im q_{X} = X$ by step 4.1, so the sequence $Free (K_{X}) \overset{d}{\to} P_{X} \overset{q_{X}}{\to} X \to 0$ is exact at $P_{X}$ and at $X$ ; the map $d$ is not asserted monic, the indexing set $H_{X}$ and the degrees $\deg x$ are determined by $X$ , and the direct sums are indexed by those elements, so no generator, basis, resolution or other choice is made.

Depends on

Used by

Dependency tree · two levels

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