Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - feat(category_theory/abelian/*): functors that preserve finite limits and colimits preserve exactness #14581

Closed
wants to merge 19 commits into from

Conversation

jjaassoonn
Copy link
Collaborator

@jjaassoonn jjaassoonn commented Jun 6, 2022

If $F$ is a functor between two abelian categories which preserves limits and colimits, then it preserves exactness.


Open in Gitpod

@jjaassoonn jjaassoonn added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. labels Jun 6, 2022
@jjaassoonn jjaassoonn removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Jun 6, 2022
src/category_theory/abelian/exact.lean Outdated Show resolved Hide resolved
src/category_theory/abelian/exact.lean Outdated Show resolved Hide resolved
src/category_theory/abelian/exact.lean Outdated Show resolved Hide resolved
src/category_theory/abelian/basic.lean Outdated Show resolved Hide resolved
src/category_theory/abelian/basic.lean Outdated Show resolved Hide resolved
@TwoFX TwoFX added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jun 10, 2022
jjaassoonn and others added 4 commits June 13, 2022 11:36
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
@jjaassoonn jjaassoonn added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jun 16, 2022
@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jun 18, 2022
@jjaassoonn jjaassoonn added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jun 20, 2022
@TwoFX TwoFX added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jul 10, 2022
@jjaassoonn jjaassoonn added awaiting-CI The author would like to see what CI has to say before doing more work. awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 10, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Jul 10, 2022
@TwoFX
Copy link
Member

TwoFX commented Jul 11, 2022

Thanks! bors r+

@kmill
Copy link
Collaborator

kmill commented Jul 14, 2022

bors r+

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Jul 14, 2022
bors bot pushed a commit that referenced this pull request Jul 14, 2022
… and colimits preserve exactness (#14581)

If $F$ is a functor between two abelian categories which preserves limits and colimits, then it preserves exactness.
@bors
Copy link

bors bot commented Jul 14, 2022

Build failed:

@jjaassoonn
Copy link
Collaborator Author

bors r+

Thank you for approving this PR, but the build failed last time, now everything is fixed and I am getting green marks everywhere. Could you please approve it again. Thanks!

@kmill
Copy link
Collaborator

kmill commented Jul 15, 2022

Let's try again!

bors r+

bors bot pushed a commit that referenced this pull request Jul 15, 2022
… and colimits preserve exactness (#14581)

If $F$ is a functor between two abelian categories which preserves limits and colimits, then it preserves exactness.
@bors
Copy link

bors bot commented Jul 15, 2022

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Jul 15, 2022
… and colimits preserve exactness (#14581)

If $F$ is a functor between two abelian categories which preserves limits and colimits, then it preserves exactness.
@bors
Copy link

bors bot commented Jul 15, 2022

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Jul 15, 2022
… and colimits preserve exactness (#14581)

If $F$ is a functor between two abelian categories which preserves limits and colimits, then it preserves exactness.
@bors
Copy link

bors bot commented Jul 15, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(category_theory/abelian/*): functors that preserve finite limits and colimits preserve exactness [Merged by Bors] - feat(category_theory/abelian/*): functors that preserve finite limits and colimits preserve exactness Jul 15, 2022
@bors bors bot closed this Jul 15, 2022
@bors bors bot deleted the jjaassoonn/preserves_exact branch July 15, 2022 10:49
joelriou pushed a commit that referenced this pull request Jul 23, 2022
… and colimits preserve exactness (#14581)

If $F$ is a functor between two abelian categories which preserves limits and colimits, then it preserves exactness.
bors bot pushed a commit that referenced this pull request Aug 8, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

4 participants