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

    Equations
    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

      Equations
      Instances For

        Composition as a bilinear group homomorphism

        Equations
        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

          Equations
          • CategoryTheory.Preadditive.instSemiringEndToCategoryStruct = let __src := CategoryTheory.End.monoid; Semiring.mk Monoid.npow

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

          Equations
          • CategoryTheory.Preadditive.instRingEndToCategoryStruct = let __src := inferInstance; let __src_1 := inferInstance; Ring.mk SubNegMonoid.zsmul
          Equations
          • CategoryTheory.Preadditive.moduleEndRight = Module.mk

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

          Equations
          Instances For

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

            Equations
            Instances For

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

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

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

                Equations
                • One or more equations did not get rendered due to their size.
                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.

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

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

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

                    Equations
                    • One or more equations did not get rendered due to their size.
                    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.

                      Equations
                      • CategoryTheory.Preadditive.instSMulUnitsIntInstMonoidIntIso = { smul := fun (a : ˣ) (e : X Y) => { hom := a e.hom, inv := a⁻¹ e.inv, hom_inv_id := , inv_hom_id := } }
                      @[simp]
                      theorem CategoryTheory.Preadditive.smul_iso_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : C} {Y : C} (a : ˣ) (e : X Y) :
                      (a e).hom = a e.hom
                      @[simp]
                      theorem CategoryTheory.Preadditive.smul_iso_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : C} {Y : C} (a : ˣ) (e : X Y) :
                      (a e).inv = a⁻¹ e.inv
                      Equations
                      • CategoryTheory.Preadditive.instNegIso = { neg := fun (e : X Y) => { hom := -e.hom, inv := -e.inv, hom_inv_id := , inv_hom_id := } }
                      @[simp]
                      theorem CategoryTheory.Preadditive.neg_iso_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : C} {Y : C} (e : X Y) :
                      (-e).hom = -e.hom
                      @[simp]
                      theorem CategoryTheory.Preadditive.neg_iso_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : C} {Y : C} (e : X Y) :
                      (-e).inv = -e.inv