Documentation

Mathlib.CategoryTheory.Preadditive.Basic

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 if g ≫ f = 0 → g = 0 for all composable g.
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 CategoryTheory.Preadditive (C : Type u) [Category.{v, u} C] :

Type (max u v)

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) : CategoryStruct.comp (f + f') g = CategoryStruct.comp f g + 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) : CategoryStruct.comp f (g + g') = CategoryStruct.comp f g + 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

theorem CategoryTheory.Preadditive.add_comp_assoc {C : Type u} {inst✝ : Category.{v, u} C} [self : Preadditive C] (P Q R : C) (f f' : P ⟶ Q) (g : Q ⟶ R) {Z : C} (h : R ⟶ Z) :

CategoryStruct.comp (f + f') (CategoryStruct.comp g h) = CategoryStruct.comp (CategoryStruct.comp f g + CategoryStruct.comp f' g) h

theorem CategoryTheory.Preadditive.comp_add_assoc {C : Type u} {inst✝ : Category.{v, u} C} [self : Preadditive C] (P Q R : C) (f : P ⟶ Q) (g g' : Q ⟶ R) {Z : C} (h : R ⟶ Z) :

CategoryStruct.comp f (CategoryStruct.comp (g + g') h) = CategoryStruct.comp (CategoryStruct.comp f g + CategoryStruct.comp f g') h

instance CategoryTheory.Preadditive.inducedCategory {C : Type u} [Category.{v, u} C] [Preadditive C] {D : Type u'} (F : D → C) :

Preadditive (InducedCategory C F)

Equations

instance CategoryTheory.Preadditive.fullSubcategory {C : Type u} [Category.{v, u} C] [Preadditive C] (Z : ObjectProperty C) :

Preadditive Z.FullSubcategory

Equations

instance CategoryTheory.Preadditive.instAddCommGroupEnd {C : Type u} [Category.{v, u} C] [Preadditive C] (X : C) :

AddCommGroup (End X)

Equations

def CategoryTheory.Preadditive.leftComp {C : Type u} [Category.{v, u} C] [Preadditive C] {P Q : C} (R : C) (f : P ⟶ Q) :

(Q ⟶ R) →+ (P ⟶ R)

Composition by a fixed left argument as a group homomorphism

Equations

Instances For

def CategoryTheory.Preadditive.rightComp {C : Type u} [Category.{v, u} C] [Preadditive C] (P : C) {Q R : C} (g : Q ⟶ R) :

(P ⟶ Q) →+ (P ⟶ R)

Composition by a fixed right argument as a group homomorphism

Equations

Instances For

def CategoryTheory.Preadditive.compHom {C : Type u} [Category.{v, u} C] [Preadditive C] {P Q R : C} :

(P ⟶ Q) →+ (Q ⟶ R) →+ (P ⟶ R)

Composition as a bilinear group homomorphism

Equations

Instances For

@[simp]

theorem CategoryTheory.Preadditive.sub_comp {C : Type u} [Category.{v, u} C] [Preadditive C] {P Q R : C} (f f' : P ⟶ Q) (g : Q ⟶ R) :

CategoryStruct.comp (f - f') g = CategoryStruct.comp f g - CategoryStruct.comp f' g

theorem CategoryTheory.Preadditive.sub_comp_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] {P Q R : C} (f f' : P ⟶ Q) (g : Q ⟶ R) {Z : C} (h : R ⟶ Z) :

CategoryStruct.comp (f - f') (CategoryStruct.comp g h) = CategoryStruct.comp (CategoryStruct.comp f g - CategoryStruct.comp f' g) h

@[simp]

theorem CategoryTheory.Preadditive.comp_sub {C : Type u} [Category.{v, u} C] [Preadditive C] {P Q R : C} (f : P ⟶ Q) (g g' : Q ⟶ R) :

CategoryStruct.comp f (g - g') = CategoryStruct.comp f g - CategoryStruct.comp f g'

theorem CategoryTheory.Preadditive.comp_sub_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] {P Q R : C} (f : P ⟶ Q) (g g' : Q ⟶ R) {Z : C} (h : R ⟶ Z) :

CategoryStruct.comp f (CategoryStruct.comp (g - g') h) = CategoryStruct.comp (CategoryStruct.comp f g - CategoryStruct.comp f g') h

@[simp]

theorem CategoryTheory.Preadditive.neg_comp {C : Type u} [Category.{v, u} C] [Preadditive C] {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R) :

CategoryStruct.comp (-f) g = -CategoryStruct.comp f g

theorem CategoryTheory.Preadditive.neg_comp_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R) {Z : C} (h : R ⟶ Z) :

CategoryStruct.comp (-f) (CategoryStruct.comp g h) = CategoryStruct.comp (-CategoryStruct.comp f g) h

@[simp]

theorem CategoryTheory.Preadditive.comp_neg {C : Type u} [Category.{v, u} C] [Preadditive C] {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R) :

CategoryStruct.comp f (-g) = -CategoryStruct.comp f g

theorem CategoryTheory.Preadditive.comp_neg_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R) {Z : C} (h : R ⟶ Z) :

CategoryStruct.comp f (CategoryStruct.comp (-g) h) = CategoryStruct.comp (-CategoryStruct.comp f g) h

theorem CategoryTheory.Preadditive.neg_comp_neg {C : Type u} [Category.{v, u} C] [Preadditive C] {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R) :

CategoryStruct.comp (-f) (-g) = CategoryStruct.comp f g

theorem CategoryTheory.Preadditive.neg_comp_neg_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R) {Z : C} (h : R ⟶ Z) :

CategoryStruct.comp (-f) (CategoryStruct.comp (-g) h) = CategoryStruct.comp f (CategoryStruct.comp g h)

theorem CategoryTheory.Preadditive.nsmul_comp {C : Type u} [Category.{v, u} C] [Preadditive C] {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R) (n : ℕ) :

CategoryStruct.comp (n • f) g = n • CategoryStruct.comp f g

theorem CategoryTheory.Preadditive.comp_nsmul {C : Type u} [Category.{v, u} C] [Preadditive C] {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R) (n : ℕ) :

CategoryStruct.comp f (n • g) = n • CategoryStruct.comp f g

theorem CategoryTheory.Preadditive.zsmul_comp {C : Type u} [Category.{v, u} C] [Preadditive C] {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R) (n : ℤ) :

CategoryStruct.comp (n • f) g = n • CategoryStruct.comp f g

theorem CategoryTheory.Preadditive.comp_zsmul {C : Type u} [Category.{v, u} C] [Preadditive C] {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R) (n : ℤ) :

CategoryStruct.comp f (n • g) = n • CategoryStruct.comp f g

theorem CategoryTheory.Preadditive.comp_sum {C : Type u} [Category.{v, u} C] [Preadditive C] {P Q R : C} {J : Type u_1} (s : Finset J) (f : P ⟶ Q) (g : J → (Q ⟶ R)) :

CategoryStruct.comp f (∑ j ∈ s, g j) = ∑ j ∈ s, CategoryStruct.comp f (g j)

theorem CategoryTheory.Preadditive.comp_sum_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] {P Q R : C} {J : Type u_1} (s : Finset J) (f : P ⟶ Q) (g : J → (Q ⟶ R)) {Z : C} (h : R ⟶ Z) :

CategoryStruct.comp f (CategoryStruct.comp (∑ j ∈ s, g j) h) = CategoryStruct.comp (∑ j ∈ s, CategoryStruct.comp f (g j)) h

theorem CategoryTheory.Preadditive.sum_comp {C : Type u} [Category.{v, u} C] [Preadditive C] {P Q R : C} {J : Type u_1} (s : Finset J) (f : J → (P ⟶ Q)) (g : Q ⟶ R) :

CategoryStruct.comp (∑ j ∈ s, f j) g = ∑ j ∈ s, CategoryStruct.comp (f j) g

theorem CategoryTheory.Preadditive.sum_comp_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] {P Q R : C} {J : Type u_1} (s : Finset J) (f : J → (P ⟶ Q)) (g : Q ⟶ R) {Z : C} (h : R ⟶ Z) :

CategoryStruct.comp (∑ j ∈ s, f j) (CategoryStruct.comp g h) = CategoryStruct.comp (∑ j ∈ s, CategoryStruct.comp (f j) g) h

theorem CategoryTheory.Preadditive.sum_comp' {C : Type u} [Category.{v, u} C] [Preadditive C] {P Q R S : C} {J : Type u_1} (s : Finset J) (f : J → (P ⟶ Q)) (g : J → (Q ⟶ R)) (h : R ⟶ S) :

CategoryStruct.comp (∑ j ∈ s, CategoryStruct.comp (f j) (g j)) h = ∑ j ∈ s, CategoryStruct.comp (f j) (CategoryStruct.comp (g j) h)

theorem CategoryTheory.Preadditive.sum_comp'_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] {P Q R S : C} {J : Type u_1} (s : Finset J) (f : J → (P ⟶ Q)) (g : J → (Q ⟶ R)) (h : R ⟶ S) {Z : C} (h✝ : S ⟶ Z) :

CategoryStruct.comp (∑ j ∈ s, CategoryStruct.comp (f j) (g j)) (CategoryStruct.comp h h✝) = CategoryStruct.comp (∑ j ∈ s, CategoryStruct.comp (f j) (CategoryStruct.comp (g j) h)) h✝

instance CategoryTheory.Preadditive.instEpiNegHom {C : Type u} [Category.{v, u} C] [Preadditive C] {P Q : C} {f : P ⟶ Q} [Epi f] :

Epi (-f)

instance CategoryTheory.Preadditive.instMonoNegHom {C : Type u} [Category.{v, u} C] [Preadditive C] {P Q : C} {f : P ⟶ Q} [Mono f] :

@[instance 100]

instance CategoryTheory.Preadditive.preadditiveHasZeroMorphisms {C : Type u} [Category.{v, u} C] [Preadditive C] :

Limits.HasZeroMorphisms C

Equations

instance CategoryTheory.Preadditive.instSemiringEnd {C : Type u} [Category.{v, u} C] [Preadditive C] {X : C} :

Semiring (End X)

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

instance CategoryTheory.Preadditive.instRingEnd {C : Type u} [Category.{v, u} C] [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.

Equations

instance CategoryTheory.Preadditive.moduleEndRight {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} :

Module (End Y) (X ⟶ Y)

Equations

theorem CategoryTheory.Preadditive.mono_of_cancel_zero {C : Type u} [Category.{v, u} C] [Preadditive C] {Q R : C} (f : Q ⟶ R) (h : ∀ {P : C} (g : P ⟶ Q), CategoryStruct.comp g f = 0 → g = 0) :

theorem CategoryTheory.Preadditive.mono_iff_cancel_zero {C : Type u} [Category.{v, u} C] [Preadditive C] {Q R : C} (f : Q ⟶ R) :

Mono f ↔ ∀ (P : C) (g : P ⟶ Q), CategoryStruct.comp g f = 0 → g = 0

theorem CategoryTheory.Preadditive.mono_of_kernel_zero {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f : X ⟶ Y} [Limits.HasLimit (Limits.parallelPair f 0)] (w : Limits.kernel.ι f = 0) :

theorem CategoryTheory.Preadditive.mono_of_isZero_kernel' {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f : X ⟶ Y} (c : Limits.KernelFork f) (hc : Limits.IsLimit c) (h : Limits.IsZero c.pt) :

theorem CategoryTheory.Preadditive.mono_iff_isZero_kernel' {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f : X ⟶ Y} (c : Limits.KernelFork f) (hc : Limits.IsLimit c) :

Mono f ↔ Limits.IsZero c.pt

theorem CategoryTheory.Preadditive.mono_of_isZero_kernel {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} (f : X ⟶ Y) [Limits.HasKernel f] (h : Limits.IsZero (Limits.kernel f)) :

theorem CategoryTheory.Preadditive.mono_iff_isZero_kernel {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} (f : X ⟶ Y) [Limits.HasKernel f] :

Mono f ↔ Limits.IsZero (Limits.kernel f)

theorem CategoryTheory.Preadditive.epi_of_cancel_zero {C : Type u} [Category.{v, u} C] [Preadditive C] {P Q : C} (f : P ⟶ Q) (h : ∀ {R : C} (g : Q ⟶ R), CategoryStruct.comp f g = 0 → g = 0) :

theorem CategoryTheory.Preadditive.epi_iff_cancel_zero {C : Type u} [Category.{v, u} C] [Preadditive C] {P Q : C} (f : P ⟶ Q) :

Epi f ↔ ∀ (R : C) (g : Q ⟶ R), CategoryStruct.comp f g = 0 → g = 0

theorem CategoryTheory.Preadditive.epi_of_cokernel_zero {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f : X ⟶ Y} [Limits.HasColimit (Limits.parallelPair f 0)] (w : Limits.cokernel.π f = 0) :

theorem CategoryTheory.Preadditive.epi_of_isZero_cokernel' {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f : X ⟶ Y} (c : Limits.CokernelCofork f) (hc : Limits.IsColimit c) (h : Limits.IsZero c.pt) :

theorem CategoryTheory.Preadditive.epi_iff_isZero_cokernel' {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f : X ⟶ Y} (c : Limits.CokernelCofork f) (hc : Limits.IsColimit c) :

Epi f ↔ Limits.IsZero c.pt

theorem CategoryTheory.Preadditive.epi_of_isZero_cokernel {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} (f : X ⟶ Y) [Limits.HasCokernel f] (h : Limits.IsZero (Limits.cokernel f)) :

theorem CategoryTheory.Preadditive.epi_iff_isZero_cokernel {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} (f : X ⟶ Y) [Limits.HasCokernel f] :

Epi f ↔ Limits.IsZero (Limits.cokernel f)

@[simp]

theorem CategoryTheory.Preadditive.IsIso.comp_left_eq_zero {C : Type u} [Category.{v, u} C] [Preadditive C] {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R) [IsIso f] :

CategoryStruct.comp f g = 0 ↔ g = 0

@[simp]

theorem CategoryTheory.Preadditive.IsIso.comp_right_eq_zero {C : Type u} [Category.{v, u} C] [Preadditive C] {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R) [IsIso g] :

CategoryStruct.comp f g = 0 ↔ f = 0

theorem CategoryTheory.Preadditive.mono_of_kernel_iso_zero {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] {X Y : C} {f : X ⟶ Y} [Limits.HasLimit (Limits.parallelPair f 0)] (w : Limits.kernel f ≅ 0) :

theorem CategoryTheory.Preadditive.epi_of_cokernel_iso_zero {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] {X Y : C} {f : X ⟶ Y} [Limits.HasColimit (Limits.parallelPair f 0)] (w : Limits.cokernel f ≅ 0) :

def CategoryTheory.Preadditive.forkOfKernelFork {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f g : X ⟶ Y} (c : Limits.KernelFork (f - g)) :

Limits.Fork f g

Map a kernel cone on the difference of two morphisms to the equalizer fork.

Equations

Instances For

@[simp]

theorem CategoryTheory.Preadditive.forkOfKernelFork_pt {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f g : X ⟶ Y} (c : Limits.KernelFork (f - g)) :

(forkOfKernelFork c).pt = c.pt

@[simp]

theorem CategoryTheory.Preadditive.forkOfKernelFork_ι {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f g : X ⟶ Y} (c : Limits.KernelFork (f - g)) :

(forkOfKernelFork c).ι = Limits.Fork.ι c

def CategoryTheory.Preadditive.kernelForkOfFork {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f g : X ⟶ Y} (c : Limits.Fork f g) :

Limits.KernelFork (f - g)

Map any equalizer fork to a cone on the difference of the two morphisms.

Equations

Instances For

@[simp]

theorem CategoryTheory.Preadditive.kernelForkOfFork_ι {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f g : X ⟶ Y} (c : Limits.Fork f g) :

Limits.Fork.ι (kernelForkOfFork c) = c.ι

@[simp]

theorem CategoryTheory.Preadditive.kernelForkOfFork_ofι {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f g : X ⟶ Y} {P : C} (ι : P ⟶ X) (w : CategoryStruct.comp ι f = CategoryStruct.comp ι g) :

kernelForkOfFork (Limits.Fork.ofι ι w) = Limits.KernelFork.ofι ι ⋯

def CategoryTheory.Preadditive.isLimitForkOfKernelFork {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f g : X ⟶ Y} {c : Limits.KernelFork (f - g)} (i : Limits.IsLimit c) :

Limits.IsLimit (forkOfKernelFork c)

A kernel of f - g is an equalizer of f and g.

Equations

Instances For

@[simp]

theorem CategoryTheory.Preadditive.isLimitForkOfKernelFork_lift {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f g : X ⟶ Y} {c : Limits.KernelFork (f - g)} (i : Limits.IsLimit c) (s : Limits.Fork f g) :

(isLimitForkOfKernelFork i).lift s = i.lift (kernelForkOfFork s)

def CategoryTheory.Preadditive.isLimitKernelForkOfFork {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f g : X ⟶ Y} {c : Limits.Fork f g} (i : Limits.IsLimit c) :

Limits.IsLimit (kernelForkOfFork c)

An equalizer of f and g is a kernel of f - g.

Equations

Instances For

theorem CategoryTheory.Preadditive.hasEqualizer_of_hasKernel {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} (f g : X ⟶ Y) [Limits.HasKernel (f - g)] :

Limits.HasEqualizer 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} [Category.{v, u} C] [Preadditive C] {X Y : C} (f g : X ⟶ Y) [Limits.HasEqualizer f g] :

Limits.HasKernel (f - g)

A preadditive category has a kernel for f - g if it has an equalizer for f and g.

def CategoryTheory.Preadditive.coforkOfCokernelCofork {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f g : X ⟶ Y} (c : Limits.CokernelCofork (f - g)) :

Limits.Cofork f g

Map a cokernel cocone on the difference of two morphisms to the coequalizer cofork.

Equations

Instances For

@[simp]

theorem CategoryTheory.Preadditive.coforkOfCokernelCofork_pt {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f g : X ⟶ Y} (c : Limits.CokernelCofork (f - g)) :

(coforkOfCokernelCofork c).pt = c.pt

@[simp]

theorem CategoryTheory.Preadditive.coforkOfCokernelCofork_π {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f g : X ⟶ Y} (c : Limits.CokernelCofork (f - g)) :

(coforkOfCokernelCofork c).π = Limits.Cofork.π c

def CategoryTheory.Preadditive.cokernelCoforkOfCofork {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f g : X ⟶ Y} (c : Limits.Cofork f g) :

Limits.CokernelCofork (f - g)

Map any coequalizer cofork to a cocone on the difference of the two morphisms.

Equations

Instances For

@[simp]

theorem CategoryTheory.Preadditive.cokernelCoforkOfCofork_π {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f g : X ⟶ Y} (c : Limits.Cofork f g) :

Limits.Cofork.π (cokernelCoforkOfCofork c) = c.π

@[simp]

theorem CategoryTheory.Preadditive.cokernelCoforkOfCofork_ofπ {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f g : X ⟶ Y} {P : C} (π : Y ⟶ P) (w : CategoryStruct.comp f π = CategoryStruct.comp g π) :

cokernelCoforkOfCofork (Limits.Cofork.ofπ π w) = Limits.CokernelCofork.ofπ π ⋯

def CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f g : X ⟶ Y} {c : Limits.CokernelCofork (f - g)} (i : Limits.IsColimit c) :

Limits.IsColimit (coforkOfCokernelCofork c)

A cokernel of f - g is a coequalizer of f and g.

Equations

Instances For

@[simp]

theorem CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork_desc {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f g : X ⟶ Y} {c : Limits.CokernelCofork (f - g)} (i : Limits.IsColimit c) (s : Limits.Cofork f g) :

(isColimitCoforkOfCokernelCofork i).desc s = i.desc (cokernelCoforkOfCofork s)

def CategoryTheory.Preadditive.isColimitCokernelCoforkOfCofork {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f g : X ⟶ Y} {c : Limits.Cofork f g} (i : Limits.IsColimit c) :

Limits.IsColimit (cokernelCoforkOfCofork c)

A coequalizer of f and g is a cokernel of f - g.

Equations

Instances For

theorem CategoryTheory.Preadditive.hasCoequalizer_of_hasCokernel {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} (f g : X ⟶ Y) [Limits.HasCokernel (f - g)] :

Limits.HasCoequalizer 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} [Category.{v, u} C] [Preadditive C] {X Y : C} (f g : X ⟶ Y) [Limits.HasCoequalizer f g] :

Limits.HasCokernel (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} [Category.{v, u} C] [Preadditive C] [Limits.HasKernels C] :

Limits.HasEqualizers C

If a preadditive category has all kernels, then it also has all equalizers.

theorem CategoryTheory.Preadditive.hasCoequalizers_of_hasCokernels {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasCokernels C] :

Limits.HasCoequalizers C

If a preadditive category has all cokernels, then it also has all coequalizers.

instance CategoryTheory.Preadditive.instSMulUnitsIntIso {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X Y : C} :

SMul ℤ ˣ (X ≅ Y)

Equations

@[simp]

theorem CategoryTheory.Preadditive.smul_iso_hom {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X Y : C} (a : ℤ ˣ) (e : X ≅ Y) :

(a • e).hom = a • e.hom

@[simp]

theorem CategoryTheory.Preadditive.smul_iso_inv {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X Y : C} (a : ℤ ˣ) (e : X ≅ Y) :

(a • e).inv = a⁻¹ • e.inv

instance CategoryTheory.Preadditive.instNegIso {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X Y : C} :

Neg (X ≅ Y)

Equations

@[simp]

theorem CategoryTheory.Preadditive.neg_iso_hom {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X Y : C} (e : X ≅ Y) :

(-e).hom = -e.hom

@[simp]

theorem CategoryTheory.Preadditive.neg_iso_inv {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X Y : C} (e : X ≅ Y) :

(-e).inv = -e.inv