Skip to content

feat(CategoryTheory): pseudofunctors to Cat#24384

Closed
joelriou wants to merge 10 commits intomasterfrom
pseudofunctor-mapcomp-prime-cat
Closed

feat(CategoryTheory): pseudofunctors to Cat#24384
joelriou wants to merge 10 commits intomasterfrom
pseudofunctor-mapcomp-prime-cat

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Apr 26, 2025 •
edited
Loading

We specialize the API from PR #24382 to the case of pseudofunctors to Cat.

Co-authored-by: Christian Merten christian@merten.dev

Open in Gitpod

@joelriou joelriou added the t-category-theory Category theory label Apr 26, 2025
@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 Apr 26, 2025
@joelriou joelriou mentioned this pull request Apr 26, 2025
Closed
2 tasks
@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 26, 2025 •
edited
Loading

PR summary db52f0992d

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.CategoryTheory.Bicategory.Functor.Cat (new file) 367

Declarations diff

+ mapComp'_comp_id_hom_app
+ mapComp'_comp_id_inv_app
+ mapComp'_hom_app_comp_mapComp'_hom_app_map_obj
+ mapComp'_hom_app_comp_map_map_mapComp'_hom_app
+ mapComp'_hom_naturality
+ mapComp'_id_comp_hom_app
+ mapComp'_id_comp_inv_app
+ mapComp'_inv_app_comp_mapComp'_hom_app
+ mapComp'_inv_app_map_obj_comp_mapComp'_inv_app
+ mapComp'_inv_naturality
+ mapComp'_naturality_1
+ mapComp'_naturality_2
+ mapComp'₀₁₃_hom_app
+ mapComp'₀₁₃_inv_app
+ mapId'_hom_naturality
+ mapId'_inv_naturality
+ map_map_mapComp'_inv_app_comp_mapComp'_inv_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.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

This was referenced Apr 28, 2025
Open
Closed
callesonne
callesonne reviewed Jun 7, 2025
View reviewed changes
Mathlib/CategoryTheory/Bicategory/Functor/Cat.lean
Comment on lines +92 to +106
lemma mapComp'_comp_id_hom_app :
(F.mapComp' f (𝟙 b₁) f).hom.app X = (F.mapId b₁).inv.app ((F.map f).obj X) := by
simp [mapComp'_comp_id]

lemma mapComp'_comp_id_inv_app :
(F.mapComp' f (𝟙 b₁) f).inv.app X = (F.mapId b₁).hom.app ((F.map f).obj X) := by
simp [mapComp'_comp_id]

lemma mapComp'_id_comp_hom_app :
(F.mapComp' (𝟙 b₀) f f).hom.app X = (F.map f).map ((F.mapId b₀).inv.app X) := by
simp [mapComp'_id_comp]

lemma mapComp'_id_comp_inv_app :
(F.mapComp' (𝟙 b₀) f f).inv.app X = (F.map f).map ((F.mapId b₀).hom.app X) := by
simp [mapComp'_id_comp]
Copy link
Copy Markdown
Collaborator

@callesonne callesonne Jun 7, 2025 •
edited
Loading

Choose a reason for hiding this comment

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

FYI, I have written an attribute to deal with this exact situation! Tagging a lemma, which is an equality between two 2-morphisms, with @[to_app] automatically adds a new lemma that specializes the Bicategory where the equality is taking place to Cat, applies NatTrans.app on both sides and peforms some basic simplification. Then name of the new lemma will then be old_name_app. I wrote this because I was also dealing with Pseudofunctors to Cat when making some progress on 2-Yoneda. So I think if you stated these lemmas as mapComp'_comp_id_hom in the Strict file, you would get these for free by tagging it with @[to_app].

Copy link
Copy Markdown
Collaborator

@callesonne callesonne Jun 7, 2025 •
edited
Loading

Choose a reason for hiding this comment

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

So in theory, this file should (maybe?) not need to exist, as you can prove all these lemmas for (strict?) bicategories and tag it with @[to_app]. Although the point of making that attribute was to save time, I am not sure if there is any point in making you rewrite these lemmas for strict bicategories just to be able to tag them with @[to_app]...

Copy link
Copy Markdown
Collaborator

@callesonne callesonne Jun 8, 2025

Choose a reason for hiding this comment

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

So in other words, what I think you should do is add hom/inv lemmas to the strict file and tag these with @[to_app].

Copy link
Copy Markdown
Contributor Author

@joelriou joelriou Jun 18, 2025 •
edited
Loading

Choose a reason for hiding this comment

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

Thanks for this attribute! However, in other to get suitable lemmas, I had to add a few lemmas #25971 in the simp set to take into account that associators and unitors induce identities.

Copy link
Copy Markdown
Collaborator

@callesonne callesonne Jun 18, 2025

Choose a reason for hiding this comment

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

Thanks! Yes I imagined this simp-set was incomplete, and would be added to once people start using the attribute.

@callesonne callesonne added the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 7, 2025
@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 Jun 16, 2025
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Jun 16, 2025

This PR/issue depends on:

@joelriou joelriou mentioned this pull request Jun 16, 2025
Closed
1 task
@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Jun 16, 2025

This PR has been migrated to a fork-based workflow: #25971

@joelriou joelriou closed this Jun 16, 2025
@YaelDillies YaelDillies deleted the pseudofunctor-mapcomp-prime-cat branch August 18, 2025 07:31
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

1 more reviewer

@callesonne callesonne callesonne left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

awaiting-author A reviewer has asked the author a question or requested changes. migrated-to-fork t-category-theory Category theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@joelriou @mathlib4-dependent-issues-bot @callesonne