Computable version of pointwiseLeftKanExtension

Stream: mathlib4

[Kenny Lau]

Currently, we have CategoryTheory.Functor.pointwiseLeftKanExtension which noncomputably constructs a pointwise left Kan extension, given a similarly anti-computable Prop instance of HasPointwiseLeftKanExtension.

As a result, the constructed left extension would have worse definitional equality when it is used.

I think there should be a version of this that takes the explicit colimits, and explicitly constructs the extension instead. Is this desirable?

[Kenny Lau]

update: I essentially copied the code to my situation and the same code just works

[Kenny Lau]

@Joël Riou @Robin Carlier you might be interested in this

[Kenny Lau]

more concretely now, I have this code in my personal repo, which is a generalisation of this code in mathlib that takes in explicit colimit cocones and hence removes the "noncomputable" tag. should I PR this to mathlib?

(And note that I essentially just copied the code, and everything works out)

[Joël Riou]

I do not think we need computable colimits.

[Kenny Lau]

then we can't really control the left extension, we can only say what they're isomorphic to

[Robin Carlier]

I would guess if we really need good object-level def-eqs, we can use docs#CategoryTheory.Functor.copyObj to get a functor isomorphic to the original one, and being a pointwise left Kan extension is a property that is preserved by isomorphisms, so the new functor will have good defeqs and will remain a pointwise left Kan extension.

[Robin Carlier]

There’s also the option and building the functor and extension first, and only then prove that it is a pointwise left Kan extension, most of the time, you already have the candidate functor and extension before the colimit cocones.

[Kenny Lau]

well in my "real" use case it's a functor to types and you can see how the Types.leftExtension makes use of this computable version, and I don't really have the candidate functor except this explicit construction, which I would argue would be easier if it goes through the computable version in my repo

[Kenny Lau]

Robin Carlier said:

being a pointwise left Kan extension is a property that is preserved by isomorphisms,

ok, so you use copyObj to make the new functor, but how do you prove that they're isomorphic? you would need to go through an explicit colimit argument (so you still need the explicit colimit as argument). moreover, you don't get functoriality for free when you build your new functor (whereas the pointwise extension is, well, pointwise).

[Kenny Lau]

when you're proving functoriality, you will be basically using the same code as the functoriality code in this noncomputable version, so you're duplicating code

[Kenny Lau]

in some sense you don't actually "need" to control the colimit i guess, because for example we only care about P^2_S as a scheme over S, so we don't really think about it as a scheme over Spec Z

[Robin Carlier]

I don’t understand what you mean when you say you don’t get functoriality. F.copyObj e is a functor. docs#CategoryTheory.Functor.isoCopyObj tells you that F.copyObj e is isomorphic to F. Now if you take F to be the pointwise left Kan extension with "bad defeq" and e be the family of colimit.uniqueUpToIso that your isColimit gives you, then you get a new functor, and a natural isomorphism, and what I’m saying is that if α : F ⟶ L ⋙ G exhibhits G as a pointwise left Kan extension of F along L , and e : G ≅ G' is an isomorphism, then the canonical F ⟶ L ⋙ G' induced by e exhibits G' as a pointwise Left kan extension: noncomputably, this is isPointwiseLeftKanExtensionOfIsLeftKanExtension with the corresponding fact about non-pointwise left Kan extensions (docs#CategoryTheory.Functor.LeftExtension.isUniversalEquivOfIso₂): so as long as you have any family of isomorphism between from the objects of the arbitrary pointwise extension, you have a pointwise extension, with the desired objects.

[Kenny Lau]

thanks for the explanation. it makes more sense now.

[Robin Carlier]

Also, this is really a "chosen/abstract colimit" issue rather than a "computable/noncomputable" one: if IsColimit were a Prop and IsColimit.desc were tagged noncomputable, these kind of issues would still be there! This is because at the end of the day IsColimit asserts something about a specific colimit cocone, with specific cocone point and maps, and any other one, however obtained, will be canonically (though possibly noncomputably, but that’s irrelevant 90% of the time) isomorphic but not equal to this one.