mathlib documentation

category_theory.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 #

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 #

Tags #

additive, preadditive, Hom group, Ab-category, Ab-enriched

@[class]
structure category_theory.preadditive (C : Type u) [category_theory.category 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.

Instances of this typeclass
Instances of other typeclasses for category_theory.preadditive
@[simp]
theorem category_theory.preadditive.add_comp {C : Type u} [category_theory.category C] [self : category_theory.preadditive C] (P Q R : C) (f f' : P Q) (g : Q R) :
(f + f') g = f g + f' g
@[simp]
theorem category_theory.preadditive.comp_add {C : Type u} [category_theory.category C] [self : category_theory.preadditive C] (P Q R : C) (f : P Q) (g g' : Q R) :
f (g + g') = f g + f g'
@[simp]
theorem category_theory.preadditive.add_comp_assoc {C : Type u} [category_theory.category C] [self : category_theory.preadditive C] (P Q R : C) (f f' : P Q) (g : Q R) {X' : C} (f'_1 : R X') :
(f + f') g f'_1 = (f g + f' g) f'_1
theorem category_theory.preadditive.comp_add_assoc {C : Type u} [category_theory.category C] [self : category_theory.preadditive C] (P Q R : C) (f : P Q) (g g' : Q R) {X' : C} (f' : R X') :
f (g + g') f' = (f g + f g') f'
@[protected, instance]
Equations
def category_theory.preadditive.left_comp {C : Type u} [category_theory.category C] [category_theory.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
def category_theory.preadditive.right_comp {C : Type u} [category_theory.category C] [category_theory.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

Composition as a bilinear group homomorphism

Equations
@[simp]
theorem category_theory.preadditive.sub_comp_assoc {C : Type u} [category_theory.category C] [category_theory.preadditive C] {P Q R : C} (f f' : P Q) (g : Q R) {X' : C} (f'_1 : R X') :
(f - f') g f'_1 = (f g - f' g) f'_1
@[simp]
theorem category_theory.preadditive.sub_comp {C : Type u} [category_theory.category C] [category_theory.preadditive C] {P Q R : C} (f f' : P Q) (g : Q R) :
(f - f') g = f g - f' g
@[simp]
theorem category_theory.preadditive.comp_sub {C : Type u} [category_theory.category C] [category_theory.preadditive C] {P Q R : C} (f : P Q) (g g' : Q R) :
f (g - g') = f g - f g'
theorem category_theory.preadditive.comp_sub_assoc {C : Type u} [category_theory.category C] [category_theory.preadditive C] {P Q R : C} (f : P Q) (g g' : Q R) {X' : C} (f' : R X') :
f (g - g') f' = (f g - f g') f'
@[simp]
theorem category_theory.preadditive.neg_comp_assoc {C : Type u} [category_theory.category C] [category_theory.preadditive C] {P Q R : C} (f : P Q) (g : Q R) {X' : C} (f' : R X') :
(-f) g f' = (-f g) f'
@[simp]
theorem category_theory.preadditive.neg_comp {C : Type u} [category_theory.category C] [category_theory.preadditive C] {P Q R : C} (f : P Q) (g : Q R) :
(-f) g = -f g
theorem category_theory.preadditive.comp_neg_assoc {C : Type u} [category_theory.category C] [category_theory.preadditive C] {P Q R : C} (f : P Q) (g : Q R) {X' : C} (f' : R X') :
f (-g) f' = (-f g) f'
@[simp]
theorem category_theory.preadditive.comp_neg {C : Type u} [category_theory.category C] [category_theory.preadditive C] {P Q R : C} (f : P Q) (g : Q R) :
f -g = -f g
theorem category_theory.preadditive.neg_comp_neg {C : Type u} [category_theory.category C] [category_theory.preadditive C] {P Q R : C} (f : P Q) (g : Q R) :
(-f) -g = f g
theorem category_theory.preadditive.neg_comp_neg_assoc {C : Type u} [category_theory.category C] [category_theory.preadditive C] {P Q R : C} (f : P Q) (g : Q R) {X' : C} (f' : R X') :
(-f) (-g) f' = f g f'
theorem category_theory.preadditive.nsmul_comp {C : Type u} [category_theory.category C] [category_theory.preadditive C] {P Q R : C} (f : P Q) (g : Q R) (n : ) :
(n f) g = n f g
theorem category_theory.preadditive.comp_nsmul {C : Type u} [category_theory.category C] [category_theory.preadditive C] {P Q R : C} (f : P Q) (g : Q R) (n : ) :
f (n g) = n f g
theorem category_theory.preadditive.zsmul_comp {C : Type u} [category_theory.category C] [category_theory.preadditive C] {P Q R : C} (f : P Q) (g : Q R) (n : ) :
(n f) g = n f g
theorem category_theory.preadditive.comp_zsmul {C : Type u} [category_theory.category C] [category_theory.preadditive C] {P Q R : C} (f : P Q) (g : Q R) (n : ) :
f (n g) = n f g
theorem category_theory.preadditive.comp_sum_assoc {C : Type u} [category_theory.category C] [category_theory.preadditive C] {P Q R : C} {J : Type u_1} (s : finset J) (f : P Q) (g : J (Q R)) {X' : C} (f' : R X') :
f s.sum g f' = s.sum (λ (j : J), f g j) f'
theorem category_theory.preadditive.comp_sum {C : Type u} [category_theory.category C] [category_theory.preadditive C] {P Q R : C} {J : Type u_1} (s : finset J) (f : P Q) (g : J (Q R)) :
f s.sum (λ (j : J), g j) = s.sum (λ (j : J), f g j)
theorem category_theory.preadditive.sum_comp {C : Type u} [category_theory.category C] [category_theory.preadditive C] {P Q R : C} {J : Type u_1} (s : finset J) (f : J (P Q)) (g : Q R) :
s.sum (λ (j : J), f j) g = s.sum (λ (j : J), f j g)
theorem category_theory.preadditive.sum_comp_assoc {C : Type u} [category_theory.category C] [category_theory.preadditive C] {P Q R : C} {J : Type u_1} (s : finset J) (f : J (P Q)) (g : Q R) {X' : C} (f' : R X') :
s.sum f g f' = s.sum (λ (j : J), f j g) f'
theorem category_theory.preadditive.mono_of_cancel_zero {C : Type u} [category_theory.category C] [category_theory.preadditive C] {Q R : C} (f : Q R) (h : {P : C} (g : P Q), g f = 0 g = 0) :
theorem category_theory.preadditive.epi_of_cancel_zero {C : Type u} [category_theory.category C] [category_theory.preadditive C] {P Q : C} (f : P Q) (h : {R : C} (g : Q R), f g = 0 g = 0) :

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

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

A preadditive category has a coequalizer for f and g if it has a cokernel for f - g.

A preadditive category has a cokernel for f - g if it has a coequalizer for f and g.