Skip to content

[Merged by Bors] - feat: (co)products in functor categories#18987

Closed
TwoFX wants to merge 2 commits intomasterfrom
piObjIso
Closed

[Merged by Bors] - feat: (co)products in functor categories#18987
TwoFX wants to merge 2 commits intomasterfrom
piObjIso

Conversation

@TwoFX
Copy link
Copy Markdown
Member

@TwoFX TwoFX commented Nov 13, 2024

Open in Gitpod

@github-actions github-actions bot added the t-category-theory Category theory label Nov 13, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 13, 2024

PR summary 40e036e14b

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products 401

Declarations diff

+ piObjIso
+ piObjIso_hom_comp_π
+ piObjIso_inv_comp_pi
+ sigmaObjIso
+ ι_comp_sigmaObjIso_hom
+ ι_comp_sigmaObjIso_inv

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.

@TwoFX TwoFX mentioned this pull request Nov 13, 2024
Closed
5 tasks
@joelriou
Copy link
Copy Markdown
Contributor

joelriou commented Nov 13, 2024

Thanks!

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Nov 13, 2024
mathlib-bors bot pushed a commit that referenced this pull request Nov 13, 2024
@TwoFX
feat: (co)products in functor categories (#18987)
00a090b 
Co-authored-by: Markus Himmel <markus@lean-fro.org>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 13, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: (co)products in functor categories [Merged by Bors] - feat: (co)products in functor categories Nov 13, 2024
@mathlib-bors mathlib-bors bot closed this Nov 13, 2024
@mathlib-bors mathlib-bors bot deleted the piObjIso branch November 13, 2024 21:59
TobiasLeichtfried pushed a commit that referenced this pull request Nov 21, 2024
@TwoFX @TobiasLeichtfried
feat: (co)products in functor categories (#18987)
ed0badf 
Co-authored-by: Markus Himmel <markus@lean-fro.org>
@TwoFX TwoFX mentioned this pull request Feb 23, 2025
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

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.

2 participants

@TwoFX @joelriou