Theorems · Inductive type · category theory
CategoryTheory.Preadditive
(C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max u v)A category is called preadditive if P ⟶ Q is an abelian group such that composition is
linear in both variables.
- Defined in
- Mathlib.CategoryTheory.Preadditive.Basic
- Cited by
- 3,309 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement · cited by 32,673
Cited by4,414
Results whose statement or proof uses this declaration.
- CategoryTheory.Functor.Additivestatement · cited by 1,179
- CategoryTheory.Pretriangulatedstatement · cited by 669
- CochainComplex.HomComplex.Cochainstatement and proof · cited by 341
- CategoryTheory.Triangulated.TStructurestatement · cited by 318
- CategoryTheory.Pretriangulated.distinguishedTrianglesstatement and proof · cited by 316
- HomologicalComplex.HasHomotopyCofiberstatement · cited by 225
- CochainComplex.HomComplex.Cochain.vstatement and proof · cited by 213
- CochainComplex.mappingConestatement and proof · cited by 181
- AlgebraicTopology.AlternatingFaceMapComplex.objstatement and proof · cited by 146
- HomotopyCategorystatement and proof · cited by 132
- CategoryTheory.Linearstatement · cited by 131
- CochainComplex.HomComplex.Cocyclestatement and proof · cited by 130
Showing the 200 most cited of 4,414.