Preadditive categories #
A preadditive category is a category in which
X ⟶ Y is an abelian group in such a way that
composition of morphisms is linear in both variables.
This file contains a definition of preadditive category that directly encodes the definition given above. The definition could also be phrased as follows: A preadditive category is a category enriched over the category of Abelian groups. Once the general framework to state this in Lean is available, the contents of this file should become obsolete.
Main results #
- Definition of preadditive categories and basic properties
- In a preadditive category,
f : Q ⟶ Ris mono if and only if
g ≫ f = 0 → g = 0for all composable
- A preadditive category with kernels has equalizers.
Implementation notes #
The simp normal form for negation and composition is to push negations as far as possible to
the outside. For example,
f ≫ (-g) and
(-f) ≫ g both become
-(f ≫ g), and
(-f) ≫ (-g)
is simplified to
f ≫ g.
additive, preadditive, Hom group, Ab-category, Ab-enriched
- hom_group : (Π (P Q : C), add_comm_group (P ⟶ Q)) . "apply_instance"
- add_comp' : (∀ (P Q R : C) (f f' : P ⟶ Q) (g : Q ⟶ R), (f + f') ≫ g = f ≫ g + f' ≫ g) . "obviously"
- comp_add' : (∀ (P Q R : C) (f : P ⟶ Q) (g g' : Q ⟶ R), f ≫ (g + g') = f ≫ g + f ≫ g') . "obviously"
A category is called preadditive if
P ⟶ Q is an abelian group such that composition is
linear in both variables.
Composition by a fixed left argument as a group homomorphism
Composition by a fixed right argument as a group homomorphism
A kernel of
f - g is an equalizer of
If a preadditive category has all kernels, then it also has all equalizers.
A cokernel of
f - g is a coequalizer of
If a preadditive category has all cokernels, then it also has all coequalizers.