Skip to content

[Merged by Bors] - feat: ind-objects are closed under products#18988

Closed
TwoFX wants to merge 17 commits intomasterfrom
markus-ipc
Closed

[Merged by Bors] - feat: ind-objects are closed under products#18988
TwoFX wants to merge 17 commits intomasterfrom
markus-ipc

Conversation

@TwoFX
Copy link
Copy Markdown
Member

@TwoFX TwoFX commented Nov 13, 2024 •
edited
Loading

@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 13, 2024 •
edited
Loading

PR summary cc30156f52

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct (new file) 566
Mathlib.CategoryTheory.Limits.Indization.Products (new file) 614

Declarations diff

+ IsIPC
+ Types.isIso_colimitPointwiseProductToProductColimit
+ coconePointwiseProduct
+ colimitPointwiseProductToProductColimit
+ colimitPointwiseProductToProductColimit_app
+ instance : IsIPC.{u} (Type u)
+ instance [HasProducts.{w} C] [HasFilteredColimitsOfSize.{w, w} C] [IsIPC.{w} C] {D : Type u₁}
+ isIndObject_limit_of_discrete
+ isIndObject_limit_of_discrete_of_hasLimitsOfShape
+ isIndObject_pi
+ pointwiseProduct
+ pointwiseProductCompEvaluation
+ ι_colimitPointwiseProductToProductColimit_π

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.

No changes to technical debt.

You can run this locally as

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

@github-actions github-actions bot added the t-category-theory Category theory label Nov 13, 2024
@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 Nov 13, 2024
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Nov 13, 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 13, 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 14, 2024
joelriou
joelriou reviewed Nov 25, 2024
View reviewed changes
@joelriou joelriou added the WIP Work in progress label Nov 25, 2024
@TwoFX TwoFX removed the WIP Work in progress label Nov 25, 2024
@TwoFX
Copy link
Copy Markdown
Member Author

TwoFX commented Nov 25, 2024

@joelriou I assume you put WIP instead of awaiting-author by accident, or was that deliberate?

@joelriou
Copy link
Copy Markdown
Contributor

joelriou commented Nov 27, 2024

Thanks!

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Nov 27, 2024
mathlib-bors bot pushed a commit that referenced this pull request Nov 27, 2024
@TwoFX
feat: ind-objects are closed under products (#18988)
c59545b 
Co-authored-by: Markus Himmel <markus@lean-fro.org>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 27, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: ind-objects are closed under products [Merged by Bors] - feat: ind-objects are closed under products Nov 27, 2024
@mathlib-bors mathlib-bors bot closed this Nov 27, 2024
@mathlib-bors mathlib-bors bot deleted the markus-ipc branch November 27, 2024 10:39
@TwoFX TwoFX mentioned this pull request Jan 6, 2025
Closed
mathlib-bors bot pushed a commit that referenced this pull request Jan 6, 2025
@TwoFX
feat(CategoryTheory): products in the category of Ind-objects (#20507)
3279a44 
Follow-up to #18988.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@joelriou joelriou joelriou left review comments

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.

4 participants

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