Bicategory of enriched categories

Stream: Infinity-Cosmos

[Jakob von Raumer]

Are we still missing the bicategory V-Cat or is that in some PR?

[Jakob von Raumer]

(Anyways, started working on this a bit, at least started to show that enriched functors form a categories)

[Emily Riehl]

Yes, we've got a lot of enriched category pieces missing. What's most helpful is to develop things both in the enriched category setting and the enriched ordinary category setting because the latter will give us a slightly between strict bicategory of infinity-categories.

[Emily Riehl]

It would be awesome if someday someone adopted some of the conical limits PRs from @Jon Eugster; search "label=infinity-cosmos" on the open mathlib PRs. But no pressure... :)

[Jakob von Raumer]

Ah, did @Jon Eugster abandon those for some reason?

[pro-Lie stabilizer]

@Emily Riehl I am only reading here and not following at the code level.

Is it ok if I ask on this topic about the strictness in the bicategory of ∞-categories? I would like to know if it is possible in your or any appraoch you are aware of that there would be a more "lax" thing to do than strict bicategory

[Emily Riehl]

Jakob von Raumer said:

Ah, did Jon Eugster abandon those for some reason?

Yes, Jon told me he'd be happy if someone else took them over. He's been too busy with other things.

[Emily Riehl]

Akil Qasim said:

Is it ok if I ask on this topic about the strictness in the bicategory of ∞-categories? I would like to know if it is possible in your or any appraoch you are aware of that there would be a more "lax" thing to do than strict bicategory

Absolutely. A design decision made with the ∞-cosmos axioms is to take advantage of the fact that many of the models of ∞-categories (quasi-categories, complete Segal spaces) are categories of fibrant objects in a model structure with all objects cofibrant that is enriched (strictly) of simplicial sets with the Joyal model structure. As a consequence, after applying some "change of enrichment" to the hom objects (this hoFunctor thing we've been on about) you get a strict bicategory of ∞-categories, ∞-functors, and ∞-natural transformations.

[Emily Riehl]

All of the stuff we're about to do in this bicategory is equivalence invariant, so it's possible (and arguably more morally correct) to work instead in a bicategory of ∞-categories, ∞-functors, ∞-natural transformations. But our thought was it would make the proofs a bit shorter to assume a little extra strictness since it's present in examples.

[pro-Lie stabilizer]

Thanks for this explanation.

I noticed something simple: bicategories can be arranged to have as many entries as the strict one, in a way such that the identity and associativity laws are just natural isomorphisms, and with the effect that there is not a pentagon anymore.

If this is true (which it has been a while since I thought about that) then is that also consistent with how (∞,1)-categories are said to form an (∞,2)-category?

[Jakob von Raumer]

V : Type v
inst✝³ : Category.{w, v} V
inst✝² : MonoidalCategory V
C : Type u₁
inst✝¹ : EnrichedCategory V C
D : Type u₂
inst✝ : EnrichedCategory V D
F G H : EnrichedFunctor V C D
α : EnrichedNatTrans F G
β : EnrichedNatTrans G H
X Y : C
hα : (λ_ (Hom X Y)).hom ≫ (ρ_ (Hom X Y)).inv ≫ (F.map X Y ⊗ₘ α.app Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) =
  (α.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
hβ : (λ_ (Hom X Y)).hom ≫ (ρ_ (Hom X Y)).inv ≫ (G.map X Y ⊗ₘ β.app Y) ≫ eComp V (G.obj X) (G.obj Y) (H.obj Y) =
  (β.app X ⊗ₘ H.map X Y) ≫ eComp V (G.obj X) (H.obj X) (H.obj Y)
⊢ (λ_ (Hom X Y)).hom ≫
    (ρ_ (Hom X Y)).inv ≫
      (F.map X Y ▷ 𝟙_ V ≫
          Hom (F.obj X) (F.obj Y) ◁ (ρ_ (𝟙_ V)).inv ≫
            Hom (F.obj X) (F.obj Y) ◁ (α.app Y ⊗ₘ β.app Y) ≫
              Hom (F.obj X) (F.obj Y) ◁ eComp V (F.obj Y) (G.obj Y) (H.obj Y)) ≫
        eComp V (F.obj X) (F.obj Y) (H.obj Y) =
  ((ρ_ (𝟙_ V)).inv ≫ (α.app X ⊗ₘ β.app X) ≫ eComp V (F.obj X) (G.obj X) (H.obj X) ⊗ₘ H.map X Y) ≫
    eComp V (F.obj X) (H.obj X) (H.obj Y)

Here's hoping grind will be able to solve such goals soon :sweat_smile:

[Jakob von Raumer]

On the other hand, the string diagrams we now have are already pretty helpful, the widget didn't exist yet, when I last dabbled in monoidal categories...
image.png

[Jakob von Raumer]

(@Yuma Mizuno at some steps the diagrams cannot be shown, do you know why that is? Can give you a MWE if you want)

[Kim Morrison]

Jakob von Raumer said:

Here's hoping grind will be able to solve such goals soon

It's not crazy. We're going to have to add some custom support for associativity (i.e. the 1-category parenthesisation problem), but then I think after that every 2-categorical diagram I've even met (and I've seen many) might actually be in range for grind... It will take us a while to get the support in place though, as more algebraic/arithmetical problems are higher priorities right now.

[Jakob von Raumer]

Put the category of enriched functors in its own PR as a first step: #26731

[Jakob von Raumer]

(Also, if anyone wants to have a look at the (probably not infinity cosmos related) PR on linear categories: #26357)

[Jon Eugster]

Jakob von Raumer said:

Ah, did Jon Eugster abandon those for some reason?

I've taken up a different job outside the Lean universe and have yet to find my way back to make some time for Lean. Hopefully, Lean will see more of me again in a few weeks/months

I'd be happy if they'd be adopted and please DM if I can help directly.

[Yuma Mizuno]

Jakob von Raumer said:

(Yuma Mizuno at some steps the diagrams cannot be shown, do you know why that is? Can give you a MWE if you want)

Could you provide a MWE? I would like to take a look at it.

[Jakob von Raumer]

Seems to be related to creating a hypothesis with a have statement:

example {C : Type} [Category C] [MonoidalCategory C]
    {D : Type} [Category D] [MonoidalCategory D]
    (F G : C ⥤ D) (α : F ⟶ G)
    {X Y : C} {Z : D} (h : α.app X = α.app X) :
    α.app X ⊗ₘ 𝟙 Z = α.app X ⊗ₘ 𝟙 Z := by
  have h' := h
  with_panel_widgets [Mathlib.Tactic.Widget.StringDiagram]
  sorry  -- "No String Diagram."

[Yuma Mizuno]

Thanks! I hope #26748 fixes the bug.

[Emily Riehl]

@Kim Morrison I haven't been following along with grind but I'd be happy with something that could do some 1-categorical diagram chasing (perhaps with the user supplying the equalities like α : f ≫ g = h ≫ k, perhaps even in the direction or order they should be used) that would automate (i) searching for the right associativity and (ii) searching whether you can apply them under a functor (eg rewriting back and forth along Functor.map_comp as needed).

[Emily Riehl]

Jakob von Raumer said:

V : Type v
inst✝³ : Category.{w, v} V
inst✝² : MonoidalCategory V
C : Type u₁
inst✝¹ : EnrichedCategory V C
D : Type u₂
inst✝ : EnrichedCategory V D
F G H : EnrichedFunctor V C D
α : EnrichedNatTrans F G
β : EnrichedNatTrans G H
X Y : C
hα : (λ_ (Hom X Y)).hom ≫ (ρ_ (Hom X Y)).inv ≫ (F.map X Y ⊗ₘ α.app Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) =
  (α.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
hβ : (λ_ (Hom X Y)).hom ≫ (ρ_ (Hom X Y)).inv ≫ (G.map X Y ⊗ₘ β.app Y) ≫ eComp V (G.obj X) (G.obj Y) (H.obj Y) =
  (β.app X ⊗ₘ H.map X Y) ≫ eComp V (G.obj X) (H.obj X) (H.obj Y)
⊢ (λ_ (Hom X Y)).hom ≫
    (ρ_ (Hom X Y)).inv ≫
      (F.map X Y ▷ 𝟙_ V ≫
          Hom (F.obj X) (F.obj Y) ◁ (ρ_ (𝟙_ V)).inv ≫
            Hom (F.obj X) (F.obj Y) ◁ (α.app Y ⊗ₘ β.app Y) ≫
              Hom (F.obj X) (F.obj Y) ◁ eComp V (F.obj Y) (G.obj Y) (H.obj Y)) ≫
        eComp V (F.obj X) (F.obj Y) (H.obj Y) =
  ((ρ_ (𝟙_ V)).inv ≫ (α.app X ⊗ₘ β.app X) ≫ eComp V (F.obj X) (G.obj X) (H.obj X) ⊗ₘ H.map X Y) ≫
    eComp V (F.obj X) (H.obj X) (H.obj Y)

Here's hoping grind will be able to solve such goals soon :sweat_smile:

This is cool. What is it a proof of?

[Jakob von Raumer]

@Emily Riehl That's the naturality of the vertical composition of two enriched natural transformations.

[Jakob von Raumer]

@Joël Riou We don't have the constructor for bicategories that derives whiskering from horizontal composition instead of the other way around, do we?

[Emily Riehl]

Last I heard from @Yuma Mizuno, horizontal composition of bicategories isn't in mathlib at all, with one exception being as an auxilliary definition in PR #25784 where we use it to extract the bicategory structure from the Cat-enriched category. By the way, if anyone wants to contribute to the reviewing it would be very appreciated, as I'd love to get this merged.

[Jakob von Raumer]

Next puzzle piece on the way to defining $\mathcal{V}\textbf{-Cat}$: Isos in enriched categories #26931 (Took the definition from the paper by @Kim Morrison 's paper as well, though I'm not entirely sure why don't want to define isos as a triple of G ⟶ X ⟶[V] Y, H ⟶ Y ⟶[V] X and an iso between 𝟙_ V and G ⊗ H with appropriate conditions)

[Emily Riehl]

Sorry what definition do you have in mind? Is there a typo here?

It is standard in the enriched categories literature to define an isomorphism in an enriched category to be an isomorphism in the underlying category (as you've done in your code). As motivation perhaps the enriched Yoneda lemma holds: representable V-functors are V-naturally isomorphic iff the representing objects are isomorphic in the underlying category.

[Jakob von Raumer]

Thanks, that's the kind of reasoning, I was looking for, I also noticed that otherwise it wouldn't correspond to isos in the enriched ordinary category case.

The alternative definition I had in mind was something along these lines:

structure EnrichedIso (X Y : C) where
  G : Center V
  H : Center V
  iso_GH : 𝟙_ V ≅ G.1 ⊗ H.1
  hom : G.1 ⟶ X ⟶[V] Y
  inv : H.1 ⟶ Y ⟶[V] X
  hom_inv : iso_GH.hom ≫ (hom ⊗ₘ inv) ≫ eComp V X Y X = eId V X := by aesop_cat
  inv_hom : iso_GH.hom ≫ (G.2.β _).hom ≫ (inv ⊗ₘ hom) ≫ eComp V Y X Y = eId V Y := by aesop_cat

[Jakob von Raumer]

(or some other way of "grading" it by an element in the Drinfeld center)

[Jakob von Raumer]

The PR is ready for review anyways :grinning_face_with_smiling_eyes:

[Emily Riehl]

What is center V?

[Jakob von Raumer]

The Drinfeld center of V

[Jakob von Raumer]

Finished the instantiation of $\mathcal{V}\textbf{-Cat}$ as a bicategory in #27129 :slight_smile: , needs some golf and clean up, and the iso PR to be merged first

[Jakob von Raumer]

Has anyone actually see the X ⟶[V] Ynotation being pretty-printed? I'm a bit lost on why it's not properly delabed by the pretty printer

[Jakob von Raumer]

That's because of that weird type ascription.

[Jakob von Raumer]

Fixed in the PR.

[Robin Carlier]

Kim Morrison said:

[…] We're going to have to add some custom support for associativity (i.e. the 1-category parenthesisation problem).

Re this: can you be more specific about this? At what level is this "custom support" supposed to take place: Core's work on grind? Mathlib through special annotations? other?

[Kim Morrison]

Yes, this would be Leo-level work on grind.

[Kim Morrison]

The most useful way to help would be to find examples from the category theory library where grind currently uses a huge number of Category.assoc instantiations, and ideally even to minimize these.

[Jakob von Raumer]

Made a new attempt in #27129 at the definition that doesn't use a separate notion of enriched natural transformations but instead just has natural transformations between F.forget and G.forget as 2-cells. Comments welcome!