Commit 2024-10-22 18:49 7d93d007

View on Github →

feat(CategoryTheory/Abelian): AB5 implies AB4 (#17406) An AB4 category is a category in which taking coproducts is exact, an AB5 category is one where taking filtered colimits is exact. This shows that any Abelian catgory which is AB5 is also AB4.

Estimated changes

Modified Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean

added def CategoryTheory.AB4.ofAB5

Modified Mathlib/CategoryTheory/Limits/Constructions/Filtered.lean

added def CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetEvaluationIso

Modified Mathlib/CategoryTheory/Limits/Preserves/FunctorCategory.lean