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: completion of the basic ShortComplex.Homology API #7195

Closed
wants to merge 13 commits into from
Closed

[Merged by Bors] - feat: completion of the basic ShortComplex.Homology API #7195

wants to merge 13 commits into from

Conversation

joelriou
Copy link
Collaborator

@joelriou joelriou commented Sep 15, 2023 •
edited by riccardobrasca
Loading

This PR marks the completion of the file Algebra.Homology.ShortComplex.Homology. It adds various API definitions and lemmas, including a comparison of the homology in a category and its opposite category.

Open in Gitpod

@joelriou joelriou added the t-category-theory Category theory label Sep 15, 2023
@joelriou joelriou mentioned this pull request Sep 15, 2023
Open
joelriou and others added 4 commits September 15, 2023 16:11
@joelriou @github-actions
Update Mathlib/Algebra/Homology/ShortComplex/Homology.lean
ec3f806 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@joelriou @github-actions
Update Mathlib/Algebra/Homology/ShortComplex/Homology.lean
a1c4e4d 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@joelriou @github-actions
Update Mathlib/Algebra/Homology/ShortComplex/Homology.lean
bd824c4 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@joelriou @github-actions
Update Mathlib/Algebra/Homology/ShortComplex/Homology.lean
3fbbbe7 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Sep 15, 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 merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Sep 18, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) labels Sep 19, 2023
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

riccardobrasca
riccardobrasca reviewed Sep 19, 2023
View reviewed changes
Copy link
Member

@riccardobrasca riccardobrasca left a comment

Choose a reason for hiding this comment

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

This file is getting quite long... do you plan to add a lot of other stuff? In this case we can maybe split it.

Mathlib/Algebra/Homology/ShortComplex/Homology.lean Show resolved Hide resolved
Mathlib/Algebra/Homology/ShortComplex/Homology.lean
S.op.leftHomologyIso.symm ≪≫ S.leftHomologyOpIso ≪≫ S.rightHomologyIso.symm.op

@[simp]
lemma homologyMap'_op : (homologyMap' φ h₁ h₂).op =
Copy link
Member

Choose a reason for hiding this comment

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

I am not sure, but is the RHS in this and the following lemma really simpler than the LHS? Asking because there is op on both side.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Thanks. I have just removed these simp attributes. (I had probably put these attributes in order to automatize a proof in the definition of homologyFunctorOpNatIso.)

Mathlib/Algebra/Homology/ShortComplex/Homology.lean Show resolved Hide resolved
Mathlib/Algebra/Homology/ShortComplex/Homology.lean Outdated Show resolved Hide resolved
Mathlib/Algebra/Homology/ShortComplex/Homology.lean Outdated Show resolved Hide resolved
@riccardobrasca
Copy link
Member

LGTM, thanks!

bors d+

@bors
Copy link

bors bot commented Sep 19, 2023

✌️ joelriou can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@joelriou
Copy link
Collaborator Author

Thanks @riccardobrasca for your suggestions, which I have mostly followed.

I do not intend to add any more material to this file. With this PR, the three large files LeftHomology.lean, RightHomology.lean and Homology.lean shall be exactly as they are in my dev branch #4197, and these are the only three files that shall be >1000 lines long in this directory.

Next, I plan to develop a little bit more PreservesHomology.lean (following #7197) before I return to Exact.lean (following #7052).

@joelriou
Copy link
Collaborator Author

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Sep 19, 2023
bors bot pushed a commit that referenced this pull request Sep 19, 2023
@joelriou
feat: completion of the basic ShortComplex.Homology API (#7195)
6af751e 
This PR marks the completion of the file `Algebra.Homology.ShortComplex.Homology`. It adds various API definitions and lemmas, including a comparison of the homology in a category and its opposite category.



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
@bors
Copy link

bors bot commented Sep 19, 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: completion of the basic ShortComplex.Homology API [Merged by Bors] - feat: completion of the basic ShortComplex.Homology API Sep 19, 2023
@bors bors bot closed this Sep 19, 2023
@bors bors bot deleted the shortcomplex_homology8 branch September 19, 2023 14:59
kodyvajjha pushed a commit that referenced this pull request Sep 22, 2023
@joelriou @kodyvajjha
feat: completion of the basic ShortComplex.Homology API (#7195)
62c9575 
This PR marks the completion of the file `Algebra.Homology.ShortComplex.Homology`. It adds various API definitions and lemmas, including a comparison of the homology in a category and its opposite category.



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@github-actions github-actions[bot] github-actions[bot] left review comments

@riccardobrasca riccardobrasca riccardobrasca left review comments

Assignees
No one assigned
Labels
delegated 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.
3 participants
@joelriou @leanprover-community-mathlib4-bot @riccardobrasca