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
- homGroup : (P Q : C) → AddCommGroup (P ⟶ Q)
A category is called preadditive if
P ⟶ Qis 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 ⟶ Qis 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 ⟶ Qis an abelian group such that composition is linear in both variables.
A category is called preadditive if P ⟶ Q is an abelian group such that composition is
linear in both variables.
Instances
theorem
CategoryTheory.Preadditive.add_comp_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[self : CategoryTheory.Preadditive C]
(P : C)
(Q : C)
(R : C)
(f : P ⟶ Q)
(f' : P ⟶ Q)
(g : Q ⟶ R)
{Z : C}
(h : R ⟶ Z)
:
theorem
CategoryTheory.Preadditive.comp_add_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[self : CategoryTheory.Preadditive C]
(P : C)
(Q : C)
(R : C)
(f : P ⟶ Q)
(g : Q ⟶ R)
(g' : Q ⟶ R)
{Z : C}
(h : R ⟶ Z)
:
instance
CategoryTheory.Preadditive.inducedCategory
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{D : Type u'}
(F : D → C)
:
instance
CategoryTheory.Preadditive.fullSubcategory
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(Z : C → Prop)
:
instance
CategoryTheory.Preadditive.instAddCommGroupEndToCategoryStruct
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(X : C)
:
def
CategoryTheory.Preadditive.leftComp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{P : C}
{Q : C}
(R : C)
(f : P ⟶ Q)
:
Composition by a fixed left argument as a group homomorphism
Instances For
def
CategoryTheory.Preadditive.rightComp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(P : C)
{Q : C}
{R : C}
(g : Q ⟶ R)
:
Composition by a fixed right argument as a group homomorphism
Instances For
def
CategoryTheory.Preadditive.compHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{P : C}
{Q : C}
{R : C}
:
Composition as a bilinear group homomorphism
Instances For
theorem
CategoryTheory.Preadditive.sub_comp_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{P : C}
{Q : C}
{R : C}
(f : P ⟶ Q)
(f' : P ⟶ Q)
(g : Q ⟶ R)
{Z : C}
(h : R ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Preadditive.sub_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{P : C}
{Q : C}
{R : C}
(f : P ⟶ Q)
(f' : P ⟶ Q)
(g : Q ⟶ R)
:
theorem
CategoryTheory.Preadditive.comp_sub_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{P : C}
{Q : C}
{R : C}
(f : P ⟶ Q)
(g : Q ⟶ R)
(g' : Q ⟶ R)
{Z : C}
(h : R ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Preadditive.comp_sub
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{P : C}
{Q : C}
{R : C}
(f : P ⟶ Q)
(g : Q ⟶ R)
(g' : Q ⟶ R)
:
theorem
CategoryTheory.Preadditive.neg_comp_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{P : C}
{Q : C}
{R : C}
(f : P ⟶ Q)
(g : Q ⟶ R)
{Z : C}
(h : R ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Preadditive.neg_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{P : C}
{Q : C}
{R : C}
(f : P ⟶ Q)
(g : Q ⟶ R)
:
theorem
CategoryTheory.Preadditive.comp_neg_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{P : C}
{Q : C}
{R : C}
(f : P ⟶ Q)
(g : Q ⟶ R)
{Z : C}
(h : R ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Preadditive.comp_neg
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{P : C}
{Q : C}
{R : C}
(f : P ⟶ Q)
(g : Q ⟶ R)
:
theorem
CategoryTheory.Preadditive.neg_comp_neg_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{P : C}
{Q : C}
{R : C}
(f : P ⟶ Q)
(g : Q ⟶ R)
{Z : C}
(h : R ⟶ Z)
:
theorem
CategoryTheory.Preadditive.neg_comp_neg
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{P : C}
{Q : C}
{R : C}
(f : P ⟶ Q)
(g : Q ⟶ R)
:
theorem
CategoryTheory.Preadditive.nsmul_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{P : C}
{Q : C}
{R : C}
(f : P ⟶ Q)
(g : Q ⟶ R)
(n : ℕ)
:
CategoryTheory.CategoryStruct.comp (n • f) g = n • CategoryTheory.CategoryStruct.comp f g
theorem
CategoryTheory.Preadditive.comp_nsmul
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{P : C}
{Q : C}
{R : C}
(f : P ⟶ Q)
(g : Q ⟶ R)
(n : ℕ)
:
CategoryTheory.CategoryStruct.comp f (n • g) = n • CategoryTheory.CategoryStruct.comp f g
theorem
CategoryTheory.Preadditive.zsmul_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{P : C}
{Q : C}
{R : C}
(f : P ⟶ Q)
(g : Q ⟶ R)
(n : ℤ)
:
CategoryTheory.CategoryStruct.comp (n • f) g = n • CategoryTheory.CategoryStruct.comp f g
theorem
CategoryTheory.Preadditive.comp_zsmul
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{P : C}
{Q : C}
{R : C}
(f : P ⟶ Q)
(g : Q ⟶ R)
(n : ℤ)
:
CategoryTheory.CategoryStruct.comp f (n • g) = n • CategoryTheory.CategoryStruct.comp f g
theorem
CategoryTheory.Preadditive.comp_sum_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{P : C}
{Q : C}
{R : C}
{J : Type u_1}
(s : Finset J)
(f : P ⟶ Q)
(g : J → (Q ⟶ R))
{Z : C}
(h : R ⟶ Z)
:
CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (Finset.sum s fun j => g j) h) = CategoryTheory.CategoryStruct.comp (Finset.sum s fun j => CategoryTheory.CategoryStruct.comp f (g j)) h
theorem
CategoryTheory.Preadditive.comp_sum
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{P : C}
{Q : C}
{R : C}
{J : Type u_1}
(s : Finset J)
(f : P ⟶ Q)
(g : J → (Q ⟶ R))
:
CategoryTheory.CategoryStruct.comp f (Finset.sum s fun j => g j) = Finset.sum s fun j => CategoryTheory.CategoryStruct.comp f (g j)
theorem
CategoryTheory.Preadditive.sum_comp_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{P : C}
{Q : C}
{R : C}
{J : Type u_1}
(s : Finset J)
(f : J → (P ⟶ Q))
(g : Q ⟶ R)
{Z : C}
(h : R ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (Finset.sum s fun j => f j) (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp (Finset.sum s fun j => CategoryTheory.CategoryStruct.comp (f j) g) h
theorem
CategoryTheory.Preadditive.sum_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{P : C}
{Q : C}
{R : C}
{J : Type u_1}
(s : Finset J)
(f : J → (P ⟶ Q))
(g : Q ⟶ R)
:
CategoryTheory.CategoryStruct.comp (Finset.sum s fun j => f j) g = Finset.sum s fun j => CategoryTheory.CategoryStruct.comp (f j) g
instance
CategoryTheory.Preadditive.instEpiNegHomToQuiverToCategoryStructToNegToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidHomGroup
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{P : C}
{Q : C}
{f : P ⟶ Q}
[CategoryTheory.Epi f]
:
instance
CategoryTheory.Preadditive.instMonoNegHomToQuiverToCategoryStructToNegToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidHomGroup
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{P : C}
{Q : C}
{f : P ⟶ Q}
[CategoryTheory.Mono f]
:
instance
CategoryTheory.Preadditive.instSemiringEndToCategoryStruct
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
:
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
instance
CategoryTheory.Preadditive.instRingEndToCategoryStruct
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
:
Porting note: It looks like Ring's parent classes changed in Lean 4 so the previous instance needed modification. Was following my nose here.
instance
CategoryTheory.Preadditive.moduleEndRight
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
:
Module (CategoryTheory.End Y) (X ⟶ Y)
theorem
CategoryTheory.Preadditive.mono_of_cancel_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{Q : C}
{R : C}
(f : Q ⟶ R)
(h : ∀ {P : C} (g : P ⟶ Q), CategoryTheory.CategoryStruct.comp g f = 0 → g = 0)
:
theorem
CategoryTheory.Preadditive.mono_iff_cancel_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{Q : C}
{R : C}
(f : Q ⟶ R)
:
CategoryTheory.Mono f ↔ ∀ (P : C) (g : P ⟶ Q), CategoryTheory.CategoryStruct.comp g f = 0 → g = 0
theorem
CategoryTheory.Preadditive.mono_of_kernel_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair f 0)]
(w : CategoryTheory.Limits.kernel.ι f = 0)
:
theorem
CategoryTheory.Preadditive.epi_of_cancel_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{P : C}
{Q : C}
(f : P ⟶ Q)
(h : ∀ {R : C} (g : Q ⟶ R), CategoryTheory.CategoryStruct.comp f g = 0 → g = 0)
:
theorem
CategoryTheory.Preadditive.epi_iff_cancel_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{P : C}
{Q : C}
(f : P ⟶ Q)
:
CategoryTheory.Epi f ↔ ∀ (R : C) (g : Q ⟶ R), CategoryTheory.CategoryStruct.comp f g = 0 → g = 0
theorem
CategoryTheory.Preadditive.epi_of_cokernel_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelPair f 0)]
(w : CategoryTheory.Limits.cokernel.π f = 0)
:
@[simp]
theorem
CategoryTheory.Preadditive.IsIso.comp_left_eq_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{P : C}
{Q : C}
{R : C}
(f : P ⟶ Q)
(g : Q ⟶ R)
[CategoryTheory.IsIso f]
:
CategoryTheory.CategoryStruct.comp f g = 0 ↔ g = 0
@[simp]
theorem
CategoryTheory.Preadditive.IsIso.comp_right_eq_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{P : C}
{Q : C}
{R : C}
(f : P ⟶ Q)
(g : Q ⟶ R)
[CategoryTheory.IsIso g]
:
CategoryTheory.CategoryStruct.comp f g = 0 ↔ f = 0
theorem
CategoryTheory.Preadditive.mono_of_kernel_iso_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair f 0)]
(w : CategoryTheory.Limits.kernel f ≅ 0)
:
theorem
CategoryTheory.Preadditive.epi_of_cokernel_iso_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelPair f 0)]
(w : CategoryTheory.Limits.cokernel f ≅ 0)
:
@[simp]
theorem
CategoryTheory.Preadditive.forkOfKernelFork_pt
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(c : CategoryTheory.Limits.KernelFork (f - g))
:
(CategoryTheory.Preadditive.forkOfKernelFork c).pt = c.pt
def
CategoryTheory.Preadditive.forkOfKernelFork
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(c : CategoryTheory.Limits.KernelFork (f - g))
:
Map a kernel cone on the difference of two morphisms to the equalizer fork.
Instances For
@[simp]
theorem
CategoryTheory.Preadditive.forkOfKernelFork_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(c : CategoryTheory.Limits.KernelFork (f - g))
:
def
CategoryTheory.Preadditive.kernelForkOfFork
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(c : CategoryTheory.Limits.Fork f g)
:
Map any equalizer fork to a cone on the difference of the two morphisms.
Instances For
@[simp]
theorem
CategoryTheory.Preadditive.kernelForkOfFork_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(c : CategoryTheory.Limits.Fork f g)
:
@[simp]
theorem
CategoryTheory.Preadditive.kernelForkOfFork_ofι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{P : C}
(ι : P ⟶ X)
(w : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g)
:
def
CategoryTheory.Preadditive.isLimitForkOfKernelFork
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{c : CategoryTheory.Limits.KernelFork (f - g)}
(i : CategoryTheory.Limits.IsLimit c)
:
A kernel of f - g is an equalizer of f and g.
Instances For
@[simp]
theorem
CategoryTheory.Preadditive.isLimitForkOfKernelFork_lift
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{c : CategoryTheory.Limits.KernelFork (f - g)}
(i : CategoryTheory.Limits.IsLimit c)
(s : CategoryTheory.Limits.Fork f g)
:
def
CategoryTheory.Preadditive.isLimitKernelForkOfFork
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{c : CategoryTheory.Limits.Fork f g}
(i : CategoryTheory.Limits.IsLimit c)
:
An equalizer of f and g is a kernel of f - g.
Instances For
theorem
CategoryTheory.Preadditive.hasEqualizer_of_hasKernel
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasKernel (f - g)]
:
A preadditive category has an equalizer for f and g if it has a kernel for f - g.
theorem
CategoryTheory.Preadditive.hasKernel_of_hasEqualizer
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasEqualizer f g]
:
A preadditive category has a kernel for f - g if it has an equalizer for f and g.
@[simp]
theorem
CategoryTheory.Preadditive.coforkOfCokernelCofork_pt
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(c : CategoryTheory.Limits.CokernelCofork (f - g))
:
(CategoryTheory.Preadditive.coforkOfCokernelCofork c).pt = c.pt
def
CategoryTheory.Preadditive.coforkOfCokernelCofork
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(c : CategoryTheory.Limits.CokernelCofork (f - g))
:
Map a cokernel cocone on the difference of two morphisms to the coequalizer cofork.
Instances For
@[simp]
theorem
CategoryTheory.Preadditive.coforkOfCokernelCofork_π
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(c : CategoryTheory.Limits.CokernelCofork (f - g))
:
def
CategoryTheory.Preadditive.cokernelCoforkOfCofork
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(c : CategoryTheory.Limits.Cofork f g)
:
Map any coequalizer cofork to a cocone on the difference of the two morphisms.
Instances For
@[simp]
theorem
CategoryTheory.Preadditive.cokernelCoforkOfCofork_π
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(c : CategoryTheory.Limits.Cofork f g)
:
@[simp]
theorem
CategoryTheory.Preadditive.cokernelCoforkOfCofork_ofπ
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{P : C}
(π : Y ⟶ P)
(w : CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π)
:
def
CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{c : CategoryTheory.Limits.CokernelCofork (f - g)}
(i : CategoryTheory.Limits.IsColimit c)
:
A cokernel of f - g is a coequalizer of f and g.
Instances For
@[simp]
theorem
CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork_desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{c : CategoryTheory.Limits.CokernelCofork (f - g)}
(i : CategoryTheory.Limits.IsColimit c)
(s : CategoryTheory.Limits.Cofork f g)
:
def
CategoryTheory.Preadditive.isColimitCokernelCoforkOfCofork
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{c : CategoryTheory.Limits.Cofork f g}
(i : CategoryTheory.Limits.IsColimit c)
:
A coequalizer of f and g is a cokernel of f - g.
Instances For
theorem
CategoryTheory.Preadditive.hasCoequalizer_of_hasCokernel
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel (f - g)]
:
A preadditive category has a coequalizer for f and g if it has a cokernel for f - g.
theorem
CategoryTheory.Preadditive.hasCokernel_of_hasCoequalizer
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasCoequalizer f g]
:
A preadditive category has a cokernel for f - g if it has a coequalizer for f and g.
theorem
CategoryTheory.Preadditive.hasEqualizers_of_hasKernels
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasKernels C]
:
If a preadditive category has all kernels, then it also has all equalizers.
theorem
CategoryTheory.Preadditive.hasCoequalizers_of_hasCokernels
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasCokernels C]
:
If a preadditive category has all cokernels, then it also has all coequalizers.