Preadditive categories #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
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.
Instances of this typeclass
Instances of other typeclasses for category_theory.preadditive
- category_theory.preadditive.has_sizeof_inst
- category_theory.subsingleton_preadditive_of_has_binary_biproducts
@[simp]
theorem
category_theory.preadditive.add_comp
{C : Type u}
[category_theory.category C]
[self : category_theory.preadditive C]
(P Q R : C)
(f f' : P ⟶ Q)
(g : Q ⟶ R) :
@[simp]
theorem
category_theory.preadditive.comp_add
{C : Type u}
[category_theory.category C]
[self : category_theory.preadditive C]
(P Q R : C)
(f : P ⟶ Q)
(g g' : Q ⟶ R) :
@[protected, instance]
def
category_theory.preadditive.induced_category
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u'}
(F : D → C) :
Equations
- category_theory.preadditive.induced_category F = {hom_group := λ (P Q : category_theory.induced_category C F), category_theory.preadditive.hom_group (F P) (F Q), add_comp' := _, comp_add' := _}
@[protected, instance]
def
category_theory.preadditive.full_subcategory
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
(Z : C → Prop) :
Equations
- category_theory.preadditive.full_subcategory Z = {hom_group := λ (P Q : category_theory.full_subcategory Z), category_theory.preadditive.hom_group P.obj Q.obj, add_comp' := _, comp_add' := _}
@[protected, instance]
def
category_theory.preadditive.category_theory.End.add_comm_group
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
(X : C) :
@[protected, instance]
def
category_theory.preadditive.category_theory.End.ring
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
(X : C) :
Equations
- category_theory.preadditive.category_theory.End.ring X = {add := add_comm_group.add infer_instance, add_assoc := _, zero := add_comm_group.zero infer_instance, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul infer_instance, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg infer_instance, sub := add_comm_group.sub infer_instance, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul infer_instance, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := add_comm_group_with_one.int_cast._default (add_comm_group_with_one.nat_cast._default monoid.one add_comm_group.add _ add_comm_group.zero _ _ add_comm_group.nsmul _ _) add_comm_group.add _ add_comm_group.zero _ _ add_comm_group.nsmul _ _ monoid.one _ _ add_comm_group.neg add_comm_group.sub _ add_comm_group.zsmul _ _ _ _, nat_cast := add_comm_group_with_one.nat_cast._default monoid.one add_comm_group.add _ add_comm_group.zero _ _ add_comm_group.nsmul _ _, one := monoid.one infer_instance, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := monoid.mul infer_instance, mul_assoc := _, one_mul := _, mul_one := _, npow := monoid.npow infer_instance, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}
def
category_theory.preadditive.left_comp
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{P Q : C}
(R : C)
(f : P ⟶ Q) :
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}
(g : Q ⟶ R) :
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) _
def
category_theory.preadditive.comp_hom
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{P Q R : C} :
Composition as a bilinear group homomorphism
Equations
- category_theory.preadditive.comp_hom = add_monoid_hom.mk' (λ (f : P ⟶ Q), category_theory.preadditive.left_comp R f) category_theory.preadditive.comp_hom._proof_1
@[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.comp_sub
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{P Q R : C}
(f : P ⟶ Q)
(g 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') :
@[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) :
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
{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.nsmul_comp
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{P Q R : C}
(f : P ⟶ Q)
(g : Q ⟶ R)
(n : ℕ) :
theorem
category_theory.preadditive.comp_nsmul
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{P Q R : C}
(f : P ⟶ Q)
(g : Q ⟶ R)
(n : ℕ) :
theorem
category_theory.preadditive.zsmul_comp
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{P Q R : C}
(f : P ⟶ Q)
(g : Q ⟶ R)
(n : ℤ) :
theorem
category_theory.preadditive.comp_zsmul
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{P Q R : C}
(f : P ⟶ Q)
(g : Q ⟶ R)
(n : ℤ) :
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
{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) :
@[protected, instance]
def
category_theory.preadditive.has_neg.neg.category_theory.epi
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{P Q : C}
{f : P ⟶ Q}
[category_theory.epi f] :
@[protected, instance]
def
category_theory.preadditive.has_neg.neg.category_theory.mono
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{P Q : C}
{f : P ⟶ Q}
[category_theory.mono f] :
@[protected, 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_zero_class.to_has_zero (X ⟶ Y)), comp_zero' := _, zero_comp' := _}
@[protected, instance]
def
category_theory.preadditive.module_End_right
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C} :
module (category_theory.End Y) (X ⟶ Y)
Equations
- category_theory.preadditive.module_End_right = {to_distrib_mul_action := {to_mul_action := category_theory.End.mul_action_right Y, smul_zero := _, smul_add := _}, add_smul := _, zero_smul := _}
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)
(h : ∀ {P : C} (g : P ⟶ Q), g ≫ f = 0 → g = 0) :
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)]
(w : category_theory.limits.kernel.ι 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)
(h : ∀ {R : C} (g : Q ⟶ R), f ≫ g = 0 → g = 0) :
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)]
(w : category_theory.limits.cokernel.π f = 0) :
@[simp]
theorem
category_theory.preadditive.is_iso.comp_left_eq_zero
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{P Q R : C}
(f : P ⟶ Q)
(g : Q ⟶ R)
[category_theory.is_iso f] :
@[simp]
theorem
category_theory.preadditive.is_iso.comp_right_eq_zero
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{P Q R : C}
(f : P ⟶ Q)
(g : Q ⟶ R)
[category_theory.is_iso g] :
theorem
category_theory.preadditive.mono_of_kernel_iso_zero
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_zero_object C]
{X Y : C}
{f : X ⟶ Y}
[category_theory.limits.has_limit (category_theory.limits.parallel_pair f 0)]
(w : category_theory.limits.kernel f ≅ 0) :
theorem
category_theory.preadditive.epi_of_cokernel_iso_zero
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_zero_object C]
{X Y : C}
{f : X ⟶ Y}
[category_theory.limits.has_colimit (category_theory.limits.parallel_pair f 0)]
(w : category_theory.limits.cokernel f ≅ 0) :
def
category_theory.preadditive.fork_of_kernel_fork
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f g : X ⟶ Y}
(c : category_theory.limits.kernel_fork (f - g)) :
Map a kernel cone on the difference of two morphisms to the equalizer fork.
@[simp]
theorem
category_theory.preadditive.fork_of_kernel_fork_X
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f g : X ⟶ Y}
(c : category_theory.limits.kernel_fork (f - g)) :
@[simp]
theorem
category_theory.preadditive.fork_of_kernel_fork_ι
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f g : X ⟶ Y}
(c : category_theory.limits.kernel_fork (f - g)) :
def
category_theory.preadditive.kernel_fork_of_fork
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f g : X ⟶ Y}
(c : category_theory.limits.fork f g) :
Map any equalizer fork to a cone on the difference of the two morphisms.
@[simp]
theorem
category_theory.preadditive.kernel_fork_of_fork_ι
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f g : X ⟶ Y}
(c : category_theory.limits.fork f g) :
@[simp]
theorem
category_theory.preadditive.kernel_fork_of_fork_of_ι
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f g : X ⟶ Y}
{P : C}
(ι : P ⟶ X)
(w : ι ≫ f = ι ≫ g) :
def
category_theory.preadditive.is_limit_fork_of_kernel_fork
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f g : X ⟶ Y}
{c : category_theory.limits.kernel_fork (f - g)}
(i : category_theory.limits.is_limit c) :
A kernel of f - g is an equalizer of f and g.
@[simp]
theorem
category_theory.preadditive.is_limit_fork_of_kernel_fork_lift
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f g : X ⟶ Y}
{c : category_theory.limits.kernel_fork (f - g)}
(i : category_theory.limits.is_limit c)
(s : category_theory.limits.fork f g) :
def
category_theory.preadditive.is_limit_kernel_fork_of_fork
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f g : X ⟶ Y}
{c : category_theory.limits.fork f g}
(i : category_theory.limits.is_limit c) :
An equalizer of f and g is a kernel of f - g.
theorem
category_theory.preadditive.has_equalizer_of_has_kernel
{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 preadditive category has an equalizer for f and g if it has a kernel for f - g.
theorem
category_theory.preadditive.has_kernel_of_has_equalizer
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
(f g : X ⟶ Y)
[category_theory.limits.has_equalizer f g] :
A preadditive category has a kernel for f - g if it has an equalizer for f and g.
def
category_theory.preadditive.cofork_of_cokernel_cofork
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f g : X ⟶ Y}
(c : category_theory.limits.cokernel_cofork (f - g)) :
Map a cokernel cocone on the difference of two morphisms to the coequalizer cofork.
@[simp]
theorem
category_theory.preadditive.cofork_of_cokernel_cofork_X
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f g : X ⟶ Y}
(c : category_theory.limits.cokernel_cofork (f - g)) :
@[simp]
theorem
category_theory.preadditive.cofork_of_cokernel_cofork_π
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f g : X ⟶ Y}
(c : category_theory.limits.cokernel_cofork (f - g)) :
def
category_theory.preadditive.cokernel_cofork_of_cofork
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f g : X ⟶ Y}
(c : category_theory.limits.cofork f g) :
Map any coequalizer cofork to a cocone on the difference of the two morphisms.
@[simp]
theorem
category_theory.preadditive.cokernel_cofork_of_cofork_π
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f g : X ⟶ Y}
(c : category_theory.limits.cofork f g) :
@[simp]
theorem
category_theory.preadditive.cokernel_cofork_of_cofork_of_π
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f g : X ⟶ Y}
{P : C}
(π : Y ⟶ P)
(w : f ≫ π = g ≫ π) :
def
category_theory.preadditive.is_colimit_cofork_of_cokernel_cofork
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f g : X ⟶ Y}
{c : category_theory.limits.cokernel_cofork (f - g)}
(i : category_theory.limits.is_colimit c) :
A cokernel of f - g is a coequalizer of f and g.
@[simp]
theorem
category_theory.preadditive.is_colimit_cofork_of_cokernel_cofork_desc
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f g : X ⟶ Y}
{c : category_theory.limits.cokernel_cofork (f - g)}
(i : category_theory.limits.is_colimit c)
(s : category_theory.limits.cofork f g) :
def
category_theory.preadditive.is_colimit_cokernel_cofork_of_cofork
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f g : X ⟶ Y}
{c : category_theory.limits.cofork f g}
(i : category_theory.limits.is_colimit c) :
A coequalizer of f and g is a cokernel of f - g.
Equations
theorem
category_theory.preadditive.has_coequalizer_of_has_cokernel
{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 preadditive category has a coequalizer for f and g if it has a cokernel for f - g.
theorem
category_theory.preadditive.has_cokernel_of_has_coequalizer
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
(f g : X ⟶ Y)
[category_theory.limits.has_coequalizer f g] :
A preadditive category has a cokernel for f - g if it has a coequalizer for f and g.
theorem
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.
theorem
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.