Commit 2024-12-13 08:59 e42ca30b

View on Github →

feat(CategoryTheory/Abelian): AB axioms carry over to functor categories (#19914)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/Grp/AB.lean

Renamed Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean to Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean

added theorem CategoryTheory.HasExactColimitsOfShape.domain_of_functor

added theorem CategoryTheory.HasExactLimitsOfShape.domain_of_functor

Created Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/FunctorCategory.lean

Created Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Sheaf.lean

Modified Mathlib/Condensed/Light/AB.lean