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(CategoryTheory): more properties of exact sequences #8159

Closed
wants to merge 25 commits into from

Conversation

joelriou
Copy link
Collaborator

@joelriou joelriou commented Nov 3, 2023

The basic API of exact sequences in developed in this PR. As a result, the snake lemma can be formulated as a 6-term exact sequence.


Open in Gitpod

@joelriou joelriou added WIP Work in progress t-category-theory Category theory labels Nov 3, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Nov 3, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) labels Nov 10, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 10, 2023
@joelriou joelriou added awaiting-review and removed WIP Work in progress labels Nov 11, 2023
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Nov 13, 2023
mathlib-bors bot pushed a commit that referenced this pull request Nov 13, 2023
The basic API of exact sequences in developed in this PR. As a result, the snake lemma can be formulated as a 6-term exact sequence.
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Nov 13, 2023

Build failed (retrying...):

mathlib-bors bot pushed a commit that referenced this pull request Nov 13, 2023
The basic API of exact sequences in developed in this PR. As a result, the snake lemma can be formulated as a 6-term exact sequence.
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Nov 13, 2023

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(CategoryTheory): more properties of exact sequences [Merged by Bors] - feat(CategoryTheory): more properties of exact sequences Nov 13, 2023
@mathlib-bors mathlib-bors bot closed this Nov 13, 2023
@mathlib-bors mathlib-bors bot deleted the exact-sequence2 branch November 13, 2023 11:08
alexkeizer pushed a commit that referenced this pull request Nov 17, 2023
The basic API of exact sequences in developed in this PR. As a result, the snake lemma can be formulated as a 6-term exact sequence.
alexkeizer pushed a commit that referenced this pull request Nov 21, 2023
The basic API of exact sequences in developed in this PR. As a result, the snake lemma can be formulated as a 6-term exact sequence.
grunweg pushed a commit that referenced this pull request Dec 15, 2023
The basic API of exact sequences in developed in this PR. As a result, the snake lemma can be formulated as a 6-term exact sequence.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
ready-to-merge This PR has been sent to bors. t-category-theory Category theory
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants