Skip to content

[Merged by Bors] - feat(CategoryTheory/SmallObject/Iteration): the unique morphism (bot and succ cases)#18127

Closed
joelriou wants to merge 13 commits intomasterfrom
small-object-5
Closed

[Merged by Bors] - feat(CategoryTheory/SmallObject/Iteration): the unique morphism (bot and succ cases)#18127
joelriou wants to merge 13 commits intomasterfrom
small-object-5

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Oct 23, 2024 •
edited by alreadydone
Loading

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

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

PR summary b9018760c7

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.CategoryTheory.SmallObject.Iteration.UniqueHom 417

Declarations diff

+ mkOfBot
+ mkOfSucc
+ mkOfSuccNatTrans
+ mkOfSuccNatTransApp
+ mkOfSuccNatTransApp_eq_of_le
+ mkOfSuccNatTransApp_succ_eq

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 the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 23, 2024
joelriou and others added 2 commits October 23, 2024 17:28
@joelriou @github-actions
Update Mathlib.lean
9a2e020 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@joelriou
fix Mathlib.lean
f497043
@joelriou joelriou changed the title feat(CategoryTheory/SmallObject): construction of a morphism between two "iterations" of a functor in two cases feat(CategoryTheory/SmallObject/Iteration): the unique morphism (bot and succ cases) Oct 23, 2024
@joelriou joelriou mentioned this pull request Oct 23, 2024
Closed
2 tasks
@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 25, 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 26, 2024
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 27, 2024
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Oct 27, 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 27, 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 27, 2024
@joelriou joelriou removed the WIP Work in progress label Oct 28, 2024
TwoFX
TwoFX approved these changes Nov 10, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@TwoFX TwoFX 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 d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 10, 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 Nov 10, 2024
@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Nov 10, 2024

Thanks!

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Nov 10, 2024
mathlib-bors bot pushed a commit that referenced this pull request Nov 10, 2024
@joelriou
feat(CategoryTheory/SmallObject/Iteration): the unique morphism (bot …
9041e9d 
…and succ cases) (#18127)




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

mathlib-bors bot commented Nov 10, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(CategoryTheory/SmallObject/Iteration): the unique morphism (bot and succ cases) [Merged by Bors] - feat(CategoryTheory/SmallObject/Iteration): the unique morphism (bot and succ cases) Nov 10, 2024
@mathlib-bors mathlib-bors bot closed this Nov 10, 2024
@mathlib-bors mathlib-bors bot deleted the small-object-5 branch November 10, 2024 22:37
Jun2M pushed a commit that referenced this pull request Nov 17, 2024
@joelriou @Jun2M
feat(CategoryTheory/SmallObject/Iteration): the unique morphism (bot …
1ccadaf 
…and succ cases) (#18127)




Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
TobiasLeichtfried pushed a commit that referenced this pull request Nov 21, 2024
@joelriou @TobiasLeichtfried
feat(CategoryTheory/SmallObject/Iteration): the unique morphism (bot …
2786423 
…and succ cases) (#18127)




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

@TwoFX TwoFX TwoFX approved these changes

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). 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.

4 participants

@joelriou @mathlib4-dependent-issues-bot @TwoFX @leanprover-community-bot-assistant