[Merged by Bors] - feat(CategoryTheory): pseudofunctors from strict bicategories by joelriou · Pull Request #24382 · leanprover-community/mathlib4

joelriou · 2025-04-26T08:22:23Z

This PR provides an API for pseudofunctors F from a strict bicategory B. In particular, this shall apply to pseudofunctors from locally discrete bicategories.

We first introduce more flexible variants of mapId and mapComp: for example, if f and g are composable morphisms and fg is such that h : fg = f ≫ f, we provide an isomorphism F.mapComp' f g fg h : F.map fg ≅ F.map f ≫ F.map g. We study the compatibilities of these isomorphisms with respect to composition with identities and associativity.

Secondly, given a commutative square t ≫ r = l ≫ b in B, we construct an isomorphism F.map t ≫ F.map r ≅ F.map l ≫ F.map b.

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

github-actions · 2025-04-26T08:23:23Z

PR summary a4ec7db301

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.CategoryTheory.Bicategory.Functor.Strict` (new file)	360

Declarations diff

+ isoMapOfCommSq
+ isoMapOfCommSq_eq
+ isoMapOfCommSq_horiz_id
+ isoMapOfCommSq_vert_id
+ mapComp'
+ mapComp'_comp_id
+ mapComp'_eq_mapComp
+ mapComp'_hom_comp_mapComp'_hom_whiskerRight
+ mapComp'_hom_comp_whiskerLeft_mapComp'_hom
+ mapComp'_id_comp
+ mapComp'_inv_comp_mapComp'_hom
+ mapComp'_inv_whiskerRight_comp_mapComp'_inv
+ mapId'
+ mapId'_eq_mapId
+ whiskerLeft_mapComp'_inv_comp_mapComp'_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.

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

erdOne

Do you think .hom and .inv simp lemmas are useful here?

Mathlib/CategoryTheory/Bicategory/Functor/Strict.lean

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

joelriou · 2025-05-01T21:19:50Z

Do you think .hom and .inv simp lemmas are useful here?

If the remark applies to mapComp'_comp_id and mapComp'_id_comp, I do not think we need _hom/_inv versions, as it seems very unlikely that we would need to apply these lemmas in the backwards direction. The situation is different for the associativity lemmas because they relate four different mapComp' isomorphisms.

Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean

Mathlib/CategoryTheory/Bicategory/Functor/Strict.lean

Co-authored-by: Calle Sönne <calle.sonne@gmail.com>

joelriou · 2025-05-11T10:12:18Z

Thanks @callesonne and @erdOne for the reviews!

Mathlib/CategoryTheory/Bicategory/Functor/Strict.lean

callesonne

LGTM!

Mathlib/CategoryTheory/Bicategory/Functor/Strict.lean

callesonne · 2025-06-07T17:03:24Z

@erdOne do you want to maintainer merge this?

erdOne

Thanks!
maintainer merge

github-actions · 2025-06-07T22:21:07Z

🚀 Pull request has been placed on the maintainer queue by erdOne.

jcommelin · 2025-06-16T06:49:11Z

Thanks 🎉

bors merge

This PR provides an API for pseudofunctors `F` from a strict bicategory `B`. In particular, this shall apply to pseudofunctors from locally discrete bicategories. We first introduce more flexible variants of `mapId` and `mapComp`: for example, if `f` and `g` are composable morphisms and `fg` is such that `h : fg = f ≫ f`, we provide an isomorphism `F.mapComp' f g fg h : F.map fg ≅ F.map f ≫ F.map g`. We study the compatibilities of these isomorphisms with respect to composition with identities and associativity. Secondly, given a commutative square `t ≫ r = l ≫ b` in `B`, we construct an isomorphism `F.map t ≫ F.map r ≅ F.map l ≫ F.map b`. Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

mathlib-bors · 2025-06-16T07:16:48Z

Pull request successfully merged into master.

Build succeeded:

CI Success

…over-community#24382) This PR provides an API for pseudofunctors `F` from a strict bicategory `B`. In particular, this shall apply to pseudofunctors from locally discrete bicategories. We first introduce more flexible variants of `mapId` and `mapComp`: for example, if `f` and `g` are composable morphisms and `fg` is such that `h : fg = f ≫ f`, we provide an isomorphism `F.mapComp' f g fg h : F.map fg ≅ F.map f ≫ F.map g`. We study the compatibilities of these isomorphisms with respect to composition with identities and associativity. Secondly, given a commutative square `t ≫ r = l ≫ b` in `B`, we construct an isomorphism `F.map t ≫ F.map r ≅ F.map l ≫ F.map b`. Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

feat(CategoryTheory): pseudofunctors from strict bicategories

4913881

joelriou added the t-category-theory Category theory label Apr 26, 2025

joelriou added 3 commits April 26, 2025 10:25

better names

430466b

cleaning up

6d3eca6

whitespace

74dc8c5

joelriou added the WIP Work in progress label Apr 26, 2025

cleaning up

6529163

joelriou removed the WIP Work in progress label Apr 26, 2025

joelriou mentioned this pull request Apr 26, 2025

feat(CategoryTheory): (co)descent data for a pseudofunctor #24327

Closed

2 tasks

joelriou added the WIP Work in progress label Apr 26, 2025

better lemmas

45d4532

joelriou removed the WIP Work in progress label Apr 26, 2025

joelriou mentioned this pull request Apr 26, 2025

feat(CategoryTheory): pseudofunctors to Cat #24384

Closed

1 task

erdOne requested a review from callesonne April 27, 2025 11:52

erdOne reviewed Apr 27, 2025

View reviewed changes

Mathlib/CategoryTheory/Bicategory/Functor/Strict.lean Outdated Show resolved Hide resolved

Mathlib/CategoryTheory/Bicategory/Functor/Strict.lean Outdated Show resolved Hide resolved

Mathlib/CategoryTheory/Bicategory/Functor/Strict.lean Outdated Show resolved Hide resolved

erdOne reviewed Apr 27, 2025

View reviewed changes

Mathlib/CategoryTheory/Bicategory/Functor/Strict.lean Outdated Show resolved Hide resolved

This was referenced Apr 28, 2025

feat(CategoryTheory): effectiveness of descent #24434

Open

feat(CategoryTheory): descent of morphisms for a pseudofunctor #24411

Closed

joelriou and others added 2 commits May 1, 2025 16:52

Update Mathlib/CategoryTheory/Bicategory/Functor/Strict.lean

fcbb711

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Update Mathlib/CategoryTheory/Bicategory/Functor/Strict.lean

c052df6

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label May 1, 2025

joelriou added 2 commits May 1, 2025 22:43

Merge remote-tracking branch 'origin' into pseudofunctor-mapcomp-prime

d1d42ab

moved mapId' and mapComp' to Pseudofunctor.lean

b70c6a4

joelriou removed the awaiting-author A reviewer has asked the author a question or requested changes. label May 1, 2025

callesonne reviewed May 11, 2025

View reviewed changes

Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean Show resolved Hide resolved

Mathlib/CategoryTheory/Bicategory/Functor/Strict.lean Outdated Show resolved Hide resolved

joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label May 11, 2025

joelriou and others added 2 commits May 11, 2025 12:07

Update Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean

d28f9d2

Co-authored-by: Calle Sönne <calle.sonne@gmail.com>

Update Mathlib/CategoryTheory/Bicategory/Functor/Strict.lean

eeb2af6

Co-authored-by: Calle Sönne <calle.sonne@gmail.com>

Merge remote-tracking branch 'origin' into pseudofunctor-mapcomp-prime

c66c05a

joelriou removed the awaiting-author A reviewer has asked the author a question or requested changes. label May 11, 2025

callesonne reviewed May 11, 2025

View reviewed changes

Mathlib/CategoryTheory/Bicategory/Functor/Strict.lean Show resolved Hide resolved

callesonne added the awaiting-author A reviewer has asked the author a question or requested changes. label May 11, 2025

joelriou removed the awaiting-author A reviewer has asked the author a question or requested changes. label May 11, 2025

callesonne reviewed May 11, 2025

View reviewed changes

Mathlib/CategoryTheory/Bicategory/Functor/Strict.lean Show resolved Hide resolved

callesonne approved these changes Jun 7, 2025

View reviewed changes

Mathlib/CategoryTheory/Bicategory/Functor/Strict.lean Show resolved Hide resolved

Mathlib/CategoryTheory/Bicategory/Functor/Strict.lean Show resolved Hide resolved

erdOne reviewed Jun 7, 2025

View reviewed changes

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jun 7, 2025

callesonne mentioned this pull request Jun 8, 2025

feat(Category/Grpd): define the bicategory of groupoids #25561

Open

Merge remote-tracking branch 'origin' into pseudofunctor-mapcomp-prime

22abd26

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Jun 16, 2025

mathlib-bors bot changed the title ~~feat(CategoryTheory): pseudofunctors from strict bicategories~~ [Merged by Bors] - feat(CategoryTheory): pseudofunctors from strict bicategories Jun 16, 2025

mathlib-bors bot closed this Jun 16, 2025

mathlib-bors bot deleted the pseudofunctor-mapcomp-prime branch June 16, 2025 07:16

joelriou mentioned this pull request Oct 3, 2025

[Merged by Bors] - feat(CategoryTheory): prestacks #30177

Closed

2 tasks

Conversation

joelriou commented Apr 26, 2025

Uh oh!

github-actions bot commented Apr 26, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary a4ec7db301

Import changes for modified files

Declarations diff

Uh oh!

erdOne left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

joelriou commented May 1, 2025

Uh oh!

Uh oh!

Uh oh!

joelriou commented May 11, 2025

Uh oh!

Uh oh!

Uh oh!

callesonne left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

callesonne commented Jun 7, 2025

Uh oh!

erdOne left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Jun 7, 2025

Uh oh!

jcommelin commented Jun 16, 2025

Uh oh!

mathlib-bors bot commented Jun 16, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

github-actions bot commented Apr 26, 2025 •

edited

Loading