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

feat(category_theory/*/injective): definition of injective objects #11878

Closed
wants to merge 22 commits into from
Closed

feat(category_theory/*/injective): definition of injective objects #11878

wants to merge 22 commits into from

Conversation

jjaassoonn
Copy link
Collaborator

@jjaassoonn jjaassoonn commented Feb 6, 2022 •
edited

In this branch, I attempt to define injective objects. Some basic properties and examples are provided as well, for example:

  • zero object is injective
  • category of types has enough injectives
  • injective objects is dual to projective objects
  • injective resolutions
  • trivial injective resolutions for injective object
  • injective resolutions are homotopically equivalent
  • taking injective resolutions is functorial
  • etc.

These files are almost in one to one correspodence to projective.lean and projective_resolution.lean.

Open in Gitpod

@jcommelin jcommelin changed the title feat(category_theory/*/injective.lean) : definition of injective objects feat(category_theory/*/injective.lean): definition of injective objects Feb 7, 2022
@jcommelin jcommelin changed the title feat(category_theory/*/injective.lean): definition of injective objects feat(category_theory/*/injective): definition of injective objects Feb 7, 2022
@jjaassoonn jjaassoonn added this to In progress in Homological algebra via automation Feb 7, 2022
@jjaassoonn jjaassoonn added the WIP Work in progress label Feb 8, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Mar 4, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Mar 5, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Mar 5, 2022
@jjaassoonn
Copy link
Collaborator Author

This pr is now obsolete because other it has been splitted and merged into mathlib. Everything remaining is now
#12810. So I will close this pr.

@jjaassoonn jjaassoonn closed this Mar 20, 2022
@jjaassoonn jjaassoonn deleted the injectives branch June 8, 2022 11:13
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin left review comments

@kbuzzard kbuzzard kbuzzard left review comments

Assignees
No one assigned
Labels
merge-conflict Please `git merge origin/master` then a bot will remove this label. WIP Work in progress
Projects
Homological algebra
  
In progress
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@jjaassoonn @jcommelin @kbuzzard @leanprover-community-bot-assistant