Skip to content

[Merged by Bors] - feat(CategoryTheory/SmallObject/Iteration): the unique morphism (limit case)#18137

Closed
joelriou wants to merge 19 commits intomasterfrom
small-object-6
Closed

[Merged by Bors] - feat(CategoryTheory/SmallObject/Iteration): the unique morphism (limit case)#18137
joelriou wants to merge 19 commits intomasterfrom
small-object-6

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Oct 23, 2024 •
edited
Loading

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

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

PR summary 24c18055eb

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ instance : Nonempty (iter₁ ⟶ iter₂) := by
+ instance : Unique (iter₁ ⟶ iter₂)
+ iso
+ iso_refl
+ iso_trans
+ mkOfLimit
+ mkOfLimitNatTrans
+ mkOfLimitNatTransApp
+ mkOfLimitNatTransApp_eq_of_lt
+ mkOfLimitNatTransApp_naturality_top

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.

Increase in tech debt: 1.00
Current number Change Type
1555 1 erw

Current commit 24c18055eb
Reference commit 23ecdee3fc

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

@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
@alreadydone alreadydone mentioned this pull request Oct 23, 2024
Closed
@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
alreadydone
alreadydone reviewed Oct 25, 2024
View reviewed changes
@leanprover-community-bot-assistant leanprover-community-bot-assistant 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 Oct 26, 2024
@joelriou @alreadydone
Update Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
ecdbc60 
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Oct 27, 2024

Thanks @alreadydone for the suggestions!

@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
@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 Nov 10, 2024
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Nov 10, 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 Nov 10, 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 Nov 12, 2024
@joelriou joelriou removed the WIP Work in progress label Nov 12, 2024
@joelriou joelriou mentioned this pull request Nov 14, 2024
Closed
1 task
TwoFX
TwoFX approved these changes Nov 14, 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.

Looks good to me, just one question.
bors d+

Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean
Comment on lines +241 to +243
lemma iso_refl : iso iter₁ iter₁ = Iso.refl _ := by aesop_cat

lemma iso_trans : iso iter₁ iter₂ ≪≫ iso iter₂ iter₃ = iso iter₁ iter₃ := by aesop_cat
Copy link
Copy Markdown
Member

@TwoFX TwoFX Nov 14, 2024

Choose a reason for hiding this comment

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

I don't know how the place where you're applying iso_trans looks like, but would it make sense to provide Unique (iter₁ ≅ iter₂) instead (or in addition)?

Copy link
Copy Markdown
Contributor Author

@joelriou joelriou Nov 14, 2024

Choose a reason for hiding this comment

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

Thanks for the suggestion. I will try to see if this idea may help or not in the future downsteam PRs.

@mathlib-bors
Copy link
Copy Markdown
Contributor

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

joelriou commented Nov 14, 2024

Thanks!

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Nov 14, 2024
mathlib-bors bot pushed a commit that referenced this pull request Nov 14, 2024
@joelriou
feat(CategoryTheory/SmallObject/Iteration): the unique morphism (limi…
a692b47 
…t case) (#18137)




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

mathlib-bors bot commented Nov 14, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(CategoryTheory/SmallObject/Iteration): the unique morphism (limit case) [Merged by Bors] - feat(CategoryTheory/SmallObject/Iteration): the unique morphism (limit case) Nov 14, 2024
@mathlib-bors mathlib-bors bot closed this Nov 14, 2024
@mathlib-bors mathlib-bors bot deleted the small-object-6 branch November 14, 2024 20:21
TobiasLeichtfried pushed a commit that referenced this pull request Nov 21, 2024
@joelriou @TobiasLeichtfried
feat(CategoryTheory/SmallObject/Iteration): the unique morphism (limi…
95345cf 
…t case) (#18137)




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

@alreadydone alreadydone alreadydone left review comments

@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.

5 participants

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