Skip to content

[Merged by Bors] - feat: exactness of short complexes#7052

Closed
joelriou wants to merge 3 commits intomasterfrom
shortcomplex_exact
Closed

[Merged by Bors] - feat: exactness of short complexes#7052
joelriou wants to merge 3 commits intomasterfrom
shortcomplex_exact

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Sep 9, 2023 •
edited
Loading

This PR introduces the definition of a proposition S.Exact when S is a short complex.

Open in Gitpod

@joelriou joelriou added the t-category-theory Category theory label Sep 9, 2023
@joelriou joelriou mentioned this pull request Sep 9, 2023
Closed
11 tasks
jcommelin
jcommelin reviewed Sep 14, 2023
View reviewed changes
Copy link
Copy Markdown
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.

Under suitable assumptions, this new definition of exactness is equivalent to the existing one in mathlib. I understand that you plan to phase out the old definition. But in the mean time, I think it is good to provide a "glue" lemma that shows that the two are equivalent.

@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Sep 14, 2023
@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Sep 14, 2023

Thanks for the suggestions! I shall include a comparison lemma with the current Exact f g under suitable assumptions, but I need slightly more basic API (one or two PR on this file) before I can do this.

@joelriou joelriou added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Sep 14, 2023
jcommelin
jcommelin approved these changes Sep 14, 2023
View reviewed changes
Copy link
Copy Markdown
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

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Sep 14, 2023
bors bot pushed a commit that referenced this pull request Sep 14, 2023
@joelriou
feat: exactness of short complexes (#7052)
9a44ef1 
This PR introduces the definition of a proposition `S.Exact` when `S` is a short complex.
@bors
Copy link
Copy Markdown

bors bot commented Sep 14, 2023

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Sep 14, 2023
@joelriou
feat: exactness of short complexes (#7052)
376f2fe 
This PR introduces the definition of a proposition `S.Exact` when `S` is a short complex.
@bors
Copy link
Copy Markdown

bors bot commented Sep 14, 2023

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Sep 14, 2023
@joelriou
feat: exactness of short complexes (#7052)
91c6e24 
This PR introduces the definition of a proposition `S.Exact` when `S` is a short complex.
@bors
Copy link
Copy Markdown

bors bot commented Sep 14, 2023

Build failed:

@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Sep 15, 2023

bors retry

bors bot pushed a commit that referenced this pull request Sep 15, 2023
@joelriou
feat: exactness of short complexes (#7052)
31f3bd8 
This PR introduces the definition of a proposition `S.Exact` when `S` is a short complex.
@bors
Copy link
Copy Markdown

bors bot commented Sep 15, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat: exactness of short complexes [Merged by Bors] - feat: exactness of short complexes Sep 15, 2023
@bors bors bot closed this Sep 15, 2023
@bors bors bot deleted the shortcomplex_exact branch September 15, 2023 09:39
@joelriou joelriou mentioned this pull request Sep 19, 2023
Closed
3 tasks
kodyvajjha pushed a commit that referenced this pull request Sep 22, 2023
@joelriou @kodyvajjha
feat: exactness of short complexes (#7052)
2581dd0 
This PR introduces the definition of a proposition `S.Exact` when `S` is a short complex.
@joelriou joelriou mentioned this pull request Jun 13, 2025
Open
11 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin approved these changes

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-category-theory Category theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@joelriou @jcommelin