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
@[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'
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.gsmul_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_gsmul {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' = (∑ (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) (h : ∀ {P : C} (g : P Q), g f = 0g = 0) :
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) (h : ∀ {R : C} (g : Q R), f g = 0g = 0) :
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