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 ifg ≫ f = 0 → g = 0for 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
- [F. Borceux, Handbook of Categorical Algebra 2][borceux-vol2]
Tags
additive, preadditive, Hom group, Ab-category, Ab-enriched
@[class]
- 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.
def
category_theory.preadditive.left_comp
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{P Q : C}
(R : C) :
Composition by a fixed left argument as a group homomorphism
Equations
- category_theory.preadditive.left_comp R f = add_monoid_hom.mk' (λ (g : Q ⟶ R), f ≫ g) _
def
category_theory.preadditive.right_comp
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
(P : C)
{Q R : C} :
Composition by a fixed right argument as a group homomorphism
Equations
- category_theory.preadditive.right_comp P g = add_monoid_hom.mk' (λ (f : P ⟶ Q), f ≫ g) _
@[simp]
theorem
category_theory.preadditive.sub_comp
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{P Q R : C}
(f f' : P ⟶ Q)
(g : Q ⟶ R) :
@[simp]
theorem
category_theory.preadditive.sub_comp_assoc
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{P Q R : C}
(f f' : P ⟶ Q)
(g : Q ⟶ R)
{X' : C}
(f'_1 : R ⟶ X') :
@[simp]
theorem
category_theory.preadditive.comp_sub
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{P Q R : C}
(f : P ⟶ Q)
(g g' : Q ⟶ R) :
theorem
category_theory.preadditive.comp_sub_assoc
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{P Q R : C}
(f : P ⟶ Q)
(g g' : Q ⟶ R)
{X' : C}
(f' : R ⟶ X') :
@[simp]
theorem
category_theory.preadditive.neg_comp
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{P Q R : C}
(f : P ⟶ Q)
(g : Q ⟶ R) :
@[simp]
theorem
category_theory.preadditive.neg_comp_assoc
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{P Q R : C}
(f : P ⟶ Q)
(g : Q ⟶ R)
{X' : C}
(f' : R ⟶ X') :
theorem
category_theory.preadditive.comp_neg_assoc
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{P Q R : C}
(f : P ⟶ Q)
(g : Q ⟶ R)
{X' : C}
(f' : R ⟶ X') :
@[simp]
theorem
category_theory.preadditive.comp_neg
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{P Q R : C}
(f : P ⟶ Q)
(g : Q ⟶ R) :
theorem
category_theory.preadditive.neg_comp_neg_assoc
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{P Q R : C}
(f : P ⟶ Q)
(g : Q ⟶ R)
{X' : C}
(f' : R ⟶ X') :
theorem
category_theory.preadditive.neg_comp_neg
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{P Q R : C}
(f : P ⟶ Q)
(g : Q ⟶ R) :
theorem
category_theory.preadditive.comp_sum_assoc
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{P Q R : C}
{J : Type u_1}
{s : finset J}
(f : P ⟶ Q)
(g : J → (Q ⟶ R))
{X' : C}
(f' : R ⟶ X') :
theorem
category_theory.preadditive.comp_sum
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{P Q R : C}
{J : Type u_1}
{s : finset J}
(f : P ⟶ Q)
(g : J → (Q ⟶ R)) :
theorem
category_theory.preadditive.sum_comp_assoc
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{P Q R : C}
{J : Type u_1}
{s : finset J}
(f : J → (P ⟶ Q))
(g : Q ⟶ R)
{X' : C}
(f' : R ⟶ X') :
theorem
category_theory.preadditive.sum_comp
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{P Q R : C}
{J : Type u_1}
{s : finset J}
(f : J → (P ⟶ Q))
(g : Q ⟶ R) :
@[instance]
def
category_theory.preadditive.category_theory.epi
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{P Q : C}
{f : P ⟶ Q}
[category_theory.epi f] :
Equations
@[instance]
def
category_theory.preadditive.category_theory.mono
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{P Q : C}
{f : P ⟶ Q}
[category_theory.mono f] :
Equations
@[instance]
def
category_theory.preadditive.preadditive_has_zero_morphisms
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C] :
Equations
- category_theory.preadditive.preadditive_has_zero_morphisms = {has_zero := infer_instance (λ (X Y : C), add_monoid.to_has_zero (X ⟶ Y)), comp_zero' := _, zero_comp' := _}
theorem
category_theory.preadditive.mono_of_cancel_zero
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{Q R : C}
(f : Q ⟶ R) :
(∀ {P : C} (g : P ⟶ Q), g ≫ f = 0 → g = 0) → category_theory.mono f
theorem
category_theory.preadditive.mono_iff_cancel_zero
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{Q R : C}
(f : Q ⟶ R) :
theorem
category_theory.preadditive.mono_of_kernel_zero
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f : X ⟶ Y}
[category_theory.limits.has_limit (category_theory.limits.parallel_pair f 0)] :
theorem
category_theory.preadditive.epi_of_cancel_zero
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{P Q : C}
(f : P ⟶ Q) :
(∀ {R : C} (g : Q ⟶ R), f ≫ g = 0 → g = 0) → category_theory.epi f
theorem
category_theory.preadditive.epi_iff_cancel_zero
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{P Q : C}
(f : P ⟶ Q) :
theorem
category_theory.preadditive.epi_of_cokernel_zero
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_colimit (category_theory.limits.parallel_pair f 0)] :
def
category_theory.preadditive.has_limit_parallel_pair
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
(f g : X ⟶ Y)
[category_theory.limits.has_kernel (f - g)] :
A kernel of f - g is an equalizer of f and g.
Equations
- category_theory.preadditive.has_limit_parallel_pair f g = {cone := category_theory.limits.fork.of_ι (category_theory.limits.kernel.ι (f - g)) _, is_limit := category_theory.limits.fork.is_limit.mk (category_theory.limits.fork.of_ι (category_theory.limits.kernel.ι (f - g)) _) (λ (s : category_theory.limits.fork f g), category_theory.limits.kernel.lift (f - g) s.ι _) _ _}
def
category_theory.preadditive.has_equalizers_of_has_kernels
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_kernels C] :
If a preadditive category has all kernels, then it also has all equalizers.
def
category_theory.preadditive.has_colimit_parallel_pair
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
(f g : X ⟶ Y)
[category_theory.limits.has_cokernel (f - g)] :
A cokernel of f - g is a coequalizer of f and g.
Equations
- category_theory.preadditive.has_colimit_parallel_pair f g = {cocone := category_theory.limits.cofork.of_π (category_theory.limits.cokernel.π (f - g)) _, is_colimit := category_theory.limits.cofork.is_colimit.mk (category_theory.limits.cofork.of_π (category_theory.limits.cokernel.π (f - g)) _) (λ (s : category_theory.limits.cofork f g), category_theory.limits.cokernel.desc (f - g) s.π _) _ _}
def
category_theory.preadditive.has_coequalizers_of_has_cokernels
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_cokernels C] :
If a preadditive category has all cokernels, then it also has all coequalizers.