mates

Stream: mathlib4

[Emily Riehl]

I'd like to make some changes to: file#CategoryTheory/Adjunction/Mates

Here "mates" refers to a bijection between natural transformations in certain (not-necessarily commutative squares) of functors involving a pair of adjunctions:

def transferNatTrans : (G ⋙ L₂ ⟶ L₁ ⋙ H) ≃ (R₁ ⋙ G ⟶ H ⋙ R₂)

I'd like to introduce simpler names "RightMate" and "LeftMate" to describe the toFun and invFun respectively. (I can also give these maps a simpler construction than appears in the current file, though ext, unfold, and simp can prove that these agree with the current functions.)

The reason I care so much about the explicit functions is they satisfy various coherences (most fully expressed in the language of a natural isomorphism between double categories but useful at a more elementary level) and I'm hoping that if these are tagged appropriately (I have no idea how simp works) Lean could prove automatically that various natural transformations defined using these operations iteratively are equal.

I plan to apply this to the construction of Beck-Chevalley natural transformations between various composites of adjoint functors between the slices of a locally cartesian closed category. (Part of a project with @Sina H 𓃵 and Steve Awodey on LCCC and polynomial functors.) Right now I'm stressing out about how exactly to implement the constructions of these natural transformations but with the above it should be easy to prove that all of the definitions are equal.

I'm writing here because I could use some advice on:
(i) How to propose changes to a file upon which other files depend.
(ii) Whether it's reasonable to propose renaming (and if so, how to start this discussion).
(iii) Whether it's good practice (or acceptable) to give explicit names for auxiliary functions (eg the toFun and invFun of an equivalence; or the induced map on the subtype of isos that exists under more restrictive hypothesis).
(iv) How to give Lean the info it needs to hopefully automate some 2-categorical diagram chasing.

[Floris van Doorn]

Not an expert in category theory, but some general remarks:
You can suggest changes to any file by making a pull request to Mathlib. Instructions here: https://leanprover-community.github.io/contribute/index.html
You already did the very first step, namely discussing what you want to do on Zulip.

Files that are not used often yet regularly lack quite some polish, so improvements would be welcome in such cases (I don't know if that is true for Mates).

[Floris van Doorn]

About the specific points:
(i) in your pull request, you are responsible for fixing things in all later files that import the file you changed.
(ii) For renaming things, I would suggest a new name here on Zulip, and if a maintainer says that they also like the new names, you can generally go ahead.
(iii) Generally in Mathlib we like to not define too many auxiliary things. If you define def myFun := myEquiv.toFun then what is the proper way to write it? myFun or myEquiv? Should lemmas be stated using myFun or myEquiv.? We definitely don't want both lemmas. (Note: in many cases we have multiple ways of writing the same thing, and we try to use one spelling as "the canonical one")
Specifically about an equivalence, you can already easily use the equivalence itself as a function, and by adding .symm you can use the reverse function (symm is preferred over invFun). Examples:

import Mathlib.Logic.Equiv.Basic

variable {α β : Type*} (e : α ≃ β)

#check (e : α → β)
#check (e.symm : β → α)

variable (x : α) (y : β)
#check e x
#check e.symm y
#check ⇑e -- type `α → β`, not too commonly used.

(iv) This is harder. You can mark any lemmas as @[simp] that you want simp to automatically apply (and aesop_cat will also use that). But that will only get you so far...

[Adam Topaz]

I think renaming things could be nice if we could make dot notation work. For example if you make a def with the name Quiver.Hom.rightMate then you could write f.rightMate for a natural transformation f of the right shape.

[Kim Morrison]

Very happy to see renaming happening here: be bold on that front.

Regarding Floris's point (iii) about avoiding having two ways to say the same thing: you don't need to completely avoid this, but ideally there will be an explicit choice of the preferred way to say things, and a simp lemma writing non-preferred ways into the preferred way.

[Kim Morrison]

Regarding Floris' point (iv), particularly in the category theory library most of the automation comes down to by ext; simp. Thus it's important not only to mark the right simp lemmas, but whenever there is an extensionality result (i.e. "you can prove this componentwise") that it is marked with @[ext].

Generally my process is to take any statement that should be automatable, look at why by ext; simp fails, and try to add either @[ext] or @[simp] lemmas that would make further progress.

[Emily Riehl]

Thanks for these tips. It's very useful for a beginner.

I now have a draft pull request I'd love feedback on. I'm using simply Mates for the mates bijection, now that I've finally learned to extract the inverse functions.

@Adam Topaz and @Kim Morrison I would have loved to prove the left inverse and right inverse fields of the Mates definition without appealing to ext (passing to components). In my head it's true by a very simple calculation involving pasting diagrams of natural transformations (using theorems that exist in the library, though those, to be fair, are often proven with components). But to apply them I needed to rewrite along equalities between functors (also in the library) and got stuck.

@Kim Morrison you'll see later I made heavy use of slice_rhs. I found I was basically randomly guessing which integers to use, I think because sometimes my composites were hidden under the application of a functor.

https://github.com/leanprover-community/mathlib4/pull/13840

[Joël Riou]

Emily Riehl said:

Kim Morrison you'll see later I made heavy use of slice_rhs. I found I was basically randomly guessing which integers to use, I think because sometimes my composites were hidden under the application of a functor.

In many situations, slice_[lr]hs can be replaced by rewrites using lemma_assoc instead of lemma and/or by making certain parameters explicit in the applications of these lemmas in case they may be applied in multiple places in the syntactic tree.

[Bhavik Mehta]

I wrote the original version of this file, originally for motivation very similar to yours here: https://github.com/b-mehta/topos (the todo list is a bit out of date, the repo contains a bit more than what it says it does!). Leaving some comments on your PR now, but I agree your construction is nicer, thanks!

[Emily Riehl]

Adam Topaz said:

I think renaming things could be nice if we could make dot notation work. For example if you make a def with the name Quiver.Hom.rightMate then you could write f.rightMate for a natural transformation f of the right shape.

I could imagine this begin useful for adjoint transposition as well (an important special case of mates).

Eg in a cartesian closed category for $f : X \times Y \to Z$ we'd have $f.curry : X \to Z^Y$ with f.curry.uncurry = f.