Documentation

Mathlib.CategoryTheory.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

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

Instances
    def CategoryTheory.Preadditive.leftComp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {P : C} {Q : C} (R : C) (f : P Q) :
    (Q R) →+ (P R)

    Composition by a fixed left argument as a group homomorphism

    Instances For
      def CategoryTheory.Preadditive.rightComp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (P : C) {Q : C} {R : C} (g : Q R) :
      (P Q) →+ (P R)

      Composition by a fixed right argument as a group homomorphism

      Instances For

        Composition as a bilinear group homomorphism

        Instances For
          theorem CategoryTheory.Preadditive.comp_sum {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {P : C} {Q : C} {R : C} {J : Type u_1} (s : Finset J) (f : P Q) (g : J → (Q R)) :
          theorem CategoryTheory.Preadditive.sum_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {P : C} {Q : C} {R : C} {J : Type u_1} (s : Finset J) (f : J → (P Q)) (g : Q R) :

          Porting note: adding this before the ring instance allowed moduleEndRight to find the correct Monoid structure on End. Moved both down after preadditiveHasZeroMorphisms to make use of them

          Porting note: It looks like Ring's parent classes changed in Lean 4 so the previous instance needed modification. Was following my nose here.

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

          Instances For

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

            Instances For

              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.

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

              Instances For

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

                Instances For

                  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.