LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge 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.

The copower presentation construction is left adjoint to the generator Hom functor

Statement

Let $C$ be a locally small cocomplete abelian category and $P$ a small projective generator of $C$ . Assume in addition that definable assignments of copowers of $P$ (including their injections) for every set, and of cokernels (including their quotient maps) for every morphism of $C$ , are supplied. Cocompleteness alone asserts their existence individually, not such simultaneous choices. Put $E = {End}_{C} (P)$ , $A = E^{o p}$ (a unital ring by Endomorphisms of an object of a preadditive category form a ring), and $H = C (P, -) : C \to A -Mod$ with the left action $(e^{o p} \cdot h) = h \circ e$ . Then there is a functor $L : A -Mod ⟶ C$ and natural bijections $C (L (V), Y) ≅ {Hom}_{A} (V, H (Y))$ for every left $A$ -module $V$ and every $Y \in C$ ; equivalently $L ⊣ H$ (Adjunction by unit, counit, and the triangle identities). The construction is explicit: for the canonical presentation $A^{(J)} \overset{d}{\to} A^{(I)} \overset{q}{\to} V \to 0$ of Canonical free presentations force the comparison to be an isomorphism (free cover of Every module is a quotient of a free module, the first map not required to be monic), replace the free modules by the copowers $P^{(I)}$ and $P^{(J)}$ (The power and the copower of an object by a set), replace every matrix entry $e^{o p}$ of $d$ by $e : P \to P$ , and take the cokernel; the resulting object $L (V)$ is independent of the presentation up to canonical isomorphism, and the universal property defines $L$ on morphisms and proves its identity and composition laws. No choice is used beyond the supplied copowers, cokernels, and canonical presentations.

Facts & Assumptions

Given: A locally small cocomplete abelian category $C$ , a small projective generator $P$ of $C$ , the supplied definable copower and cokernel assignments of the Statement, $E = {End}_{C} (P)$ , $A = E^{o p}$ , and $H = C (P, -) : C \to A -Mod$ with the left action $(e^{o p} \cdot h) = h \circ e$ of Endomorphisms of an object of a preadditive category form a ring.

[F1]

$A$ is a unital ring, $A -Mod$ is locally small and cocomplete, and $H$ is an additive functor that is exact, preserves every set-indexed coproduct, is faithful, and satisfies $H (Z) = 0 \Rightarrow Z = 0$ (Endomorphisms of an object of a preadditive category form a ring, Left modules over a fixed ring and module homomorphisms form the large locally small category $R - M o d$ , For every ring R, the category R-Mod is complete and cocomplete, The Hom functor of a small projective generator is exact, coproduct-preserving, and faithful).

[F2]

For a set $I$ , the copower $P^{(I)}$ of $P$ by $I$ has the universal property that maps $P^{(I)} \to Y$ correspond bijectively and naturally to functions $I \to C (P, Y)$ , i.e. to families $(h_{i})_{i \in I}$ in $H (Y)$ ; in particular no finite-support restriction is imposed on maps out of a copower (The power and the copower of an object by a set, Products and coproducts as limits and colimits of discrete diagrams, including their existence-and-uniqueness equations).

[F3]

By smallness, $H (P^{(I)}) = C (P, P^{(I)}) ≅ ⨁_{i \in I} C (P, P) = ⨁_{i \in I} E$ naturally in $I$ , and the identification $E \to A$ , $e \mapsto e^{o p}$ , is an isomorphism of left $A$ -modules $H (P) ≅_{A} A$ ; hence $H (P^{(I)}) ≅ A^{(I)}$ (The Hom functor of a small projective generator is exact, coproduct-preserving, and faithful, The direct sum of an indexed family of modules).

[F4]

Every left $A$ -module $V$ has a canonical presentation $A^{(J)} \overset{d}{\to} A^{(I)} \overset{q}{\to} V \to 0$ that is exact at $A^{(I)}$ and has $q$ surjective, the first map $d$ not being required to be monic; explicitly $I$ is the underlying set of $V$ , $J$ the underlying set of $\ker q$ , $q (e_{v}) = v$ and $d$ is a canonical surjection onto $\ker q$ followed by the inclusion (Canonical free presentations force the comparison to be an isomorphism, Every module is a quotient of a free module).

[F5]

A map $A^{(I)} \to W$ into a left $A$ -module is uniquely determined by the family $(w_{i})_{i \in I} \in W^{I}$ of its values on the standard basis, and every family arises; a cokernel of $u : X \to Y$ is a map $cok u : Y \to coker u$ with $(cok u) \circ u = 0$ through which every map annihilating $u$ factors uniquely (Universal property of a direct sum of modules, Kernels and cokernels in a category with zero morphisms as equalizers and coequalizers, Abelian category).

[F6]

Representing objects of a functor are unique up to a unique compatible isomorphism (Representing objects are unique up to a unique isomorphism compatible with their universal elements), and $C (a, b) ≅ Nat (C (b, -), C (a, -))$ directly: a transformation $θ$ gives $t = θ_{b} (1_{b}) : a \to b$ and naturality at $h : b \to Y$ gives $θ_{Y} (h) = h \circ t$ ; this also proves compatibility with identities and composition.

[F7]

A natural family of bijections $D (F c, d) ≅ C (c, G d)$ determines a unique adjunction $F ⊣ G$ with unit and counit satisfying the triangle identities (Under local smallness, transposition gives the natural hom-set bijection, and conversely, Adjunction by unit, counit, and the triangle identities).

Proof

technique · constructive

1.1F1F2F3F4F5givenconstruct

(Transposing the presentation.) Write the canonical presentation of [F4] as $A^{(J)} \overset{d}{\to} A^{(I)} \overset{q}{\to} V \to 0$ , and let $d (e_{j}) = \sum_{i} a_{j i} e_{i}$ be its finite-column description with $a_{j i} \in A$ for $j \in J$ and $i \in I$ , only finitely many $a_{j i}$ nonzero for each $j$ by [F5]. Using the identifications $A = E^{o p}$ and $H (P) ≅ A$ of [F3], each entry $a_{j i} = e_{j i}^{o p}$ corresponds to the endomorphism $e_{j i} : P \to P$ , and the finite family $(e_{j i})_{i \in I}$ corresponds under [F3] to an element of $H (P^{(I)})$ , i.e. to a map $δ_{j} : P \to P^{(I)}$ . The copower universal property [F2] turns the family $(δ_{j})_{j \in J}$ into a unique map $τ (d) : P^{(J)} \to P^{(I)}$ whose $j$ -th component is $δ_{j}$ . Define $L (V) : = coker τ (d)$ , the object of $C$ returned by the supplied cokernel assignment; the construction uses only the canonical presentation and supplied copowers and cokernels.

2.1F2F3F4F5givenalgebra

(Identification of the represented functor.) Let $Y \in C$ . By [F2] a map $φ : P^{(I)} \to Y$ corresponds to a family $(h_{i})_{i \in I}$ in $H (Y)$ with $h_{i} = φ \circ ȷ_{i}$ , and by the component computation of step 1.1 $φ \circ τ (d) \circ ȷ_{j} = \sum_{i} h_{i} \circ e_{j i} = \sum_{i} a_{j i} \cdot h_{i}$ for every $j$ , the sum being finite. Hence the cokernel universal property [F5] gives a natural bijection $C (L (V), Y) ≅ {(h_{i}) \in \prod_{i \in I} H (Y) : \sum_{i} a_{j i} \cdot h_{i} = 0 for all j} .$ On the other side, an $A$ -linear map $ψ : V \to H (Y)$ gives the family $h_{i} : = ψ (q (e_{i}))$ , which satisfies $\sum_{i} a_{j i} h_{i} = ψ (q (d (e_{j}))) = 0$ for every $j$ because $q \circ d = 0$ , and conversely [F5] turns any family satisfying these relations into an $A$ -linear $\tilde{ψ} : A^{(I)} \to H (Y)$ that annihilates $im d$ and hence factors uniquely as $ψ \circ q$ for an $A$ -linear $ψ : V \to H (Y)$ by [F4] and the cokernel property in $A -Mod$ ; the two constructions are inverse. Composing the two identifications gives a bijection $Φ_{V} : C (L (V), Y) ≅ {Hom}_{A} (V, H (Y))$ that is natural in $Y$ , because postcomposition with a map $g : Y \to Y^{'}$ acts componentwise on both families.

3.1F6step 2.1given

(Independence of the presentation.) The bijection of step 2.1 exhibits $L (V)$ as a representing object of the functor $Y \mapsto {Hom}_{A} (V, H (Y))$ , a functor independent of the chosen presentation of $V$ ; by [F6] any other representing object is canonically isomorphic to $L (V)$ through a unique isomorphism compatible with the universal elements. Hence $L (V)$ is independent of the presentation up to canonical isomorphism.

4.1F6step 2.1step 3.1givenconstruct

(Functoriality.) For a map $u : V \to V^{'}$ of left $A$ -modules, precomposition with $u$ gives a natural transformation $G_{V^{'}} \Rightarrow G_{V}$ between the functors $G_{W} = {Hom}_{A} (W, H (-))$ . Transporting it through the representations $Φ_{W}$ of step 2.1 gives a natural transformation $C (L (V^{'}), -) \Rightarrow C (L (V), -)$ , which by the Yoneda bijection [F6] corresponds to a unique map $L (u) : L (V) \to L (V^{'})$ with $Φ_{V}^{- 1} (ψ \circ u) = Φ_{V^{'}}^{- 1} (ψ) \circ L (u)$ for all $ψ$ . The Yoneda correspondence is compatible with composition and identities, so $L (1_{V}) = 1_{L (V)}$ and $L (u^{'} \circ u) = L (u^{'}) \circ L (u)$ ; together with the object assignment $V \mapsto L (V)$ this is a functor $L : A -Mod \to C$ (Covariant functor, identity functor, composite functor, and contravariant functor, Category, object, morphism, domain, codomain, identity, composition, and hom-collection).

5.1F7step 2.1step 4.1given

(The adjunction.) The bijections $Φ_{V} : C (L (V), Y) ≅ {Hom}_{A} (V, H (Y))$ of step 2.1 are natural in $Y$ and, by the defining property of $L (u)$ in step 4.1, natural in $V$ as well. Since both categories are locally small, [F7] turns this natural family into a unique adjunction $L ⊣ H$ with unit $η : 1_{A - M o d} \Rightarrow H L$ and counit $ε : L H \Rightarrow 1_{C}$ satisfying the triangle identities.

6.1step 1.1step 2.1step 3.1step 4.1step 5.1discharge-construct: the cokernel $L(V)$ and the adjunction $L\dashv H$∎

Steps 1.1 and 2.1 construct $L (V)$ from a canonical presentation and prove the natural bijection $C (L (V), Y) ≅ {Hom}_{A} (V, H (Y))$ ; step 3.1 proves the construction is independent of the presentation, step 4.1 constructs $L$ on maps with its identity and composition laws, and step 5.1 converts the natural bijections into the adjunction $L ⊣ H$ . The only data used are the canonical presentation determined by $V$ , the supplied copowers $P^{(I)}$ , $P^{(J)}$ and the supplied cokernel, so nothing is selected from a nonempty family and no choice principle is used.

Depends on

Used by

Dependency tree · two levels

78 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

W. Crawley-Boevey, Noncommutative Algebra, §3.12, proof of 'A is equivalent to R-Mod iff A is cocomplete with a finitely generated projective generator P, R = End(P)^op', printed pp.68-69 (standard reference, not scraped)
P. Etingen, S. Gelaki, D. Nikshych, V. Ostrik, Tensor Categories, printed p.10 (Hom_C(P,-) and the algebra End(P)^op) (standard reference, not scraped)