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(category_theory/abelian): definition of projective object #7108

Closed
wants to merge 9 commits into from
Closed

[Merged by Bors] - feat(category_theory/abelian): definition of projective object #7108

wants to merge 9 commits into from

Conversation

semorrison
Copy link
Collaborator

@semorrison semorrison commented Apr 8, 2021 •
edited by TwoFX

This is extracted from @TwoFX's projective branch, with some slight tweaks (make things Prop valued classes), and documentation.

This is just the definition of projective and enough_projectives, with no attempt to construct projective resolutions. I want this in place because constructing projective resolutions will hopefully be a good test of experiments with chain complexes.

Co-authored-by: Markus Himmel markus@himmel-villmar.de

Open in Gitpod

@github-actions github-actions bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Apr 8, 2021
@semorrison semorrison mentioned this pull request Apr 8, 2021
Closed
2 tasks
@semorrison semorrison mentioned this pull request Apr 8, 2021
Closed
2 tasks
@semorrison @TwoFX
Update src/category_theory/abelian/projective.lean
23c77e6 
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
@TwoFX
Copy link
Member

TwoFX commented Apr 8, 2021 •
edited

If someone can come up with better names than over, left, π and d, I'd be very happy to hear them.

@semorrison
Copy link
Collaborator Author

If someone can come up with better names than over, left, π and d, I'd be very happy to hear them.

At first I was dubious, but when you think over them written out as projective.over X, projective.π X and projective.left f they seem much more understandable. projective.d is still unhelpful. :-)

@github-actions github-actions bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Apr 8, 2021
@github-actions
Copy link

github-actions bot commented Apr 8, 2021

🎉 Great news! Looks like all the dependencies have been resolved:

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

@semorrison semorrison added the awaiting-review The author would like community review of the PR label Apr 10, 2021
b-mehta
b-mehta approved these changes Apr 13, 2021
View reviewed changes
Copy link
Collaborator

@b-mehta b-mehta left a comment

Choose a reason for hiding this comment

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

I'm not super familiar with projective objects in abelian categories but this looks good to me - any comments @jcommelin?

@TwoFX
Copy link
Member

TwoFX commented Apr 14, 2021

It is occasionally useful to consider variants of projectivity where we require factoring through some class of morphisms other than epimorphisms. Perhaps it would be nice to have some sort of projective_for such that the current definition of projectivity is recovered as projective_for epi. I'm not sure how easy it is to set up something like this with very little boilerplate, so I don't mind merging the current PR and experimenting with generalisations later.

@TwoFX TwoFX requested a review from jcommelin April 19, 2021 19:57
@jcommelin
Copy link
Member

I agree that projective_for will probably become useful at some point in the future.

jcommelin
jcommelin approved these changes Apr 20, 2021
View reviewed changes
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

@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 Apr 20, 2021
bors bot pushed a commit that referenced this pull request Apr 20, 2021
@semorrison
feat(category_theory/abelian): definition of projective object (#7108)
5e188d2 
This is extracted from @TwoFX's `projective` branch, with some slight tweaks (make things `Prop` valued classes), and documentation.

This is just the definition of `projective` and `enough_projectives`, with no attempt to construct projective resolutions. I want this in place because constructing projective resolutions will hopefully be a good test of experiments with chain complexes.

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link

bors bot commented Apr 20, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(category_theory/abelian): definition of projective object [Merged by Bors] - feat(category_theory/abelian): definition of projective object Apr 20, 2021
@bors bors bot closed this Apr 20, 2021
@bors bors bot deleted the projective_defs branch April 20, 2021 09:13
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@TwoFX TwoFX TwoFX left review comments

@jcommelin jcommelin jcommelin approved these changes

@b-mehta b-mehta b-mehta approved these changes

Assignees
No one assigned
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
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@semorrison @TwoFX @jcommelin @b-mehta