feat(Bicactegory/NaturalTransformation): refactor strong natural transformations

[callesonne]

This PR is a minor refactor of strong natural transformations. Previously, I had defined strong natural transformations between oplax functors. Now I specialize this directly to pseudofunctors and improve the API for this. The reason for doing this is that strong natural transformations of pseudofunctors should be defined directly in terms of pseudofunctors (instead of being defined as strong transformations of the underlying oplax functors). This is because there should also be strong transformations between lax functors, making this definition somewhat unnatural.

I have chosen not to simultaneously define strong transformations between oplax functors as this is the only case I care about for now (I want to define the bicategory of pseudofunctors), but it will be very easy to generalize if one feels the need to do so.

---

• [ ] depends on: #18250
• [ ] depends on: #18252

[github-actions[bot]]

PR summary b04d5fa562

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo (new file)	356

---

Declarations diff

+ comp_app + hasCoeToOplax ++ StrongTrans ++ instance : Inhabited (StrongTrans F F) ++- whiskerLeft_naturality_comp ++- whiskerLeft_naturality_id ++- whiskerLeft_naturality_naturality ++- whiskerRight_naturality_comp ++- whiskerRight_naturality_id ++- whiskerRight_naturality_naturality +-+ id.toOplax +-+ mkOfOplax +-+ toOplax - OplaxFunctor.bicategory - Pseudofunctor.categoryStruct - StrongOplaxTrans - category - instance : CategoryStruct (OplaxFunctor B C) - instance : Inhabited (StrongOplaxTrans F F) -++ id -++ vcomp

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

[leanprover-community-bot-assistant]

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

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#18250~~
• ~~leanprover-community/mathlib4#18252~~ By Dependent Issues (🤖). Happy coding!

[callesonne]

Do we agree that OplaxFunctor.StrongOplaxTrans and PseudoFunctor.StrongTrans are exactly the same structure, up to replacing OplaxFunctor with PseudoFunctor?

Another equivalent way of defining StrongTrans between pseudofunctors would be as StrongTrans F.toOplax G.toOplax. However, I thought this approach here would give a more uniform approach for treating the Lax and Oplax settings similarly. @joelriou or @yuma-mizuno what do you think about this? Should I just define StrongTrans between pseudofunctors as an abbrev for StrongTrans F.toOplax G.toOplax? This has the advantage of not having to duplicate any API, but I guess it will be slightly trickier to transfer API results that should be stated in the Lax setting.

[YaelDillies]

I think a good analogy is with Bimon_. Bimon_ C is defined as Comon_ (Mon_ C), and the equivalence with Mon_ (Comon_ C) is proved later

[yuma-mizuno]

Should I just define StrongTrans between pseudofunctors as an abbrev for StrongTrans F.toOplax G.toOplax?

I don't have a strong opinion about that, but I think doing so is reasonable. The definition mapId (a : B) : map (𝟙 a) ≅ 𝟙 (obj a) already chooses the "oplax direction" in a sense.

[callesonne]

Okay I tried out the abbrev approach, but I still need to restate pretty much all simp lemmas for strong transformations of pseudofunctors anyways, as otherwise I get F.toOplax.map instead of F.map for a pseudofunctor F etc in the statement of these lemmas, and this makes it so that simp is unable to use them. There are also other simp lemmas that break in my bicategory of Pseudofunctor PR and I am still not completely sure why.

The only gain from the abbrev approach is therefore that I can avoid these .toOplax constructors.

On the other hand, the current approach will make the Lax case identical, and in case we develop some automation later on (which we definitely should at some point if all 9 variations of transformations are needed in mathlib) then this uniformity will make that much easier.

Since the gain is rather minimal, I would prefer to just go ahead with it as it is now (but if someone has strong opinions on this, I can try a bit harder to make it work)

[callesonne]

For clarity, in a recent commit when cleaning this up, I added a CategoryStruct instance for strong transformations of Oplax functors. To not get clashes, I have made all similar category struct instances scoped (so e.g. to get the bicategory of oplax functors w oplax natural transformations, you now have to be in the Oplax.OplaxTrans namespace. Then later (if someone wishes) they can define a bicategory using strong transformations in the namespace Oplax.StrongTrans

[github-actions[bot]]

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

[jcommelin]

Thanks :tada:

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build