mathlib documentation

category_theory.preadditive.default

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)
  • hom_group : (Π (P Q : C), add_comm_group (P Q)) . "apply_instance"
  • add_comp' : (∀ (P Q R : C) (f f' : P Q) (g : Q R), (f + f') g = f g + f' g) . "obviously"
  • comp_add' : (∀ (P Q R : C) (f : P Q) (g g' : Q R), f (g + g') = f g + f g') . "obviously"

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

Instances
def category_theory.preadditive.left_comp {C : Type u} [category_theory.category C] [category_theory.preadditive C] {P Q : C} (R : C) :
(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} :
(Q R)(P Q) →+ (P R)

Composition by a fixed right argument as a 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.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' = (∑ (j : J) in s, 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 ∑ (j : J) in s, g j = ∑ (j : J) in s, 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) :
(∑ (j : J) in s, f j) g = ∑ (j : J) in s, 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' = (∑ (j : J) in s, 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) :
(∀ {P : C} (g : P Q), g f = 0g = 0)category_theory.mono f

theorem category_theory.preadditive.mono_iff_cancel_zero {C : Type u} [category_theory.category C] [category_theory.preadditive C] {Q R : C} (f : Q R) :
category_theory.mono f ∀ (P : C) (g : P Q), g f = 0g = 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) :
(∀ {R : C} (g : Q R), f g = 0g = 0)category_theory.epi f

theorem category_theory.preadditive.epi_iff_cancel_zero {C : Type u} [category_theory.category C] [category_theory.preadditive C] {P Q : C} (f : P Q) :
category_theory.epi f ∀ (R : C) (g : Q R), f g = 0g = 0