Skip to content

[Merged by Bors] - feat(CategoryTheory/Limits): the end of a functor#18082

Closed
joelriou wants to merge 12 commits intomasterfrom
category-limits-shapes-end
Closed

[Merged by Bors] - feat(CategoryTheory/Limits): the end of a functor#18082
joelriou wants to merge 12 commits intomasterfrom
category-limits-shapes-end

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Oct 22, 2024 •
edited
Loading

In this file, given a functor F : Jᵒᵖ ⥤ J ⥤ C, we define its end end_ F. It is a particular case of multiequalizer. The abbreviation Wedge for the corresponding category of cones is also introduced.

Open in Gitpod

@joelriou joelriou added WIP Work in progress t-category-theory Category theory labels Oct 22, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 22, 2024 •
edited
Loading

PR summary 06d970de53

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.CategoryTheory.Limits.Shapes.End 417

Declarations diff

+ HasEnd
+ Wedge
+ condition
+ end_
+ end_.condition
+ end_.lift
+ end_.lift_π
+ end_.π
+ lift
+ lift_ι
+ mk
+ mk_ι
+ multicospanIndexEnd
++ hom_ext

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>

The doc-module for script/declarations_diff.sh contains some details about this script.

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Oct 22, 2024
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Oct 24, 2024

This PR/issue depends on:

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 24, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 24, 2024
@joelriou joelriou removed the WIP Work in progress label Oct 28, 2024
@joelriou joelriou mentioned this pull request Oct 29, 2024
Closed
3 tasks
@dagurtomas
Copy link
Copy Markdown
Contributor

dagurtomas commented Oct 29, 2024

Thanks!

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 29, 2024

🚀 Pull request has been placed on the maintainer queue by dagurtomas.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Oct 29, 2024
joelriou
joelriou commented Oct 29, 2024
View reviewed changes
jcommelin
jcommelin reviewed Oct 29, 2024
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.

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 29, 2024

✌️ 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.

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Oct 29, 2024
@joelriou @jcommelin
Update Mathlib/CategoryTheory/Limits/Shapes/End.lean
06d970d 
Co-authored-by: Johan Commelin <johan@commelin.net>
@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Oct 29, 2024

Thanks very much!

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Oct 29, 2024
mathlib-bors bot pushed a commit that referenced this pull request Oct 29, 2024
@joelriou
feat(CategoryTheory/Limits): the end of a functor (#18082)
43e571a 
In this file, given a functor `F : Jᵒᵖ ⥤ J ⥤ C`, we define its end `end_ F`. It is a particular case of multiequalizer. The abbreviation `Wedge` for the corresponding category of cones is also introduced.



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

mathlib-bors bot commented Oct 29, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(CategoryTheory/Limits): the end of a functor [Merged by Bors] - feat(CategoryTheory/Limits): the end of a functor Oct 29, 2024
@mathlib-bors mathlib-bors bot closed this Oct 29, 2024
@mathlib-bors mathlib-bors bot deleted the category-limits-shapes-end branch October 29, 2024 13:45
jcommelin pushed a commit that referenced this pull request Oct 29, 2024
@joelriou @jcommelin
feat(CategoryTheory/Limits): the end of a functor (#18082)
147c666 
In this file, given a functor `F : Jᵒᵖ ⥤ J ⥤ C`, we define its end `end_ F`. It is a particular case of multiequalizer. The abbreviation `Wedge` for the corresponding category of cones is also introduced.



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

@jcommelin jcommelin jcommelin left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. 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.

5 participants

@joelriou @mathlib4-dependent-issues-bot @dagurtomas @jcommelin @leanprover-community-bot-assistant