Every non_preadditive_abelian category is preadditive
In mathlib, we define an abelian category as a preadditive category with a zero object, kernels and cokernels, products and coproducts and in which every monomorphism and epimorphis is normal.
While virtually every interesting abelian category has a natural preadditive structure (which is why it is included in the definition), preadditivity is not actually needed: Every category that has all of the other properties appearing in the definition of an abelian category admits a preadditive structure. This is the construction we carry out in this file.
The proof proceeds in roughly five steps:
- Prove some results (for example that all equalizers exist) that would be trivial if we already had the preadditive structure but are a bit of work without it.
- Develop images and coimages to show that every monomorphism is the kernel of its cokernel.
The results of the first two steps are also useful for the "normal" development of abelian categories, and will be used there.
- For every object
A, define a "subtraction" morphismσ : A ⨯ A ⟶ Aand use it to define subtraction on morphisms asf - g := prod.lift f g ≫ σ. - Prove a small number of identities about this subtraction from the definition of
σ. - From these identities, prove a large number of other identities that imply that defining
f + g := f - (0 - g)indeed gives an abelian group structure on morphisms such that composition is bilinear.
The construction is non-trivial and it is quite remarkable that this abelian group structure can be constructed purely from the existence of a few limits and colimits. What's even more impressive is that all additive structures on a category are in some sense isomorphic, so for abelian categories with a natural preadditive structure, this construction manages to "almost" reconstruct this natural structure. However, we have not formalized this isomorphism.
References
- [F. Borceux, Handbook of Categorical Algebra 2][borceux-vol2]
@[class]
structure
category_theory.non_preadditive_abelian
(C : Type u)
[category_theory.category C] :
Type (max u (v+1))
- has_zero_object : category_theory.limits.has_zero_object C
- has_zero_morphisms : category_theory.limits.has_zero_morphisms C
- has_kernels : category_theory.limits.has_kernels C
- has_cokernels : category_theory.limits.has_cokernels C
- has_finite_products : category_theory.limits.has_finite_products C
- has_finite_coproducts : category_theory.limits.has_finite_coproducts C
- normal_mono : Π {X Y : C} (f : X ⟶ Y) [_inst_2 : category_theory.mono f], category_theory.normal_mono f
- normal_epi : Π {X Y : C} (f : X ⟶ Y) [_inst_2 : category_theory.epi f], category_theory.normal_epi f
We call a category non_preadditive_abelian if it has a zero object, kernels, cokernels, binary
products and coproducts, and every monomorphism and every epimorphism is normal.
def
category_theory.non_preadditive_abelian.strong_epi_of_epi
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{P Q : C}
(f : P ⟶ Q)
[category_theory.epi f] :
In a non_preadditive_abelian category, every epimorphism is strong.
def
category_theory.non_preadditive_abelian.is_iso_of_mono_of_epi
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.mono f]
[category_theory.epi f] :
In a non_preadditive_abelian category, a monomorphism which is also an epimorphism is an
isomorphism.
def
category_theory.non_preadditive_abelian.pullback_of_mono
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y Z : C}
(a : X ⟶ Z)
(b : Y ⟶ Z)
[category_theory.mono a]
[category_theory.mono b] :
The pullback of two monomorphisms exists.
Equations
- category_theory.non_preadditive_abelian.pullback_of_mono a b = category_theory.non_preadditive_abelian.pullback_of_mono._match_4 a b (category_theory.non_preadditive_abelian.normal_mono a)
- category_theory.non_preadditive_abelian.pullback_of_mono._match_4 a b {Z := P, g := f, w := haf, is_limit := i} = category_theory.non_preadditive_abelian.pullback_of_mono._match_3 a b P f haf i (category_theory.non_preadditive_abelian.normal_mono b)
- category_theory.non_preadditive_abelian.pullback_of_mono._match_3 a b P f haf i {Z := Q, g := g, w := hbg, is_limit := i'} = category_theory.non_preadditive_abelian.pullback_of_mono._match_2 a b P f haf Q g hbg i' (category_theory.limits.kernel_fork.is_limit.lift' i (category_theory.limits.kernel.ι (category_theory.limits.prod.lift f g)) _)
- category_theory.non_preadditive_abelian.pullback_of_mono._match_2 a b P f haf Q g hbg i' ⟨a', ha'⟩ = category_theory.non_preadditive_abelian.pullback_of_mono._match_1 a b P f haf Q g hbg a' ha' (category_theory.limits.kernel_fork.is_limit.lift' i' (category_theory.limits.kernel.ι (category_theory.limits.prod.lift f g)) _)
- category_theory.non_preadditive_abelian.pullback_of_mono._match_1 a b P f haf Q g hbg a' ha' ⟨b', hb'⟩ = {cone := category_theory.limits.pullback_cone.mk a' b' _, is_limit := category_theory.limits.pullback_cone.is_limit.mk a' b' _ (λ (s : category_theory.limits.pullback_cone a b), category_theory.limits.kernel.lift (category_theory.limits.prod.lift f g) (s.snd ≫ b) _) _ _ _}
def
category_theory.non_preadditive_abelian.pushout_of_epi
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y Z : C}
(a : X ⟶ Y)
(b : X ⟶ Z)
[category_theory.epi a]
[category_theory.epi b] :
The pushout of two epimorphisms exists.
Equations
- category_theory.non_preadditive_abelian.pushout_of_epi a b = category_theory.non_preadditive_abelian.pushout_of_epi._match_4 a b (category_theory.non_preadditive_abelian.normal_epi a)
- category_theory.non_preadditive_abelian.pushout_of_epi._match_4 a b {W := P, g := f, w := hfa, is_colimit := i} = category_theory.non_preadditive_abelian.pushout_of_epi._match_3 a b P f hfa i (category_theory.non_preadditive_abelian.normal_epi b)
- category_theory.non_preadditive_abelian.pushout_of_epi._match_3 a b P f hfa i {W := Q, g := g, w := hgb, is_colimit := i'} = category_theory.non_preadditive_abelian.pushout_of_epi._match_2 a b P f hfa Q g hgb i' (category_theory.limits.cokernel_cofork.is_colimit.desc' i (category_theory.limits.cokernel.π (category_theory.limits.coprod.desc f g)) _)
- category_theory.non_preadditive_abelian.pushout_of_epi._match_2 a b P f hfa Q g hgb i' ⟨a', ha'⟩ = category_theory.non_preadditive_abelian.pushout_of_epi._match_1 a b P f hfa Q g hgb a' ha' (category_theory.limits.cokernel_cofork.is_colimit.desc' i' (category_theory.limits.cokernel.π (category_theory.limits.coprod.desc f g)) _)
- category_theory.non_preadditive_abelian.pushout_of_epi._match_1 a b P f hfa Q g hgb a' ha' ⟨b', hb'⟩ = {cocone := category_theory.limits.pushout_cocone.mk a' b' _, is_colimit := category_theory.limits.pushout_cocone.is_colimit.mk a' b' _ (λ (s : category_theory.limits.pushout_cocone a b), category_theory.limits.cokernel.desc (category_theory.limits.coprod.desc f g) (b ≫ s.inr) _) _ _ _}
def
category_theory.non_preadditive_abelian.has_limit_parallel_pair
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(f g : X ⟶ Y) :
The equalizer of f and g exists.
Equations
- category_theory.non_preadditive_abelian.has_limit_parallel_pair f g = have h1f : category_theory.mono (category_theory.limits.prod.lift (𝟙 X) f), from _, have h1g : category_theory.mono (category_theory.limits.prod.lift (𝟙 X) g), from _, have huv : category_theory.limits.pullback.fst = category_theory.limits.pullback.snd, from _, have hvu : category_theory.limits.pullback.fst ≫ f = category_theory.limits.pullback.snd ≫ g, from _, have huu : category_theory.limits.pullback.fst ≫ f = category_theory.limits.pullback.fst ≫ g, from _, {cone := category_theory.limits.fork.of_ι category_theory.limits.pullback.fst huu, is_limit := category_theory.limits.fork.is_limit.mk (category_theory.limits.fork.of_ι category_theory.limits.pullback.fst huu) (λ (s : category_theory.limits.fork f g), category_theory.limits.pullback.lift s.ι s.ι _) _ _}
def
category_theory.non_preadditive_abelian.has_colimit_parallel_pair
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(f g : X ⟶ Y) :
The coequalizer of f and g exists.
Equations
- category_theory.non_preadditive_abelian.has_colimit_parallel_pair f g = have h1f : category_theory.epi (category_theory.limits.coprod.desc (𝟙 Y) f), from _, have h1g : category_theory.epi (category_theory.limits.coprod.desc (𝟙 Y) g), from _, have huv : category_theory.limits.pushout.inl = category_theory.limits.pushout.inr, from _, have hvu : f ≫ category_theory.limits.pushout.inl = g ≫ category_theory.limits.pushout.inr, from _, have huu : f ≫ category_theory.limits.pushout.inl = g ≫ category_theory.limits.pushout.inl, from _, {cocone := category_theory.limits.cofork.of_π category_theory.limits.pushout.inl huu, is_colimit := category_theory.limits.cofork.is_colimit.mk (category_theory.limits.cofork.of_π category_theory.limits.pushout.inl huu) (λ (s : category_theory.limits.cofork f g), category_theory.limits.pushout.desc s.π s.π _) _ _}
@[instance]
def
category_theory.non_preadditive_abelian.has_equalizers
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C] :
A non_preadditive_abelian category has all equalizers.
@[instance]
def
category_theory.non_preadditive_abelian.has_coequalizers
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C] :
A non_preadditive_abelian category has all coequalizers.
theorem
category_theory.non_preadditive_abelian.mono_of_zero_kernel
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(f : X ⟶ Y)
(Z : C) :
If a zero morphism is a kernel of f, then f is a monomorphism.
theorem
category_theory.non_preadditive_abelian.epi_of_zero_cokernel
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(f : X ⟶ Y)
(Z : C) :
If a zero morphism is a cokernel of f, then f is an epimorphism.
def
category_theory.non_preadditive_abelian.zero_kernel_of_cancel_zero
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(f : X ⟶ Y) :
(∀ (Z : C) (g : Z ⟶ X), g ≫ f = 0 → g = 0) → category_theory.limits.is_limit (category_theory.limits.kernel_fork.of_ι 0 _)
If g ≫ f = 0 implies g = 0 for all g, then 0 : 0 ⟶ X is a kernel of f.
Equations
def
category_theory.non_preadditive_abelian.zero_cokernel_of_zero_cancel
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(f : X ⟶ Y) :
(∀ (Z : C) (g : Y ⟶ Z), f ≫ g = 0 → g = 0) → category_theory.limits.is_colimit (category_theory.limits.cokernel_cofork.of_π 0 _)
If f ≫ g = 0 implies g = 0 for all g, then 0 : Y ⟶ 0 is a cokernel of f.
Equations
theorem
category_theory.non_preadditive_abelian.mono_of_cancel_zero
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(f : X ⟶ Y) :
(∀ (Z : C) (g : Z ⟶ X), g ≫ f = 0 → g = 0) → category_theory.mono f
If g ≫ f = 0 implies g = 0 for all g, then f is a monomorphism.
theorem
category_theory.non_preadditive_abelian.epi_of_zero_cancel
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(f : X ⟶ Y) :
(∀ (Z : C) (g : Y ⟶ Z), f ≫ g = 0 → g = 0) → category_theory.epi f
If f ≫ g = 0 implies g = 0 for all g, then g is a monomorphism.
def
category_theory.non_preadditive_abelian.image
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{P Q : C} :
(P ⟶ Q) → C
The kernel of the cokernel of f is called the image of f.
def
category_theory.non_preadditive_abelian.image.ι
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{P Q : C}
(f : P ⟶ Q) :
The inclusion of the image into the codomain.
def
category_theory.non_preadditive_abelian.factor_thru_image
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{P Q : C}
(f : P ⟶ Q) :
There is a canonical epimorphism p : P ⟶ image f for every f.
@[simp]
theorem
category_theory.non_preadditive_abelian.image.fac_assoc
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{P Q : C}
(f : P ⟶ Q)
{X' : C}
(f' : Q ⟶ X') :
@[simp]
theorem
category_theory.non_preadditive_abelian.image.fac
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{P Q : C}
(f : P ⟶ Q) :
f factors through its image via the canonical morphism p.
@[instance]
def
category_theory.non_preadditive_abelian.category_theory.epi
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{P Q : C}
(f : P ⟶ Q) :
The map p : P ⟶ image f is an epimorphism
Equations
- _ = _
@[instance]
def
category_theory.non_preadditive_abelian.mono_factor_thru_image
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{P Q : C}
(f : P ⟶ Q)
[category_theory.mono f] :
Equations
- _ = _
@[instance]
def
category_theory.non_preadditive_abelian.is_iso_factor_thru_image
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{P Q : C}
(f : P ⟶ Q)
[category_theory.mono f] :
def
category_theory.non_preadditive_abelian.coimage
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{P Q : C} :
(P ⟶ Q) → C
The cokernel of the kernel of f is called the coimage of f.
def
category_theory.non_preadditive_abelian.coimage.π
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{P Q : C}
(f : P ⟶ Q) :
The projection onto the coimage.
def
category_theory.non_preadditive_abelian.factor_thru_coimage
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{P Q : C}
(f : P ⟶ Q) :
There is a canonical monomorphism i : coimage f ⟶ Q.
theorem
category_theory.non_preadditive_abelian.coimage.fac
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{P Q : C}
(f : P ⟶ Q) :
f factors through its coimage via the canonical morphism p.
@[instance]
def
category_theory.non_preadditive_abelian.category_theory.mono
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{P Q : C}
(f : P ⟶ Q) :
The canonical morphism i : coimage f ⟶ Q is a monomorphism
Equations
- _ = _
@[instance]
def
category_theory.non_preadditive_abelian.epi_factor_thru_coimage
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{P Q : C}
(f : P ⟶ Q)
[category_theory.epi f] :
Equations
- _ = _
@[instance]
def
category_theory.non_preadditive_abelian.is_iso_factor_thru_coimage
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{P Q : C}
(f : P ⟶ Q)
[category_theory.epi f] :
def
category_theory.non_preadditive_abelian.epi_is_cokernel_of_kernel
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
{f : X ⟶ Y}
[category_theory.epi f]
(s : category_theory.limits.fork f 0) :
In a non_preadditive_abelian category, an epi is the cokernel of its kernel. More precisely:
If f is an epimorphism and s is some limit kernel cone on f, then f is a cokernel
of fork.ι s.
Equations
- category_theory.non_preadditive_abelian.epi_is_cokernel_of_kernel s h = category_theory.limits.is_cokernel.cokernel_iso s.ι f (category_theory.limits.cokernel.of_iso_comp ((category_theory.limits.limit.cone (category_theory.limits.parallel_pair f 0)).π.app category_theory.limits.walking_parallel_pair.zero) s.ι ((category_theory.limits.limit.is_limit (category_theory.limits.parallel_pair f 0)).cone_point_unique_up_to_iso h) _) (category_theory.as_iso (category_theory.non_preadditive_abelian.factor_thru_coimage f)) _
def
category_theory.non_preadditive_abelian.mono_is_kernel_of_cokernel
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
{f : X ⟶ Y}
[category_theory.mono f]
(s : category_theory.limits.cofork f 0) :
In a non_preadditive_abelian category, a mono is the kernel of its cokernel. More precisely:
If f is a monomorphism and s is some colimit cokernel cocone on f, then f is a kernel
of cofork.π s.
Equations
- category_theory.non_preadditive_abelian.mono_is_kernel_of_cokernel s h = category_theory.limits.is_kernel.iso_kernel s.π f (category_theory.limits.kernel.of_comp_iso ((category_theory.limits.colimit.cocone (category_theory.limits.parallel_pair f 0)).ι.app category_theory.limits.walking_parallel_pair.one) s.π (h.cocone_point_unique_up_to_iso (category_theory.limits.colimit.is_colimit (category_theory.limits.parallel_pair f 0))) _) (category_theory.as_iso (category_theory.non_preadditive_abelian.factor_thru_image f)) _
def
category_theory.non_preadditive_abelian.Δ
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
(A : C) :
The diagonal morphism (𝟙 A, 𝟙 A) : A → A ⨯ A.
def
category_theory.non_preadditive_abelian.r
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
(A : C) :
The composite A ⟶ A ⨯ A ⟶ cokernel (Δ A), where the first map is (𝟙 A, 0) and the second map
is the canonical projection into the cokernel.
@[instance]
def
category_theory.non_preadditive_abelian.mono_Δ
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{A : C} :
Equations
@[instance]
def
category_theory.non_preadditive_abelian.mono_r
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{A : C} :
Equations
@[instance]
def
category_theory.non_preadditive_abelian.epi_r
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{A : C} :
Equations
@[instance]
def
category_theory.non_preadditive_abelian.is_iso_r
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{A : C} :
def
category_theory.non_preadditive_abelian.σ
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{A : C} :
The composite A ⨯ A ⟶ cokernel (Δ A) ⟶ A given by the natural projection into the cokernel
followed by the inverse of r. In the category of modules, using the normal kernels and
cokernels, this map is equal to the map (a, b) ↦ a - b, hence the name σ for
"subtraction".
@[simp]
theorem
category_theory.non_preadditive_abelian.Δ_σ
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X : C} :
@[simp]
theorem
category_theory.non_preadditive_abelian.Δ_σ_assoc
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X X' : C}
(f' : X ⟶ X') :
@[simp]
theorem
category_theory.non_preadditive_abelian.lift_σ_assoc
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X X' : C}
(f' : X ⟶ X') :
@[simp]
theorem
category_theory.non_preadditive_abelian.lift_σ
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X : C} :
@[simp]
theorem
category_theory.non_preadditive_abelian.Δ_map_assoc
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(f : X ⟶ Y)
{X' : C}
(f' : Y ⨯ Y ⟶ X') :
@[simp]
theorem
category_theory.non_preadditive_abelian.Δ_map
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(f : X ⟶ Y) :
theorem
category_theory.non_preadditive_abelian.lift_map_assoc
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(f : X ⟶ Y)
{X' : C}
(f' : Y ⨯ Y ⟶ X') :
category_theory.limits.prod.lift (𝟙 X) 0 ≫ category_theory.limits.prod.map f f ≫ f' = f ≫ category_theory.limits.prod.lift (𝟙 Y) 0 ≫ f'
theorem
category_theory.non_preadditive_abelian.lift_map
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(f : X ⟶ Y) :
category_theory.limits.prod.lift (𝟙 X) 0 ≫ category_theory.limits.prod.map f f = f ≫ category_theory.limits.prod.lift (𝟙 Y) 0
def
category_theory.non_preadditive_abelian.is_colimit_σ
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X : C} :
σ is a cokernel of Δ X.
Equations
- category_theory.non_preadditive_abelian.is_colimit_σ = category_theory.limits.cokernel.cokernel_iso (category_theory.non_preadditive_abelian.Δ X) category_theory.non_preadditive_abelian.σ (category_theory.as_iso (category_theory.non_preadditive_abelian.r X)).symm category_theory.non_preadditive_abelian.is_colimit_σ._proof_1
theorem
category_theory.non_preadditive_abelian.σ_comp
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(f : X ⟶ Y) :
This is the key identity satisfied by σ.
def
category_theory.non_preadditive_abelian.has_sub
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C} :
Subtraction of morphisms in a non_preadditive_abelian category.
Equations
def
category_theory.non_preadditive_abelian.has_neg
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C} :
Negation of morphisms in a non_preadditive_abelian category.
def
category_theory.non_preadditive_abelian.has_add
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C} :
Addition of morphisms in a non_preadditive_abelian category.
theorem
category_theory.non_preadditive_abelian.sub_def
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(a b : X ⟶ Y) :
theorem
category_theory.non_preadditive_abelian.add_def
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(a b : X ⟶ Y) :
theorem
category_theory.non_preadditive_abelian.neg_def
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(a : X ⟶ Y) :
theorem
category_theory.non_preadditive_abelian.sub_zero
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(a : X ⟶ Y) :
theorem
category_theory.non_preadditive_abelian.sub_self
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(a : X ⟶ Y) :
theorem
category_theory.non_preadditive_abelian.lift_sub_lift
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(a b c d : X ⟶ Y) :
category_theory.limits.prod.lift a b - category_theory.limits.prod.lift c d = category_theory.limits.prod.lift (a - c) (b - d)
theorem
category_theory.non_preadditive_abelian.sub_sub_sub
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(a b c d : X ⟶ Y) :
theorem
category_theory.non_preadditive_abelian.neg_sub
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(a b : X ⟶ Y) :
theorem
category_theory.non_preadditive_abelian.neg_neg
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(a : X ⟶ Y) :
theorem
category_theory.non_preadditive_abelian.add_comm
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(a b : X ⟶ Y) :
theorem
category_theory.non_preadditive_abelian.add_neg
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(a b : X ⟶ Y) :
theorem
category_theory.non_preadditive_abelian.add_neg_self
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(a : X ⟶ Y) :
theorem
category_theory.non_preadditive_abelian.neg_add_self
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(a : X ⟶ Y) :
theorem
category_theory.non_preadditive_abelian.neg_sub'
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(a b : X ⟶ Y) :
theorem
category_theory.non_preadditive_abelian.neg_add
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(a b : X ⟶ Y) :
theorem
category_theory.non_preadditive_abelian.sub_add
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(a b c : X ⟶ Y) :
theorem
category_theory.non_preadditive_abelian.add_assoc
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(a b c : X ⟶ Y) :
theorem
category_theory.non_preadditive_abelian.add_zero
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y : C}
(a : X ⟶ Y) :
theorem
category_theory.non_preadditive_abelian.comp_sub
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y Z : C}
(f : X ⟶ Y)
(g h : Y ⟶ Z) :
theorem
category_theory.non_preadditive_abelian.sub_comp
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
{X Y Z : C}
(f g : X ⟶ Y)
(h : Y ⟶ Z) :
theorem
category_theory.non_preadditive_abelian.comp_add
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
(X Y Z : C)
(f : X ⟶ Y)
(g h : Y ⟶ Z) :
theorem
category_theory.non_preadditive_abelian.add_comp
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C]
(X Y Z : C)
(f g : X ⟶ Y)
(h : Y ⟶ Z) :
def
category_theory.non_preadditive_abelian.preadditive
{C : Type u}
[category_theory.category C]
[category_theory.non_preadditive_abelian C] :
Every non_preadditive_abelian category is preadditive.
Equations
- category_theory.non_preadditive_abelian.preadditive = {hom_group := λ (X Y : C), {add := has_add.add category_theory.non_preadditive_abelian.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, neg := λ (f : X ⟶ Y), -f, add_left_neg := _, add_comm := _}, add_comp' := _, comp_add' := _}