mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(category_theory/abelian/transfer): adjoint functor transfers "enough-injectiveness"

Open jjaassoonn opened this issue 3 years ago • 1 comments

If $A, B$ are abelian categories and $L\dashv R$ is a pair of adjoint functors, where $L$ is faithful and exact, then enough invectiveness of $B$ implies that of $A$

  • [x] depends on: #14581
  • [x] depends on: #15262 to fix a timeout.

Open in Gitpod

jjaassoonn avatar Jul 10 '22 23:07 jjaassoonn

This PR/issue depends on:

  • ~~leanprover-community/mathlib#14581~~
  • ~~leanprover-community/mathlib#15262~~ By Dependent Issues (🤖). Happy coding!

mathlib-dependent-issues-bot avatar Jul 17 '22 15:07 mathlib-dependent-issues-bot