Commit 2023-03-14 08:11 a5dc3767

View on Github →

feat: port CategoryTheory.Preadditive.LeftExact (#2853)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Preadditive/LeftExact.lean

added def CategoryTheory.Functor.isColimitMapCoconeBinaryCofanOfPreservesCokernels

added def CategoryTheory.Functor.isLimitMapConeBinaryFanOfPreservesKernels

added def CategoryTheory.Functor.preservesBinaryCoproductsOfPreservesCokernels

added def CategoryTheory.Functor.preservesBinaryProductOfPreservesKernels

added def CategoryTheory.Functor.preservesBinaryProductsOfPreservesKernels

added def CategoryTheory.Functor.preservesCoequalizerOfPreservesCokernels

added def CategoryTheory.Functor.preservesCoequalizersOfPreservesCokernels

added def CategoryTheory.Functor.preservesCoproductOfPreservesCokernels

added def CategoryTheory.Functor.preservesEqualizerOfPreservesKernels

added def CategoryTheory.Functor.preservesEqualizersOfPreservesKernels

added def CategoryTheory.Functor.preservesFiniteColimitsOfPreservesCokernels

added def CategoryTheory.Functor.preservesFiniteLimitsOfPreservesKernels