Proposal: Categorify the `Subobject`folder

Stream: mathlib4

[Fernando Chu]

Currently, the CategoryTheory/Subobject folder talks about two kind of "morphisms" between subobjects, those of the form x ≤ y, and those of the form x ⟶ y. It seems the former seems to be the intended way to talk about subobjects while the latter are a consequence that some of the operations are defined in terms of functors. Indeed, the Subobject/Basic lean file mentions:

Currently we describe pullback, map, etc., as functors. It may be better to just say that they are monotone functions, and even avoid using categorical language entirely when describing Subobject X. (It's worth keeping this in mind in future use; it should be a relatively easy change here if it looks preferable.)

The reason for this is clear, we usually want to show that Subobject X has some operation by showing first that MonoOver X has some corresponding operation, which is most naturally stated as a functor. Hence, in order to talk about the intend inequalities, we first have to decategorify a morphism x ⟶ y. This creates quite the overhead, as we would have to translate everything form category theory land to poset land, and some translations are missing, e.g. this.

Instead, I think the approach with lowest overhead is to talk only about category theory, and completely avoid the fact that Subobject X is a poset. That way all the results are in one single language and no translation is necessary. Of course, at some point we would like to e.g. say that Subobject X, as a poset, is a lattice; but this should then be a purely abstract consequence of the fact that it has finite (co)products, which should be stated in another file.

---

Tldr; would a PR de-de-categorifying (≅ categorifying) the Subobject folder be accepted?

[Joël Riou]

I do not think it is a good idea. One of the interests of Subobject X is that from an object X in a category, it produces a partially ordered type. For example, we have notions of artinian and noetherian objects which are defined using the order on Subobject. I believe it would be a mistake to reject the very good order API that we have, and which can express things which could be relatively ackward in the sole language of category theory.

[Joël Riou]

We currently do not use much of the functors/monotone maps involving Subobject types. As the remark suggests, we can keep in mind that using Galois connections instead of adjunctions could be an option if it turns out to become more convenient in the future.

[Fernando Chu]

I just looked at the Subobject/ArtenianObject and Suobject/NoetherianObject files and in fact they exclusively use the category-based results! (Other than in saying e.g. WellFoundedGT (Subobject X), as well as adding a .monotone/.toOrderHom/etc to a functor). So it seems to me that this rather supports my proposal. Even if it did use some stuff about the preorder, my suggestion is that the lemma would be in categorical language, so that any use of order stuff is a leOfHom/.monotone/.toOrderHom/etc away.

[Fernando Chu]

For some more context, this proposal comes from my experience formalizing for the geometric logic project, where it was very common that I was talking about subobjects in categorical language (again since that's the natural language when coming from MonoOvers, etc), but some results (e.g. OrderTop) were only in poset language, so I had to categorify them anyways.

[Joël Riou]

I would agree that we need more API, but I am afraid I cannot continue this discussion seriously if you consider that when the most basic definition of a file uses the term WellFoundedGT (Subobject X) then it "exclusively use the category-based results".

[Fernando Chu]

I think I did not explain well what I'm proposing, sorry about that. I'm not saying we should never consider Subobject X as a poset, this is definitely useful. What I'm saying is that when we are developing results specifically about subobjects, say in Subobject/Basic.lean, its content should never be using the order api. For a concrete example, we could change:

theorem le_of_comm {B : C} {X Y : Subobject B} (f : (X : C) ⟶ (Y : C)) (w : f ≫ Y.arrow = X.arrow) :
    X ≤ Y := by

So that the conclusion is X ⟶ Y. If we need this result, at some point, then we just use .leOfHom.

My claim is that delaying the introduction of the order api (as above) will allow to not have to duplicate the api, while having an almost as good api for both languages (precisely, it will be just a .leOfHom/etc worse when working with the order api, compared to having both poset and category api). Part of the glue that should be there (and is) between the two languages includes the poset instance of Subobject X.

[Fernando Chu]

For another example, I'd ague against showing this in the Subobject folder

instance semilatticeInf {B : C} : SemilatticeInf (Subobject B) where

Instead, we can translate it to category language as

instance : HasBinaryProducts (Subobject B) where

And then delay the introduction of order api by showing that HasBinaryProducts implies SemilatticeInf for a poset (which would then not reference Subobjects at all).

[Yaël Dillies]

But surely this should go the other way around? Any inf-semilattice has binary products

[Fernando Chu]

This is also true, I'm PRing both statements here. The point is that if we want to avoid duplication of api, one choice of language has to be made; for reasons I've explained above I suggest such choice should be the category language.

[Fernando Chu]

To clarify why I suggest that we want that HasBinaryProducts implies SemilatticeInf instead of the other way around: Currently the SemilatticeInf instance on subobjects is obtained by constructing a product in MonoOver, and then lowering this bifunctor to

def inf {A : C} : Subobject A ⥤ Subobject A ⥤ Subobject A :=

and then showing that this bifunctor is the inf.

Instead, with my suggestion this is unneeded. A one liner shows Subobject has products, from the fact that MonoOver has products, and so it immediately has an inf. This pattern reoccurs with all constructions.

[Aaron Liu]

does this mean typeclass search for SemilatticeInf will wander into category theory?

[Joël Riou]

Fernando Chu said:

To clarify why I suggest that we want that HasBinaryProducts implies SemilatticeInf instead of the other way around

This is not going to work: SemilatticeInf contains data while HasBinaryProducts does not.

[Fernando Chu]

Aaron Liu said:

does this mean typeclass search for SemilatticeInf will wander into category theory?

Yeah this does seem a bit weird to me. We could have this as a def instead (which is what my other PR does).

[Fernando Chu]

Joël Riou said:

Fernando Chu said:

To clarify why I suggest that we want that HasBinaryProducts implies SemilatticeInf instead of the other way around

This is not going to work: SemilatticeInf contains data while HasBinaryProducts does not.

It does, in the sense that I can make this definition.

[Fernando Chu]

The Limits.prod already gets the data out of a Prop. It is true that with the current approach we get a specific inf whereas with the suggested change you a random one, but of course this does not matter, they are equal since Subobject is skeletal.

[Jovan Gerbscheid]

What do people think about merging the to_dual PR, adding some support to to_additive for removing universe parameters, making a new translation attribute cat_to_ord, and then having this API in both forms automatically?

[Jovan Gerbscheid]

Alternatively, we could allow Prop morphisms in category theory, making the two forms equal by rfl, but that is a whole different discussion.