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.
Exact functor between abelian categories
Definition
Let and be abelian categories. A functor is exact when it is additive (Additive functor) and both left exact and right exact (Left exact and right exact functors).
Thus exactness is a two-sided preservation condition: preserves the finite limits and finite colimits that exist in its source, and it preserves the additive structure carried by the hom-sets.
Depends on
Used by
- Exact finite tensor functors have projective right-module kernels Corollary
- Exact module tensor functors correspond to right-flat bimodules Corollary
- An exact functor need not be faithful Counterexample
- The degree-zero projection is exact and cocontinuous but not a graded tensor functor Counterexample
- Localization of modules gives an exact functor between module categories Example
- Filtered colimits and sheaf cohomology on Noetherian spaces Lemma
- Filtered colimits of abelian groups are exact Lemma
- The Hom functor of a small projective generator is exact, coproduct-preserving, and faithful Lemma
- An exact base functor has the trivial universal delta functor Proposition
- An exact functor carries mapping-cone sequences to mapping-cone sequences Proposition
- An exact functor carries the long exact homology sequence to the corresponding long exact sequence Proposition
- An exact functor has vanishing positive derived functors Proposition
- Exact functors compatible with Hom transport Ext under stated adjunction hypotheses Proposition
- AB5 is equivalent to exactness of filtered colimits Theorem
- An additive functor is exact exactly when it preserves kernels and cokernels Theorem
- An equivalence between abelian categories is exact Theorem
- An exact functor commutes with homology Theorem
- An exact functor transports every diagram lemma Theorem
- An object is projective exactly when Hom out of it is exact Theorem
- Exact adjoints induce adjoint operators on Grothendieck groups Theorem
- Universal properties and functoriality of G0 and split K0 Theorem
Dependency tree · two levels
6 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
- The Stacks Project, Section 12.7 (standard reference, not scraped)
- Gautam Tamme, Algebra II Lecture 10, §10.4 (standard reference, not scraped)