Commit 2024-09-12 14:29 185d8006

View on Github →

feat(CategoryTheory/Abelian): AB4 and AB5 axioms (#6504) Joint work with @IsaacHernando and Coleton Kotch.

Estimated changes

Modified Mathlib.lean

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

Created Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean

Modified Mathlib/CategoryTheory/Adjunction/Limits.lean

Modified Mathlib/CategoryTheory/Limits/Filtered.lean