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

@[simp]

theorem CategoryTheory.Preadditive.add_comp {C : Type u} :

∀ {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Preadditive C] (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 ⟶ Q is an abelian group such that composition is linear in both variables.

@[simp]

theorem CategoryTheory.Preadditive.comp_add {C : Type u} :

∀ {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Preadditive C] (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 ⟶ Q is an abelian group such that composition is linear in both variables.

theorem CategoryTheory.Preadditive.add_comp_assoc {C : Type u} :

∀ {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Preadditive C] (P Q R : C) (f f' : P ⟶ Q) (g : Q ⟶ R) {Z : C} (h : R ⟶ Z), CategoryTheory.CategoryStruct.comp (f + f') (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g + CategoryTheory.CategoryStruct.comp f' g) h

theorem CategoryTheory.Preadditive.comp_add_assoc {C : Type u} :

∀ {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Preadditive C] (P Q R : C) (f : P ⟶ Q) (g g' : Q ⟶ R) {Z : C} (h : R ⟶ Z), CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (g + g') h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g + CategoryTheory.CategoryStruct.comp f g') h

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

CategoryTheory.Preadditive (CategoryTheory.InducedCategory C F)

Equations

CategoryTheory.Preadditive.inducedCategory F = { homGroup := fun (P Q : CategoryTheory.InducedCategory C F) => CategoryTheory.Preadditive.homGroup (F P) (F Q), add_comp := ⋯, comp_add := ⋯ }

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

CategoryTheory.Preadditive (CategoryTheory.FullSubcategory Z)

Equations

CategoryTheory.Preadditive.fullSubcategory Z = { homGroup := fun (P Q : CategoryTheory.FullSubcategory Z) => CategoryTheory.Preadditive.homGroup P.obj Q.obj, add_comp := ⋯, comp_add := ⋯ }

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

AddCommGroup (CategoryTheory.End X)

Equations

CategoryTheory.Preadditive.instAddCommGroupEnd X = id inferInstance

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

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

Composition by a fixed left argument as a group homomorphism

Equations

CategoryTheory.Preadditive.leftComp R f = AddMonoidHom.mk' (fun (g : Q ⟶ R) => CategoryTheory.CategoryStruct.comp f g) ⋯

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

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

Composition by a fixed right argument as a group homomorphism

Equations

CategoryTheory.Preadditive.rightComp P g = AddMonoidHom.mk' (fun (f : P ⟶ Q) => CategoryTheory.CategoryStruct.comp f g) ⋯

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

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

Composition as a bilinear group homomorphism

Equations

CategoryTheory.Preadditive.compHom = AddMonoidHom.mk' (fun (f : P ⟶ Q) => CategoryTheory.Preadditive.leftComp R f) ⋯

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) :

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

@[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) :

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

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) :

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

@[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) :

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

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) :

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

@[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) :

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

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) :

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

@[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) :

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

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) :

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

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) :

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

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 (∑ j ∈ s, g j) h) = CategoryTheory.CategoryStruct.comp (∑ j ∈ s, 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 (∑ j ∈ s, g j) = ∑ j ∈ s, 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 (∑ j ∈ s, f j) (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp (∑ j ∈ s, 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 (∑ j ∈ s, f j) g = ∑ j ∈ s, CategoryTheory.CategoryStruct.comp (f j) g

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

CategoryTheory.Epi (-f)

Equations

⋯ = ⋯

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

CategoryTheory.Mono (-f)

Equations

⋯ = ⋯

@[instance 100]

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

CategoryTheory.Limits.HasZeroMorphisms C

Equations

CategoryTheory.Preadditive.preadditiveHasZeroMorphisms = CategoryTheory.Limits.HasZeroMorphisms.mk ⋯ ⋯

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

Semiring (CategoryTheory.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

CategoryTheory.Preadditive.instSemiringEnd = Semiring.mk ⋯ ⋯ ⋯ ⋯ Monoid.npow ⋯ ⋯

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

Ring (CategoryTheory.End X)

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

CategoryTheory.Preadditive.instRingEnd = Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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)

Equations

CategoryTheory.Preadditive.moduleEndRight = Module.mk ⋯ ⋯

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) :

CategoryTheory.Mono f

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) :

CategoryTheory.Mono f

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

CategoryTheory.Mono f

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

CategoryTheory.Mono f

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) :

CategoryTheory.Epi f

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) :

CategoryTheory.Epi f

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

CategoryTheory.Epi f

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

CategoryTheory.Epi f

@[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) :

CategoryTheory.Mono f

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) :

CategoryTheory.Epi f

@[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)) :

CategoryTheory.Limits.Fork f g

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

Equations

CategoryTheory.Preadditive.forkOfKernelFork c = CategoryTheory.Limits.Fork.ofι (CategoryTheory.Limits.Fork.ι c) ⋯

@[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)) :

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

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) :

CategoryTheory.Limits.KernelFork (f - g)

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

Equations

CategoryTheory.Preadditive.kernelForkOfFork c = CategoryTheory.Limits.Fork.ofι c.ι ⋯

@[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) :

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

@[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) :

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

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) :

CategoryTheory.Limits.IsLimit (CategoryTheory.Preadditive.forkOfKernelFork c)

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

Equations

One or more equations did not get rendered due to their size.

@[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) :

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

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) :

CategoryTheory.Limits.IsLimit (CategoryTheory.Preadditive.kernelForkOfFork c)

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

Equations

One or more equations did not get rendered due to their size.

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)] :

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

CategoryTheory.Limits.HasKernel (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)) :

CategoryTheory.Limits.Cofork f g

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

Equations

CategoryTheory.Preadditive.coforkOfCokernelCofork c = CategoryTheory.Limits.Cofork.ofπ (CategoryTheory.Limits.Cofork.π c) ⋯

@[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)) :

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

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) :

CategoryTheory.Limits.CokernelCofork (f - g)

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

Equations

CategoryTheory.Preadditive.cokernelCoforkOfCofork c = CategoryTheory.Limits.Cofork.ofπ c.π ⋯

@[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) :

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

@[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 π) :

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

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) :

CategoryTheory.Limits.IsColimit (CategoryTheory.Preadditive.coforkOfCokernelCofork c)

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

Equations

One or more equations did not get rendered due to their size.

@[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) :

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

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) :

CategoryTheory.Limits.IsColimit (CategoryTheory.Preadditive.cokernelCoforkOfCofork c)

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

Equations

One or more equations did not get rendered due to their size.

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)] :

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

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

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

CategoryTheory.Limits.HasCoequalizers C

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

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

SMul ℤ ˣ (X ≅ Y)

Equations

CategoryTheory.Preadditive.instSMulUnitsIntIso = { smul := fun (a : ℤ ˣ) (e : X ≅ Y) => { hom := ↑a • e.hom, inv := ↑a⁻¹ • e.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ } }

@[simp]

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

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

@[simp]

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

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

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

Neg (X ≅ Y)

Equations

CategoryTheory.Preadditive.instNegIso = { neg := fun (e : X ≅ Y) => { hom := -e.hom, inv := -e.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ } }

@[simp]

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

(-e).hom = -e.hom

@[simp]

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

(-e).inv = -e.inv