colimit-preserving functors preserve pointwise LKE

Stream: Is there code for X?

[Robin Carlier]

Pointwise left kan extensions are defined via colimits, so colimit-preserving functors should preserve them. I see nothing like this in CategoryTheory/Functor/KanExtension right now, am I missing it somewhere?
Maybe @Joël Riou already has a PR/code in store for this?

[Joël Riou]

In the bicategory context, @Yuma Mizuno has developped related notions of absolute Kan extensions.
I have not formalized the notion of preservation of (pointwise) Kan extensions, and I do not intend to formalize it, because I am mostly interested in the application to derived functors, in which case the concept of derivability structure makes it easy to check derived functors are absolute (preserved by the postcomposition with any functor, as in https://github.com/leanprover-community/mathlib4/blob/40c8ff3ee0d8327916f134a1cfc41752af19a0d2/Mathlib/CategoryTheory/Functor/Derived/Adjunction.lean#L91-L92 ).

[Robin Carlier]

Ok. Then I’ll formalize it. I need it and my Kan extensions are not absolute.
For context, I want to define the Day convolution monoidal structure for functors from a (small) monoidal category C to a cocomplete, closed symmetric monoidal category V. The tensor product is by definition a (pointwise) LKE, and in computations I need to show that taking the tensor product with an element of V "commutes" with convolution, and this requires this kind of preservation of extensions statements.

[Robin Carlier]

(Ideally, Day convolution of functors will be used to define the "join" monoidal structure on augmented simplicial sets).

[Kim Morrison]

Does one actually need symmetric (not just braided) for Day convolution? I have a dim memory it is no harder, and once upon a time I actually wanted that generalization.

[Kim Morrison]

In a different direction, is there some factorization one can do, building Day convolution as a presheaf first without cocompleteness, and then representing it using cocompleteness? (Sorry if that is nonsense, it's been a while since I thought about these things...)

[Robin Carlier]

Kim Morrison said:

In a different direction, is there some factorization one can do, building Day convolution as a presheaf first without cocompleteness, and then representing it using cocompleteness? (Sorry if that is nonsense, it's been a while since I thought about these things...)

For the first thing: I think I need at least that both tensorLeft and tensorRight commutes with colimits for the way I intend to construct the associators, which is easily deduced from closed + braided, but apart from that yes, one should be able to remove that (should also be straightforward to do it right now from my wip code). (Edit: noticed that you were talking about removing symmetric, not braided. I also believe you don't need it, and will try to play with the assumption when I have more code on Day convolution)

For the second: yes, the presheaf it corepresents is easy to define (cor 2.4 here) and then assuming some Kan extensions exist, it gets corepresented.
I considered this, but I feel like working at the presheaf level is not making it easier to prove e.g associativity.
More concerning is perhaps the fact that I don't think mathlib has Yoneda-like statements to corepresents V-valued presheaves where V is not Type u. (Statements like this would require some form of cocompleteness of V anyway I think). Nonsense, its an honest presheaf and I had a brain fart.

So given the fact that we already have a machinery for left Kan extensions functors, and that it gives things like bifunctoriality for free, I prefer to work that way and lose that extra micron of generality.

[Kim Morrison]

I would have guessed that things like associativity are actually easier to prove at the presheaf level, as you can do them pointwise.

I'm a little skeptical about "V need not be cocomplete" only being a micron of generality, I guess it has a lot to do with what you expect V to be. :-)

[Robin Carlier]

(Side note on the idea that you can work at the "representable presheaf" level for defining the monoidal structure: it would work better if monoidal categories were defined as some kind of fibrations over the 2-truncated (or even the full) simplex category: this is how monoidal categories are set up for infinity-categories. It would be nice (and even necessary when we will eventually want to show that the nerve of a monoidal category is a monoidal quasicategory) to have this alternative description of monoidal categories, as well as the glue API to go back and forth between points of view, but this is going to be a lot of work)

[Robin Carlier]

Kim Morrison said:

I would have guessed that things like associativity are actually easier to prove at the presheaf level, as you can do them pointwise.

I'm a little skeptical about "V need not be cocomplete" only being a micron of generality, I guess it has a lot to do with what you expect V to be. :-)

Well I've tried associativity at the presheaf level, and it seems to be equally if not more of a pain that at the non-presheaf level. The issue is that for iterated day convolution, you get a mix of external product and day convolution, which is a bit of a pain to work with.

What do you expect V to be? Do you have an interesting application to a non-cocomplete V in mind? Most (if not all) references I could find also assume cocompleteness, so I am not sure it's that used without that hypothesis.

As I said, my motivation is joins of augmented simplicial sets, so V will be Type u, which is cocomplete enough.

[Robin Carlier]

(Also, I guess mathematically one of the reason people don’t care too much about the non-cocomplete case is that as a worst case scenario, you can replace V by presheaves on V, with day convolution monoidal structure, I think this gives "the right thing" up to composition with Yoneda)

[Robin Carlier]

Preservation of Kan extensions is at #24809.

[Kim Morrison]

Once upon a time I wanted to use Day convolutions in studying monoidal categories enriched in braided tensor categories as a model for boundary conditions for 3d TFTs. Here it's often convenient to be able to work directly with diagrammatic categories, which tend not to be themselves (co)complete (you can pass to some suitable envelope to make them cocomplete, but sometimes it's easier to stay in the diagrammatic world). In any case, none of that ever made it to papers, so I'm not going to be at all sad either way. :-)

[Robin Carlier]

Ok, I see why you’d rather not assume cocompleteness for smalll diagrams. I am still not sure how to write the thing at the level of presheaves only yet.
As I said, I feel like the main issue is associativity: since the presheaf corepresented by (dayConvolution F G) is H ↦ (F ⊠ G) ⟶ (tensor C ⋙ H), where ⊠ is the externtal tensor product, the one for dayConvolution (dayConvolution F G) H is K ↦ ((dayConvolution F G) ⊠ H) ⟶ (tensor C ⋙ K), and this one is a bit of a pain to deal with. If I can show in a non-too painful way that the latter is equivalent to K ↦ (F ⊠ G) ⊠ H) ⟶ (tensor C).prod (𝟭 C) ⋙ tensor C ⋙ K), then we can make the presheaf approach work (if the category is bi-closed, there is perhaps a way to get that - ⊠ H on the other side, but this would require a few new constructions around the external product I guess).

[Yuma Mizuno]

Joël Riou said:

In the bicategory context, @Yuma Mizuno has developped related notions of absolute Kan extensions.

In the bicategory context, the preservation is defined by docs#CategoryTheory.Bicategory.Lan.CommuteWith as a Prop class.