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 ⟶ R
is mono if and only ifg ≫ f = 0 → g = 0
for all composableg
. - 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
.
References #
Tags #
additive, preadditive, Hom group, Ab-category, Ab-enriched
A category is called preadditive if P ⟶ Q
is an abelian group such that composition is
linear in both variables.
- homGroup : (P Q : C) → AddCommGroup (P ⟶ Q)
A category is called preadditive if
P ⟶ Q
is an abelian group such that composition is linear in both variables. - add_comp : ∀ (P Q R : C) (f f' : P ⟶ Q) (g : Q ⟶ R), CategoryTheory.CategoryStruct.comp (f + f') g = CategoryTheory.CategoryStruct.comp f g + CategoryTheory.CategoryStruct.comp f' g
A category is called preadditive if
P ⟶ Q
is an abelian group such that composition is linear in both variables. - comp_add : ∀ (P Q R : C) (f : P ⟶ Q) (g g' : Q ⟶ R), CategoryTheory.CategoryStruct.comp f (g + g') = CategoryTheory.CategoryStruct.comp f g + CategoryTheory.CategoryStruct.comp f g'
A category is called preadditive if
P ⟶ Q
is an abelian group such that composition is linear in both variables.
Instances
Equations
- CategoryTheory.Preadditive.inducedCategory F = { homGroup := fun (P Q : CategoryTheory.InducedCategory C F) => CategoryTheory.Preadditive.homGroup (F P) (F Q), add_comp := ⋯, comp_add := ⋯ }
Equations
- CategoryTheory.Preadditive.fullSubcategory Z = { homGroup := fun (P Q : CategoryTheory.FullSubcategory Z) => CategoryTheory.Preadditive.homGroup P.obj Q.obj, add_comp := ⋯, comp_add := ⋯ }
Equations
- CategoryTheory.Preadditive.instAddCommGroupEnd X = id inferInstance
Composition by a fixed left argument as a group homomorphism
Equations
- CategoryTheory.Preadditive.leftComp R f = AddMonoidHom.mk' (fun (g : Q ⟶ R) => CategoryTheory.CategoryStruct.comp f g) ⋯
Instances For
Composition by a fixed right argument as a group homomorphism
Equations
- CategoryTheory.Preadditive.rightComp P g = AddMonoidHom.mk' (fun (f : P ⟶ Q) => CategoryTheory.CategoryStruct.comp f g) ⋯
Instances For
Composition as a bilinear group homomorphism
Equations
- CategoryTheory.Preadditive.compHom = AddMonoidHom.mk' (fun (f : P ⟶ Q) => CategoryTheory.Preadditive.leftComp R f) ⋯
Instances For
Equations
- CategoryTheory.Preadditive.preadditiveHasZeroMorphisms = CategoryTheory.Limits.HasZeroMorphisms.mk ⋯ ⋯
Porting note: adding this before the ring instance allowed moduleEndRight to find the correct Monoid structure on End. Moved both down after preadditiveHasZeroMorphisms to make use of them
Equations
- CategoryTheory.Preadditive.instSemiringEnd = Semiring.mk ⋯ ⋯ ⋯ ⋯ Monoid.npow ⋯ ⋯
Porting note: It looks like Ring's parent classes changed in Lean 4 so the previous instance needed modification. Was following my nose here.
Map a kernel cone on the difference of two morphisms to the equalizer fork.
Equations
Instances For
Map any equalizer fork to a cone on the difference of the two morphisms.
Equations
Instances For
A kernel of f - g
is an equalizer of f
and g
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
An equalizer of f
and g
is a kernel of f - g
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A preadditive category has an equalizer for f
and g
if it has a kernel for f - g
.
A preadditive category has a kernel for f - g
if it has an equalizer for f
and g
.
Map a cokernel cocone on the difference of two morphisms to the coequalizer cofork.
Equations
Instances For
Map any coequalizer cofork to a cocone on the difference of the two morphisms.
Equations
Instances For
A cokernel of f - g
is a coequalizer of f
and g
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A coequalizer of f
and g
is a cokernel of f - g
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A preadditive category has a coequalizer for f
and g
if it has a cokernel for f - g
.
A preadditive category has a cokernel for f - g
if it has a coequalizer for f
and g
.
If a preadditive category has all kernels, then it also has all equalizers.
If a preadditive category has all cokernels, then it also has all coequalizers.