How to define inverse system as a functor?

Stream: new members

[Jiayang Hong]

The inverse system takes type (f : ⦃i j : ι⦄ → i ≤ j → F j → F i), which is not a functor. How can we define a functor F that is an inverse system?

[Aaron Liu]

can you give more context on what you're doing and why you want this?

[Jiayang Hong]

I want to formalize https://stacks.math.columbia.edu/tag/0597. How can I state this lemma?

[Aaron Liu]

I guess first you would have to define the mittag-leffler condition

[Aaron Liu]

oh I see it already exists in mathlib as docs#CategoryTheory.Functor.IsMittagLeffler

[Jiayang Hong]

The Mittag-Leffler condition is defined for a functor, but the inverse system is not defined for a functor. How can I solve this problem?

[Jakub Nowak]

I suspect it's possible to define it as a cofunctor from I to category of sets (or of modules). By I, I mean typical category of a preorder, where there is a morphism between i j : I iff i ≤ j. And if it's a cofunctor, then it is a functor from the Iᵒᵖ category.

[Jiayang Hong]

Is the typical category of preorder already in lean, or I need to define it by myself? I did not find it.

[Matt Diamond]

are you looking for Preorder.smallCategory?

[Matt Diamond]

or the Category of Preorders, which is docs#Preord

[Jiayang Hong]

Thank you. Preorder.smallCategory is what I want.

[Jakub Nowak]

Although if you want to make sure that the statement you write in Lean coincides with the one defined in the link you given, you should define systems/inverted systems and Mittag-Leffler condition independently of what's in mathlib. And optionally define embedding of systems into functors, and prove that the Mittag-Leffler condition you wrote is equivalent to the one in mathlib.

[Aaron Liu]

Jiayang Hong said:

The Mittag-Leffler condition is defined for a functor, but the inverse system is not defined for a functor. How can I solve this problem?

Is an "inverse system" is just a functor where the source is a directed category?

[Edison Xie]

Aaron Liu said:

Jiayang Hong said:

The Mittag-Leffler condition is defined for a functor, but the inverse system is not defined for a functor. How can I solve this problem?

Is an "inverse system" is just a functor where the source is a directed category?

A contravariant functor maybe?

[Aaron Liu]

then it's a functor from the opposite category of a directed category?

[Edison Xie]

or a functor from the order dual of a directed category?

[Edison Xie]

or does it make sense to talk about co-directed sets?

[Jakub Nowak]

Isn't dual a different name for the opposite?

[Aaron Liu]

yes it is

[Aaron Liu]

but we have both docs#Opposite and docs#OrderDual and they're not the same

[Jakub Nowak]

Huh? What's the point of docs#OrderDual ?

[Aaron Liu]

so you can talk about the opposite order

[Jakub Nowak]

Ah, okay, so like LT αᵒᵈ is GT α. There's CategoryTheory.orderDualEquivalence and I guess in the context of category theory it probably makes more sense to use Opposite.

[Edison Xie]

Jakub Nowak said:

Isn't dual a different name for the opposite?

we have OrderDual.instLE but we don't have LE instance for Opposite if your original type has an order

[Jakub Nowak]

I never used OrderDual, but I suspect it might be confusing, at least for me, because now every time you see symbol <, you have to check the type of things being compared to know whether it means < or > in your original order.

[Kevin Buzzard]

But you can see the types of things in the infoview, and we have explicit functions passing from an element in the type to an element in the dual type (we don't abuse defeq) so in practice I've not found it confusing (in contrast to when we used to abuse defeq in the early days and didn't have infoview hover, when it was indeed very confusing).

[Junyan Xu]

For contravariant functors the current practice is indeed to use Opposite instead of OrderDual, see e.g. TopCat.Presheaf.

[Jakub Nowak]

Kevin Buzzard said:

But you can see the types of things in the infoview, and we have explicit functions passing from an element in the type to an element in the dual type (we don't abuse defeq) so in practice I've not found it confusing (in contrast to when we used to abuse defeq in the early days and didn't have infoview hover, when it was indeed very confusing).

Yeah, so by what you described it currently works as I though it does. You still have to hover to see the type. I think it would be nice if delabolator used different symbol for < in OrderDual. But maybe I'm too pedantic.
Also, going back to the context of the systems. I don't currently see any use for the dual order, we only need dual homomorphism. And Opposite works exactly the same as OrderDual, you also have to explicitly convert between original type and the opposite, the only difference being, that Opposite doesn't have order (which we don't need), and I think Opposite is used more commonly in mathlib.

[Jakub Nowak]

Maybe because of how things are defined in mathlib it would be simpler to restate the lemma https://stacks.math.columbia.edu/tag/0597 in terms of systems instead of inverse systems and colimit instead of limit?

[Jakub Nowak]

And one can get the original lemma by applying the new lemma to the Opposite category.

[Kevin Buzzard]

Opposite and OrderDual are used for different things: Opposite is for categories, OrderDual is for orders. I don't think we can have different notation for $<$, it's just LT in each case.

[Jakub Nowak]

For category theorist order is just a special case of category. .-.
I think it is technically possible for delabolator to display a different symbol, it could inspect the type of arguments and check if it's an application of OrderDual.