Skeleton as a pseudofunctor

Stream: Is there code for X?

[Junyan Xu]

I've been working with CategoryTheory.Skeleton lately and realized that CategoryTheory.Functor.mapSkeleton (constructed by conjugating using CategoryTheory.skeletonEquivalence) should make Skeleton a pseudofunctor from Cat to Cat. Since CategoryTheory.Adjunction has the same coherence conditions as Equivalence, we should still get an (op)lax functor if we only have one adjunction for each category. So I came up with the following piece of code with sorries:

import Mathlib.CategoryTheory.Adjunction.Basic
import Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

universe v u v' u'
namespace CategoryTheory
open Functor
variable {T : Cat.{v, u} → Cat.{v', u'}}
variable {F : ∀ C : Cat, C ⥤ T C} {G : ∀ C, T C ⥤ C}

def OplaxFunctor.ofAdjunction (adj : ∀ C, F C ⊣ G C) : OplaxFunctor Cat Cat where
  obj := T
  map f := G _ ⋙ f ⋙ F _
  map₂ h := (G _).whiskerLeft (whiskerRight h (F _))
  mapId C := (G C).whiskerLeft (leftUnitor _).hom ≫ (adj C).counit
  mapComp f g := whiskerLeft _ (associator ..).hom ≫ (associator ..).inv ≫
    whiskerRight (whiskerLeft _ ((rightUnitor _).inv ≫ whiskerLeft _ (adj _).unit ≫
      (associator ..).inv) ≫ (associator ..).inv) _ ≫ (associator ..).hom
  map₂_id _ := by rw [whiskerRight_id', whiskerLeft_id']
  map₂_comp _ _ := by rw [whiskerRight_comp, whiskerLeft_comp]
  mapComp_naturality_left := sorry
  mapComp_naturality_right := sorry
  map₂_associator := sorry
  map₂_leftUnitor _ := sorry
  map₂_rightUnitor := sorry

end CategoryTheory

My questions:

1. Is there a name for this in the literature?
2. Is there tactics/a simp set to solve the sorries automatically?
3. There should also be a version in terms of CategoryTheory.Bicategory.Adjunction, which is more general but also less universe polymorphic, and you won't be able to abuse functor composition defeq there.

[Yaël Dillies]

About 2, have you tried mon_tauto?

[Junyan Xu]

This is not about monoidal categories though?

[Junyan Xu]

As an aside, I tried to make the obj field of mapSkeleton functor defeq to Quotient.map in this branch, but it makes the map field more complicated, and I decided it's not worth it.

[Junyan Xu]

Update: Aristotle was able to solve all sorries :clap:

[Junyan Xu]

original file by Aristotle

My golfed proofs that work with latest mathlib:

import Mathlib.CategoryTheory.Adjunction.Basic
import Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

universe v u v' u'

namespace CategoryTheory

open Functor

variable {T : Cat.{v, u} → Cat.{v', u'}}

variable {F : ∀ C : Cat, C ⥤ T C} {G : ∀ C, T C ⥤ C}

def OplaxFunctor.ofAdjunction (adj : ∀ C, F C ⊣ G C) : OplaxFunctor Cat Cat where
  obj := T
  map f := G _ ⋙ f ⋙ F _
  map₂ h := whiskerLeft (G _) (whiskerRight h (F _))
  mapId C := whiskerLeft (G C) (leftUnitor _).hom ≫ (adj C).counit
  mapComp f g := whiskerLeft _ (associator ..).hom ≫ (associator ..).inv ≫
    whiskerRight (whiskerLeft _ ((rightUnitor _).inv ≫ whiskerLeft _ (adj _).unit ≫
      (associator ..).inv) ≫ (associator ..).inv) _ ≫ (associator ..).hom
  map₂_id _ := by rw [whiskerRight_id', whiskerLeft_id']
  map₂_comp _ _ := by rw [whiskerRight_comp, whiskerLeft_comp]
  mapComp_naturality_left _ _ := NatTrans.ext <| by ext; simp [← map_comp]
  mapComp_naturality_right _ _ _ _ := NatTrans.ext <| by ext; simp [← map_comp]
  map₂_associator _ _ _ := NatTrans.ext <| by
    ext; simp [Bicategory.associator, ← map_comp]
  map₂_leftUnitor _ := NatTrans.ext <| by
    ext; simp [Bicategory.leftUnitor, ← map_comp]
  map₂_rightUnitor _ := NatTrans.ext <| by ext; simp [Bicategory.rightUnitor]

end CategoryTheory

[Junyan Xu]

The proofs turn out to be not so complicated (the main insight being rewriting using map_comp backwards). Maybe a better question is making a tactic to come up with mapComp automatically ...

[Edison Xie]

Can you hint aesop_cat to use map_comp backwards and see what happens?

[Junyan Xu]

What's the incantation for doing that (adding the backward direction of a lemma to the "simp set" of aesop_cat locally in a section)?