mathlib3 documentation

category_theory.preadditive.basic

Preadditive categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
@[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
source
@[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
source
@[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'
source
@[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
source
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'
source
@[protected, instance]
def category_theory.preadditive.induced_category {C : Type u} [category_theory.category C] [category_theory.preadditive C] {D : Type u'} (F : D → C) :
category_theory.preadditive (category_theory.induced_category C F)
Equations
source
@[protected, instance]
def category_theory.preadditive.full_subcategory {C : Type u} [category_theory.category C] [category_theory.preadditive C] (Z : C → Prop) :
category_theory.preadditive (category_theory.full_subcategory Z)
Equations
source
@[protected, instance]
def category_theory.preadditive.category_theory.End.add_comm_group {C : Type u} [category_theory.category C] [category_theory.preadditive C] (X : C) :
add_comm_group (category_theory.End X)
Equations
source
@[protected, instance]
def category_theory.preadditive.category_theory.End.ring {C : Type u} [category_theory.category C] [category_theory.preadditive C] (X : C) :
ring (category_theory.End X)
Equations
source
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
source
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
source
def category_theory.preadditive.comp_hom {C : Type u} [category_theory.category C] [category_theory.preadditive C] {P Q R : C} :
(P ⟶ Q) →+ (Q ⟶ R) →+ (P ⟶ R)

Composition as a bilinear group homomorphism

Equations
source
@[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
source
@[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
source
@[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'
source
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'
source
@[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'
source
@[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
source
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'
source
@[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
source
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
source
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'
source
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
source
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
source
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
source
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
source
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'
source
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)
source
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)
source
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'
source
@[protected, instance]
def category_theory.preadditive.has_neg.neg.category_theory.epi {C : Type u} [category_theory.category C] [category_theory.preadditive C] {P Q : C} {f : P ⟶ Q} [category_theory.epi f] :
category_theory.epi (-f)
source
@[protected, instance]
def category_theory.preadditive.has_neg.neg.category_theory.mono {C : Type u} [category_theory.category C] [category_theory.preadditive C] {P Q : C} {f : P ⟶ Q} [category_theory.mono f] :
category_theory.mono (-f)
source
@[protected, instance]
def category_theory.preadditive.preadditive_has_zero_morphisms {C : Type u} [category_theory.category C] [category_theory.preadditive C] :
category_theory.limits.has_zero_morphisms C
Equations
source
@[protected, instance]
def category_theory.preadditive.module_End_right {C : Type u} [category_theory.category C] [category_theory.preadditive C] {X Y : C} :
module (category_theory.End Y) (X ⟶ Y)
Equations
source
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) :
category_theory.mono f
source
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 = 0 → g = 0
source
theorem category_theory.preadditive.mono_of_kernel_zero {C : Type u} [category_theory.category C] [category_theory.preadditive C] {X Y : C} {f : X ⟶ Y} [category_theory.limits.has_limit (category_theory.limits.parallel_pair f 0)] (w : category_theory.limits.kernel.ι f = 0) :
category_theory.mono f
source
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) :
category_theory.epi f
source
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 = 0 → g = 0
source
theorem category_theory.preadditive.epi_of_cokernel_zero {C : Type u} [category_theory.category C] [category_theory.preadditive C] {X Y : C} {f : X ⟶ Y} [category_theory.limits.has_colimit (category_theory.limits.parallel_pair f 0)] (w : category_theory.limits.cokernel.π f = 0) :
category_theory.epi f
source
@[simp]
theorem category_theory.preadditive.is_iso.comp_left_eq_zero {C : Type u} [category_theory.category C] [category_theory.preadditive C] {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R) [category_theory.is_iso f] :
f ≫ g = 0 ↔ g = 0
source
@[simp]
theorem category_theory.preadditive.is_iso.comp_right_eq_zero {C : Type u} [category_theory.category C] [category_theory.preadditive C] {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R) [category_theory.is_iso g] :
f ≫ g = 0 ↔ f = 0
source
theorem category_theory.preadditive.mono_of_kernel_iso_zero {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_zero_object C] {X Y : C} {f : X ⟶ Y} [category_theory.limits.has_limit (category_theory.limits.parallel_pair f 0)] (w : category_theory.limits.kernel f ≅ 0) :
category_theory.mono f
source
theorem category_theory.preadditive.epi_of_cokernel_iso_zero {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_zero_object C] {X Y : C} {f : X ⟶ Y} [category_theory.limits.has_colimit (category_theory.limits.parallel_pair f 0)] (w : category_theory.limits.cokernel f ≅ 0) :
category_theory.epi f
source
def category_theory.preadditive.fork_of_kernel_fork {C : Type u} [category_theory.category C] [category_theory.preadditive C] {X Y : C} {f g : X ⟶ Y} (c : category_theory.limits.kernel_fork (f - g)) :
category_theory.limits.fork f g

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

Equations
source
@[simp]
theorem category_theory.preadditive.fork_of_kernel_fork_X {C : Type u} [category_theory.category C] [category_theory.preadditive C] {X Y : C} {f g : X ⟶ Y} (c : category_theory.limits.kernel_fork (f - g)) :
(category_theory.preadditive.fork_of_kernel_fork c).X = c.X
source
@[simp]
theorem category_theory.preadditive.fork_of_kernel_fork_ι {C : Type u} [category_theory.category C] [category_theory.preadditive C] {X Y : C} {f g : X ⟶ Y} (c : category_theory.limits.kernel_fork (f - g)) :
(category_theory.preadditive.fork_of_kernel_fork c).ι = category_theory.limits.fork.ι c
source
def category_theory.preadditive.kernel_fork_of_fork {C : Type u} [category_theory.category C] [category_theory.preadditive C] {X Y : C} {f g : X ⟶ Y} (c : category_theory.limits.fork f g) :
category_theory.limits.kernel_fork (f - g)

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

Equations
source
@[simp]
theorem category_theory.preadditive.kernel_fork_of_fork_ι {C : Type u} [category_theory.category C] [category_theory.preadditive C] {X Y : C} {f g : X ⟶ Y} (c : category_theory.limits.fork f g) :
category_theory.limits.fork.ι (category_theory.preadditive.kernel_fork_of_fork c) = c.ι
source
@[simp]
theorem category_theory.preadditive.kernel_fork_of_fork_of_ι {C : Type u} [category_theory.category C] [category_theory.preadditive C] {X Y : C} {f g : X ⟶ Y} {P : C} (ι : P ⟶ X) (w : ι ≫ f = ι ≫ g) :
category_theory.preadditive.kernel_fork_of_fork (category_theory.limits.fork.of_ι ι w) = category_theory.limits.kernel_fork.of_ι ι _
source
def category_theory.preadditive.is_limit_fork_of_kernel_fork {C : Type u} [category_theory.category C] [category_theory.preadditive C] {X Y : C} {f g : X ⟶ Y} {c : category_theory.limits.kernel_fork (f - g)} (i : category_theory.limits.is_limit c) :
category_theory.limits.is_limit (category_theory.preadditive.fork_of_kernel_fork c)

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

Equations
source
@[simp]
theorem category_theory.preadditive.is_limit_fork_of_kernel_fork_lift {C : Type u} [category_theory.category C] [category_theory.preadditive C] {X Y : C} {f g : X ⟶ Y} {c : category_theory.limits.kernel_fork (f - g)} (i : category_theory.limits.is_limit c) (s : category_theory.limits.fork f g) :
(category_theory.preadditive.is_limit_fork_of_kernel_fork i).lift s = i.lift (category_theory.preadditive.kernel_fork_of_fork s)
source
def category_theory.preadditive.is_limit_kernel_fork_of_fork {C : Type u} [category_theory.category C] [category_theory.preadditive C] {X Y : C} {f g : X ⟶ Y} {c : category_theory.limits.fork f g} (i : category_theory.limits.is_limit c) :
category_theory.limits.is_limit (category_theory.preadditive.kernel_fork_of_fork c)

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

Equations
source
theorem category_theory.preadditive.has_equalizer_of_has_kernel {C : Type u} [category_theory.category C] [category_theory.preadditive C] {X Y : C} (f g : X ⟶ Y) [category_theory.limits.has_kernel (f - g)] :
category_theory.limits.has_equalizer f g

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

source
theorem category_theory.preadditive.has_kernel_of_has_equalizer {C : Type u} [category_theory.category C] [category_theory.preadditive C] {X Y : C} (f g : X ⟶ Y) [category_theory.limits.has_equalizer f g] :
category_theory.limits.has_kernel (f - g)

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

source
def category_theory.preadditive.cofork_of_cokernel_cofork {C : Type u} [category_theory.category C] [category_theory.preadditive C] {X Y : C} {f g : X ⟶ Y} (c : category_theory.limits.cokernel_cofork (f - g)) :
category_theory.limits.cofork f g

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

Equations
source
@[simp]
theorem category_theory.preadditive.cofork_of_cokernel_cofork_X {C : Type u} [category_theory.category C] [category_theory.preadditive C] {X Y : C} {f g : X ⟶ Y} (c : category_theory.limits.cokernel_cofork (f - g)) :
(category_theory.preadditive.cofork_of_cokernel_cofork c).X = c.X
source
@[simp]
theorem category_theory.preadditive.cofork_of_cokernel_cofork_π {C : Type u} [category_theory.category C] [category_theory.preadditive C] {X Y : C} {f g : X ⟶ Y} (c : category_theory.limits.cokernel_cofork (f - g)) :
(category_theory.preadditive.cofork_of_cokernel_cofork c).π = category_theory.limits.cofork.π c
source
def category_theory.preadditive.cokernel_cofork_of_cofork {C : Type u} [category_theory.category C] [category_theory.preadditive C] {X Y : C} {f g : X ⟶ Y} (c : category_theory.limits.cofork f g) :
category_theory.limits.cokernel_cofork (f - g)

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

Equations
source
@[simp]
theorem category_theory.preadditive.cokernel_cofork_of_cofork_π {C : Type u} [category_theory.category C] [category_theory.preadditive C] {X Y : C} {f g : X ⟶ Y} (c : category_theory.limits.cofork f g) :
category_theory.limits.cofork.π (category_theory.preadditive.cokernel_cofork_of_cofork c) = c.π
source
@[simp]
theorem category_theory.preadditive.cokernel_cofork_of_cofork_of_π {C : Type u} [category_theory.category C] [category_theory.preadditive C] {X Y : C} {f g : X ⟶ Y} {P : C} (π : Y ⟶ P) (w : f ≫ π = g ≫ π) :
category_theory.preadditive.cokernel_cofork_of_cofork (category_theory.limits.cofork.of_π π w) = category_theory.limits.cokernel_cofork.of_π π _
source
def category_theory.preadditive.is_colimit_cofork_of_cokernel_cofork {C : Type u} [category_theory.category C] [category_theory.preadditive C] {X Y : C} {f g : X ⟶ Y} {c : category_theory.limits.cokernel_cofork (f - g)} (i : category_theory.limits.is_colimit c) :
category_theory.limits.is_colimit (category_theory.preadditive.cofork_of_cokernel_cofork c)

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

Equations
source
@[simp]
theorem category_theory.preadditive.is_colimit_cofork_of_cokernel_cofork_desc {C : Type u} [category_theory.category C] [category_theory.preadditive C] {X Y : C} {f g : X ⟶ Y} {c : category_theory.limits.cokernel_cofork (f - g)} (i : category_theory.limits.is_colimit c) (s : category_theory.limits.cofork f g) :
(category_theory.preadditive.is_colimit_cofork_of_cokernel_cofork i).desc s = i.desc (category_theory.preadditive.cokernel_cofork_of_cofork s)
source
def category_theory.preadditive.is_colimit_cokernel_cofork_of_cofork {C : Type u} [category_theory.category C] [category_theory.preadditive C] {X Y : C} {f g : X ⟶ Y} {c : category_theory.limits.cofork f g} (i : category_theory.limits.is_colimit c) :
category_theory.limits.is_colimit (category_theory.preadditive.cokernel_cofork_of_cofork c)

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

Equations
source
theorem category_theory.preadditive.has_coequalizer_of_has_cokernel {C : Type u} [category_theory.category C] [category_theory.preadditive C] {X Y : C} (f g : X ⟶ Y) [category_theory.limits.has_cokernel (f - g)] :
category_theory.limits.has_coequalizer f g

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

source
theorem category_theory.preadditive.has_cokernel_of_has_coequalizer {C : Type u} [category_theory.category C] [category_theory.preadditive C] {X Y : C} (f g : X ⟶ Y) [category_theory.limits.has_coequalizer f g] :
category_theory.limits.has_cokernel (f - g)

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

source
theorem category_theory.preadditive.has_equalizers_of_has_kernels {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_kernels C] :
category_theory.limits.has_equalizers C

If a preadditive category has all kernels, then it also has all equalizers.

source
theorem category_theory.preadditive.has_coequalizers_of_has_cokernels {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_cokernels C] :
category_theory.limits.has_coequalizers C

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