Documentation

Mathlib.CategoryTheory.Abelian.FunctorCategory

If D is abelian, then the functor category C ⥤ D is also abelian. #

The abelian coimage in a functor category can be calculated componentwise.

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

    The abelian image in a functor category can be calculated componentwise.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      • CategoryTheory.Abelian.functorCategoryAbelian = let x := ; let x_1 := ; CategoryTheory.Abelian.ofCoimageImageComparisonIsIso