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.

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

A category is called preadditive if P ⟶ Q is an abelian group such that composition is linear in both variables.

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

A category is called preadditive if P ⟶ Q is an abelian group such that composition is linear in both variables.

@[instance_reducible]

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

Equations

• CategoryTheory.End.instAddCommGroupOfPreadditive C X = CategoryTheory.End.homEquiv.addCommGroup

@[simp]

theorem CategoryTheory.End.zsmul_asHom (C : Type u) [Category.{v, u} C] [Preadditive C] (X : C) (n : ℤ) (x : End X) : (n • x).asHom = n • x.asHom

@[simp]

theorem CategoryTheory.End.nsmul_asHom (C : Type u) [Category.{v, u} C] [Preadditive C] (X : C) (n : ℕ) (x : End X) : (n • x).asHom = n • x.asHom

@[simp]

theorem CategoryTheory.End.zero_asHom (C : Type u) [Category.{v, u} C] [Preadditive C] (X : C) : asHom 0 = 0

@[simp]

theorem CategoryTheory.End.sub_asHom (C : Type u) [Category.{v, u} C] [Preadditive C] (X : C) (x y : End X) : (x - y).asHom = x.asHom - y.asHom

@[simp]

theorem CategoryTheory.End.neg_asHom (C : Type u) [Category.{v, u} C] [Preadditive C] (X : C) (x : End X) : (-x).asHom = -x.asHom

@[simp]

theorem CategoryTheory.End.add_asHom (C : Type u) [Category.{v, u} C] [Preadditive C] (X : C) (x y : End X) : (x + y).asHom = x.asHom + y.asHom

@[implicit_reducible]

def CategoryTheory.End.addEquiv {C : Type u} [Category.{v, u} C] [Preadditive C] {X : C} : End X ≃+ (X ⟶ X)

The additive bijection End X ≃+ (X ⟶ X) when X is an object in a preadditive category.

Equations

• CategoryTheory.End.addEquiv = { toEquiv := CategoryTheory.End.homEquiv, map_add' := ⋯ }

@[simp]

theorem CategoryTheory.End.addEquiv_symm_apply_asHom {C : Type u} [Category.{v, u} C] [Preadditive C] {X : C} (asHom : X ⟶ X) : (addEquiv.symm asHom).asHom = asHom

@[simp]

theorem CategoryTheory.End.addEquiv_apply {C : Type u} [Category.{v, u} C] [Preadditive C] {X : C} (self : End X) : addEquiv self = self.asHom

@[simp]

theorem CategoryTheory.End.sum_asHom (C : Type u) [Category.{v, u} C] [Preadditive C] {X : C} {ι : Type u_1} (s : Finset ι) (f : ι → End X) : (∑ i ∈ s, f i).asHom = ∑ i ∈ s, (f i).asHom

@[instance_reducible]

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

Equations

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

def CategoryTheory.InducedCategory.homAddEquiv {C : Type u} [Category.{v, u} C] [Preadditive C] {D : Type u'} {F : D → C} {X Y : InducedCategory C F} : (X ⟶ Y) ≃+ (F X ⟶ F Y)

The additive equivalence (X ⟶ Y) ≃+ (F X ⟶ F Y) when F : D → C and C is a preadditive category.

Equations

• CategoryTheory.InducedCategory.homAddEquiv = { toEquiv := CategoryTheory.InducedCategory.homEquiv, map_add' := ⋯ }

@[simp]

theorem CategoryTheory.InducedCategory.homAddEquiv_symm_apply_hom {C : Type u} [Category.{v, u} C] [Preadditive C] {D : Type u'} {F : D → C} {X Y : InducedCategory C F} (f : F X ⟶ F Y) : (homAddEquiv.symm f).hom = f

@[simp]

theorem CategoryTheory.InducedCategory.homAddEquiv_apply {C : Type u} [Category.{v, u} C] [Preadditive C] {D : Type u'} {F : D → C} {X Y : InducedCategory C F} (f : X ⟶ Y) : homAddEquiv f = f.hom

@[instance_reducible]

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

Equations

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

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

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

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

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

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

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

@[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] : Mono (-f)

@[instance_reducible, instance 100]

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

Equations

• CategoryTheory.Preadditive.preadditiveHasZeroMorphisms = { zero := inferInstance, comp_zero := ⋯, zero_comp := ⋯ }

theorem CategoryTheory.Preadditive.hasZeroObject_of_hasCoproduct (C : Type u) [Category.{v, u} C] [Preadditive C] [Limits.HasCoproduct PEmpty.elim] : Limits.HasZeroObject C

@[instance_reducible]

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

This instance is split off from the Ring (End X) instance to speed up instance search.

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

instance CategoryTheory.Preadditive.moduleEndRight {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} : Module (End Y) (X ⟶ Y)

Equations

• CategoryTheory.Preadditive.moduleEndRight = { toMulAction := CategoryTheory.End.mulActionRight, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

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

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

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

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)) : Mono 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) : Epi f

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

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

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)) : Epi 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) : Mono f

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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_reducible]

instance CategoryTheory.Preadditive.instSMulUnitsIntIso {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] {X 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} [Category.{v_1, 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.{v_1, u_1} C] [Preadditive C] {X Y : C} (a : ℤˣ) (e : X ≅ Y) : (a • e).inv = a⁻¹ • e.inv

@[instance_reducible]

instance CategoryTheory.Preadditive.instNegIso {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] {X 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} [Category.{v_1, 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.{v_1, u_1} C] [Preadditive C] {X Y : C} (e : X ≅ Y) : (-e).inv = -e.inv