over category via a functor

Stream: Is there code for X?

[Kenny Lau]

Let F : C => D be a functor, and let y : D.

Then one can consider the category where objects are (x, u) with x : C and u : F.obj x -> y. This is like CategoryTheory.Over but across a functor.

Is this in Mathlib?

[Kenny Lau]

Context: given a scheme X, I want to consider the category of rings R equipped with a "structural morphism" Spec R -> X.

[Yaël Dillies]

docs#CategoryTheory.Comma ?

[Kenny Lau]

actually i think it's CategoryTheory.CostructuredArrow , thanks

[Kenny Lau]

@Joël Riou I was like 200 lines deep in this proof that every P : Psh(Aff/X) (defined above) has a left Kan extension to Psh(Aff) until...

I realised that none of my lines require any property at all for rings and schemes, so they can all be generalised, so in general:

If F : C => D is a functor (between locally small categories) and X : D then every presheaf on CostructuredArrow F X has a pointwise left Kan extension (along the projection functor CostructuredArrow F X => C^op to a presheaf on C^op (i.e. copresheaf on C).

Yet I cannot find any lemma like this in Mathlib. Before I spend more hours of my life on this, is this already in Mathlib?

[Kenny Lau]

(To be clear, P extends to the functor that sends c : C^op to (u : F(c) ⟶ D) × P(u)

[Kenny Lau]

MWE:

import Mathlib

universe u

open CategoryTheory

variable {C D : Type (u + 1)} [Category.{u} C] [Category.{u} D]
  (F : C ⥤ D) (d : D)
  (P : (CostructuredArrow F d)ᵒᵖ ⥤ Type u)

instance : Functor.HasPointwiseLeftKanExtension (CostructuredArrow.proj F d).op P := by
  intro c
  unfold Functor.HasPointwiseLeftKanExtensionAt
  -- 100 more lines of proof

instance : Functor.HasLeftKanExtension (CostructuredArrow.proj F d).op P := inferInstance

[Kenny Lau]

CategoryTheory.OverPresheafAux.YonedaCollection feels similar but I think my result is more general

[Kenny Lau]

Made #27309

[Robin Carlier]

I am a bit late because you went ahead and coded the thing, but I think it would be much nicer to have a result that makes no assumption on size and does not require the target category to be Type.

Here, the key result is the computation of the category "Between" that you made via the "partition".

I think your result follows from a combination of more general facts

1. The category that computes the value at c of the left Kan extension you consider (which you call Between F d c) admits a functor to a discrete category (in this case, Discrete (CostructuredArrow F d)).
2. If a category C admits a functor p to a category D such that D is discrete, the colimit of a functor out of C is given by the coproduct of the colimits of the restrictions at each fibers of p. In your case, you have identified that the relevant fibers have a terminal object, thus the computation of the colimit of each such fiber is easy.

I think result 2. itself is an instance of the more general facts that 1) a functor to a discrete category is automatically a cofibered category 2) colimits out of a cofibered category can be computed "fiberwise": first do the colimit of each fibers, and then the colimit of each diagram you obtain.

Note that all of this happens purely at the level of diagrams and so Type u or size only enters the picture at the very very end, where you use that fiberwise you have enough colimits in type.

[Kenny Lau]

@Robin Carlier it’s not too late, because in my mental picture it’s less effort to generalise existing code than to come up with the most general code at the first go.

I appreciate your generalisations a lot! Do you know if what you call cofibrred category is already in mathlib? if not, what is the closest thing we have?

[Robin Carlier]

We have fibered categories for sure (docs#CategoryTheory.Functor.IsFibered), and a cofibered category could be defined as F.op.IsFibered (even if I’d prefer it if there was also a "dual" typeclass to IsFibered)
for the point about computation of colimits in cofibered categories we have file#CategoryTheory/Limits/Shapes/Grothendieck which treats the special case of a strict Grothendieck construction but I don’t think that this is sufficient here sadly.

[Robin Carlier]

(Note that the full generalization here is probably quite a lot of work compared to the original thing though!)

[Robin Carlier]

Probably 2. is provable without all the full cofibered category picture

[Kenny Lau]

I think I would be satisfied to do 2 itself without the more general picture of cofibered category.

[Kenny Lau]

what is the closest result we have to 2?

[Robin Carlier]

Not sure that there’s much better than doing it by hand within current mathlib... I’d need to think a bit if we have better. Note that already the statement contains a possible evil: the "fibers" of a functor can either be understood in the "strict" or "weak" sense. In the strict sense, they will mention equality of objects, so "evil". In the weak (= non-evil) sense, the fiber can be defined as the docs#CategoryTheory.Limits.CategoricalPullback of the functor along fromPunit at the relevant point, but the API for categorical pullbacks is a bit new and not yet stable.

[Kenny Lau]

@Robin Carlier i've made #27321 for the fiberwise colimit

[Kenny Lau]

something amazing happened: through the CI process it was discovered that CategoryTheory.Functor.Fiber already exists, which is a testament to the effectiveness of following the naming convention!

[Kenny Lau]

this allows me to potentially use more existing API

[Robin Carlier]

Functor.Fiber is the "evil one", though.

[Kenny Lau]

yes, the one in my PR is also evil

[Robin Carlier]

At least, in the case of a functor to a discrete category we're lucky that the "non-evil" and "evil" fibers are equivalent (for a general functor, this is not the case)

[Robin Carlier]

I’d like to hear @Joël Riou’s opinion for this case but I think mathlib would prefer minimizing evil that is not "necessary", and here I think it’s not a necessary one.

[Kenny Lau]

I guess I could try to use the pullback as well, but I’m not sure if that would make it harder or easier.

[Kenny Lau]

is it really less evil if it’s “equivalent”?

[Joël Riou]

I would think that in #27321, Fiber should refer to https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/FiberedCategory/Fiber.html#CategoryTheory.Functor.Fiber

[Robin Carlier]

It is less "evil" in the sense that when working with it, you do not have goals that asks you for equality of objects, or results that produce such, and the constructions have far less chance of accidentally leaking eqToHom's everywhere. I can see happening cases where you want to "compute" the restriction of the diagram at a given fiber (say, because you know it’s naturally isomorphic to a "better" functor, for which you know how to compute the colimit), and then that alone will bring some eqToHom hell etc.

[Robin Carlier]

Joël Riou said:

I would think that in #27321, Fiber should refer to https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/FiberedCategory/Fiber.html#CategoryTheory.Functor.Fiber

Can you explain why you feel the naive fiber is what we want here?

[Joël Riou]

I am only saying that there is no need to duplicate the definition of the naive fiber.

[Kenny Lau]

@Joël Riou yes, I am aware that it's duplicated, and I actually just finished deduplicating it. But I think it would also be important to also discuss whether to use the "naive" version or the "less evil" version

[Robin Carlier]

(Note that in favor of using the "non-evil" one, it makes the result also true if D is merely equivalent to a discrete category, because we can then freely replace C and D by equivalent categories (as long as we track the coherence with F), but since mathlib has no typeclass asserting a category is "weakly discrete", it’s not the nicest to state in the current state of afairs and would be yet an other detour.)

[Joël Riou]

Currently, we only have IsDiscrete. Unless we have reasons to develop essentially discrete categories, I think it is very much fine to use the naive fiber.

[Kenny Lau]

@Robin Carlier I've updated the PR #27321.

(btw I think CategoryTheory.Functor.Fiber.fiberInclusion should have explicit p and S and I will do that in a PR)

[Robin Carlier]

Well, that’s a bit disappointing to me because I’m working hard with CategoricalPullback to make it so that we can talk about things like fibers in an actually equivalence-invariant way (one hope being that one day we will have constructors for fibered categories/cartesian morphisms that do not mention equality of objects or functors, that’s claimed to be possible). But then so be it.

I just hope this will not cause "eqToHom contamination" whenever we want to rely on the content of this PR.

[Kenny Lau]

i'll try to use the non-evil version in another file locally and see what happens

[Kenny Lau]

made #27323 to make fiberInclusion explicit

[Joël Riou]

That a functor is a fibered category in the sense of Grothendieck is not invariant under pre/post-composition with equivalences. If we want to allow a little bit more flexibility, I think that the best we could do here would be to use aHasFibers assumption from the fibered category.

[Robin Carlier]

I guess the point is that the notion of fibration linked is different from the one of Grothendieck and that it does recover the notion if the functor is furthermore an isofibration (which is the "non-equivalence invariant" part). The claims in the link is that this notion works just as well as Grothendieck’s for most purposes (critically, it should provide a straightening/unstraightening equivalence of (probably bi-)categories between fibrations over C and pseudofunctors from LocallyDiscrete C to Cat, which is most of what we want.). Eventually I’d love to be able to work on bringing this notion to Mathlib, because I feel it’s much much more flexible than HasFiber which bundles an equality of functors.

[Kenny Lau]

@Robin Carlier I now have a version using CategoricalPullback.

[Kenny Lau]

https://github.com/kckennylau/EllipticCurve/blob/07f6e9052b76ee63e85143cca10f788c461c89b7/EllipticCurve/Grassmannians/FiberColimitPullback.lean

[Robin Carlier]

Nice, did you have any pain point working with that compared to the other fiber? So that maybe I can know what to work on when making the general definition.

[Kenny Lau]

@Robin Carlier not really, i just used the first part of the file (in both versions) to define the API so that they are "the same object" to any user, and the proofs didn't need to be changed

[Kenny Lau]

this relates to the question i asked above: is it really less evil if they are equivalent?

[Kenny Lau]

Kenny Lau said:

is it really less evil if it’s “equivalent”?

[Robin Carlier]

Well, looking at the proof they still bundle all the eqToHom/equality of object that you can’t avoid because the base is discrete. Meaning i may have made too much noise about this for too little of an outcome. I guess the approach with the naive fiber will at least lead to less duplication.

[Kenny Lau]

(I was secretly wondering, after you've looked at the alternate version, whether there's a "different" way to remove the eqToHom)

[Robin Carlier]

My main worry was about spilling goals with equality of objects/eqToHom everywhere.

[Kenny Lau]

I guess I can test it by using it for the over category theorem