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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(RingTheory/Flat): a module is flat iff tensoring preserves exact sequences #14482

Closed
wants to merge 18 commits into from
Closed

[Merged by Bors] - feat(RingTheory/Flat): a module is flat iff tensoring preserves exact sequences #14482

wants to merge 18 commits into from

Conversation

jjaassoonn
Copy link
Collaborator

@jjaassoonn jjaassoonn commented Jul 6, 2024 •
edited
Loading

@github-actions GitHub Actions
Copy link

github-actions bot commented Jul 6, 2024 •
edited
Loading

PR summary 3e25c552db

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.RingTheory.Flat.CategoryTheory 1508

Declarations diff

+ iff_lTensor_preserves_shortComplex_exact
+ iff_rTensor_preserves_shortComplex_exact
+ lTensor_shortComplex_exact
+ rTensor_shortComplex_exact

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

@jjaassoonn jjaassoonn requested a review from adamtopaz July 6, 2024 18:07
@jjaassoonn jjaassoonn added awaiting-review awaiting-CI t-algebra Algebra (groups, rings, fields, etc) t-category-theory Category theory labels Jul 6, 2024
@joelriou joelriou added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Jul 6, 2024
@jjaassoonn jjaassoonn added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 8, 2024
@jjaassoonn jjaassoonn requested a review from joelriou July 8, 2024 04:10
@jjaassoonn
Copy link
Collaborator Author

!bench

@jjaassoonn jjaassoonn requested a review from kbuzzard July 8, 2024 04:20
@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 32ba554.
The entire run failed.
Found no significant differences.

@jjaassoonn
Copy link
Collaborator Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 32f3feb.
There were no significant changes against commit 06352df.

@joelriou joelriou added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Jul 8, 2024
@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 Jul 8, 2024
@jjaassoonn jjaassoonn added awaiting-CI and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 12, 2024
@jjaassoonn jjaassoonn changed the title feat(RingTheory/Flat): a module is flat iff tensoring preserves finite limits feat(RingTheory/Flat): a module is flat iff tensoring preserves exact sequences Jul 12, 2024
@jjaassoonn jjaassoonn removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Jul 12, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

@joelriou joelriou added the awaiting-author A reviewer has asked the author a question or requested changes label Jul 12, 2024
@jjaassoonn jjaassoonn removed the awaiting-author A reviewer has asked the author a question or requested changes label Jul 13, 2024
@joelriou
Copy link
Collaborator

Thanks!

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Jul 13, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 13, 2024
@jjaassoonn
feat(RingTheory/Flat): a module is flat iff tensoring preserves exact…
79741db 
… sequences (#14482)
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jul 13, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(RingTheory/Flat): a module is flat iff tensoring preserves exact sequences [Merged by Bors] - feat(RingTheory/Flat): a module is flat iff tensoring preserves exact sequences Jul 13, 2024
@mathlib-bors mathlib-bors bot closed this Jul 13, 2024
@mathlib-bors mathlib-bors bot deleted the zjj/flat_exact_cat branch July 13, 2024 20:15
@adomani adomani mentioned this pull request Aug 1, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@joelriou joelriou joelriou left review comments

@adamtopaz adamtopaz Awaiting requested review from adamtopaz

@kbuzzard kbuzzard Awaiting requested review from kbuzzard

Assignees
No one assigned
Labels
ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc) t-category-theory Category theory
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@jjaassoonn @leanprover-bot @leanprover-community-mathlib4-bot @joelriou