Documentation

Mathlib.Algebra.Category.Grp.AB5

The category of abelian groups satisfies Grothendieck's axiom AB5 #

noncomputable instance instPreservesHomologyFunctorAddCommGrpColim {J : Type u} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] :
CategoryTheory.Limits.colim.PreservesHomology
Equations
  • instPreservesHomologyFunctorAddCommGrpColim = CategoryTheory.Limits.colim.preservesHomologyOfMapExact
Equations
  • instPreservesFiniteLimitsFunctorAddCommGrpColim = CategoryTheory.Limits.colim.preservesFiniteLimitsOfPreservesHomology
Equations