Commit 2023-04-29 13:32 6a35632a

View on Github →

feat: port CategoryTheory.Abelian.Transfer (#3424)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Abelian/Transfer.lean

added def CategoryTheory.AbelianOfAdjunction.coimageIsoImage

added def CategoryTheory.AbelianOfAdjunction.coimageIsoImageAux

added theorem CategoryTheory.AbelianOfAdjunction.coimageIsoImage_hom

added def CategoryTheory.AbelianOfAdjunction.cokernelIso

added theorem CategoryTheory.AbelianOfAdjunction.hasCokernels

added theorem CategoryTheory.AbelianOfAdjunction.hasKernels

added def CategoryTheory.abelianOfAdjunction

added def CategoryTheory.abelianOfEquivalence