Skip to content

[Merged by Bors] - feat(CategoryTheory/SmallObject): very basic API for the iteration of functors#18115

Closed
joelriou wants to merge 4 commits intomasterfrom
small-object-4
Closed

[Merged by Bors] - feat(CategoryTheory/SmallObject): very basic API for the iteration of functors#18115
joelriou wants to merge 4 commits intomasterfrom
small-object-4

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Oct 23, 2024 •
edited
Loading

This PR adds some very basic API for the iteration of functors and fixes the notation for intervals (Set.Iic and Set.Iio are now used).

Open in Gitpod

@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 295d8dfd36

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.CategoryTheory.SmallObject.Iteration -412
Mathlib.CategoryTheory.SmallObject.Iteration.Basic 412

Declarations diff

+ congr_app
+ eval
+ natTrans_comp
+ natTrans_id
+ natTrans_naturality
+ restrictionLE
+ restrictionLE_map
+ restrictionLE_obj
+ trunc
+ truncFunctor
+ truncFunctor_map_natTrans_app

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.

@joelriou joelriou mentioned this pull request Oct 23, 2024
Closed
1 task
@joelriou @github-actions
Update Mathlib.lean
9a2e020 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@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
@joelriou joelriou removed the WIP Work in progress label Oct 26, 2024
TwoFX
TwoFX approved these changes Oct 27, 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 r+

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Oct 27, 2024
mathlib-bors bot pushed a commit that referenced this pull request Oct 27, 2024
@joelriou
feat(CategoryTheory/SmallObject): very basic API for the iteration of…
5532a72 
… functors (#18115)

This PR adds some very basic API for the iteration of functors and fixes the notation for intervals (`Set.Iic` and `Set.Iio` are now used).



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

mathlib-bors bot commented Oct 27, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(CategoryTheory/SmallObject): very basic API for the iteration of functors [Merged by Bors] - feat(CategoryTheory/SmallObject): very basic API for the iteration of functors Oct 27, 2024
@mathlib-bors mathlib-bors bot closed this Oct 27, 2024
@mathlib-bors mathlib-bors bot deleted the small-object-4 branch October 27, 2024 15:56
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

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.

3 participants

@joelriou @TwoFX @leanprover-community-bot-assistant