Skip to content

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

Open
callesonne wants to merge 9 commits intomasterfrom
calle_groupoid_bicat
Open

feat(Category/Grpd): define the bicategory of groupoids#25561
callesonne wants to merge 9 commits intomasterfrom
calle_groupoid_bicat

Conversation

@callesonne
Copy link
Copy Markdown
Collaborator

@callesonne callesonne commented Jun 7, 2025

Open in Gitpod

@callesonne callesonne added the t-category-theory Category theory label Jun 7, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 7, 2025 •
edited
Loading

PR summary bf1171271a

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.CategoryTheory.Category.Grpd 537 543 +6 (+1.12%)
Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps 1407 1413 +6 (+0.43%)
Import changes for all files
Files Import difference
10 files Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit Mathlib.AlgebraicTopology.FundamentalGroupoid.Product Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected Mathlib.CategoryTheory.Category.Grpd Mathlib.Geometry.Manifold.PoincareConjecture Mathlib.Topology.Homotopy.HomotopyGroup Mathlib.Topology.Homotopy.Lifting
 6
Mathlib.CategoryTheory.Bicategory.Functor.Strict (new file) 356

Declarations diff

+ IsStrict
+ associator_hom_app
+ associator_inv_app
+ bicategory
+ bicategory.strict
+ comp_app
+ comp_eq_comp
+ comp_map
+ comp_obj
+ eqToHom_app
+ forgetToCatIsStrict
+ id_app
+ id_eq_id
+ id_map
+ id_obj
+ leftUnitor_hom_app
+ leftUnitor_inv_app
+ of_α
+ rightUnitor_hom_app
+ rightUnitor_inv_app
+ toFunctor
+ whiskerLeft_app
+ whiskerRight_app
++ natTrans_ext
- hom_to_functor
- id_to_functor

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

@robin-carlier
Copy link
Copy Markdown
Contributor

robin-carlier commented Jun 7, 2025 •
edited
Loading

Cat has a whole lot of simp lemmas (id_obj, comp_obj, etc.) that Grpd doesn’t. Is it an issue? If yes, perhaps now would be a good time to add them as well?

Also (apologies if this is a naive question), given that the homs in Grpd are def-eq with the homs in Cat and that a Grpd instance will infer a Cat instance, are there risks that this design might completely confuse automation?

@callesonne
Copy link
Copy Markdown
Collaborator Author

callesonne commented Jun 7, 2025 •
edited
Loading

Cat has a whole lot of simp lemmas (id_obj, comp_obj, etc.) that Grpd doesn’t. Is it an issue? If yes, perhaps now would be a good time to add them as well?

Also (apologies if this is a naive question), given that the homs in Grpd are def-eq with the homs, in Cat and that a Grpd instance will infer a Cat instance, are there risks that this design might completely confuse automation?

Both very valid comments, thanks! :)

For the second one, yes I think you are right. I just started trying to define the pseudofunctor from Grpd to Cat and I'm running into exactly these issues!

I have added a pseudofunctor from Grpd to Cat (it wasn't that bad in the end), and I think this is how one should move between the two categories to get well-behaved automation.

@callesonne callesonne added awaiting-author A reviewer has asked the author a question or requested changes. WIP Work in progress and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 7, 2025
@callesonne callesonne removed the WIP Work in progress label Jun 7, 2025
@callesonne
Copy link
Copy Markdown
Collaborator Author

callesonne commented Jun 8, 2025

Once #24382 is merged (which also creates Functor/Strict) I will split this PR into two parts. One for strict pseudofunctors, and one for the bicategory of groupoids.

joelriou
joelriou reviewed Jun 18, 2025
View reviewed changes
@joelriou joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 18, 2025
@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 Jul 5, 2025
@leanprover-community-bot-assistant
Copy link
Copy Markdown
Collaborator

leanprover-community-bot-assistant commented Jul 5, 2025

This pull request has conflicts, please merge master and resolve them.

@callesonne callesonne mentioned this pull request Oct 2, 2025
Closed
1 task
This was referenced Oct 25, 2025
Closed
Open
mathlib-bors bot pushed a commit that referenced this pull request Nov 23, 2025
@callesonne
feat(Bicategory/Functor/Strict): add StrictPseudofunctor (#30132)
817e7b3 
This PR adds the notion of a strict pseudofunctor, where the coherence isomorphisms are equalities. This will be useful for #25561 where I define the bicategory of groupoids.
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

awaiting-author A reviewer has asked the author a question or requested changes. merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-category-theory Category theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@callesonne @robin-carlier @leanprover-community-bot-assistant @joelriou