limits as a class?

Stream: Is there code for X?

[Adam Topaz]

Do we have some idiomatic way to do something similar to the following? Should we? (ping @Bhavik Mehta )

import category_theory.limits.is_limit

open category_theory
open category_theory.limits

universe v
variables {C : Type*} [category.{v} C] {J : Type v} [small_category J] (F : J ⥤ C)

namespace category_theory

class has_cone (X : C) :=
(cone : F.cones.obj $ opposite.op X)

def as_cone (X : C) [has_cone F X] : cone F := ⟨X, has_cone.cone⟩

class is_limit (X : C) extends has_cone F X :=
(is_limit : limits.is_limit (as_cone F X))

def π (X : C) [has_cone F X] (j : J) : X ⟶ F.obj j := (as_cone F X).π.app _

lemma w (X : C) [has_cone F X] {j j' : J} (f : j ⟶ j') : π F X j ≫ F.map f = π F X j' :=
  (as_cone F X).w _

def lift (X Y : C) [is_limit F X] [has_cone F Y] : Y ⟶ X := is_limit.is_limit.lift (as_cone F Y)

-- etc...
end category_theory

[Bhavik Mehta]

I don't think this is a great idea, at least not as a typeclass: there could be multiple ways in which an object is a limit and hiding that data in the typeclass system seems not great

[Adam Topaz]

Bhavik Mehta said:

there could be multiple ways in which an object is a limit

Do you have an example in mind?

[Bhavik Mehta]

I like to pass around an is_limit predicate a lot instead, which takes the cone rather than just its point, though I'd need to see your use case to be sure

[Bhavik Mehta]

Not a specific example, but this feels similar to https://ncatlab.org/nlab/show/skeleton#uniqueness_of_constructions

[Adam Topaz]

Yes, of course if you compose with an automorphism of X you can a "new" way to express that X is a limit, but when does this show up in practice? It seems that in practice we always use limit F and the assocaited limit.\pi, limit.lift, etc., API. We can compose limit F with an automorphism, to obtain a "new" way of seeing limit F as a limit. I mostly want a way to have a similar nice API in cases where have some object X which we know is a limit in some other way.

[Bhavik Mehta]

Right, I think the correct thing to do here is for API to take in the entire cone expressing that X is a limit, using the is_limit existing things

[Bhavik Mehta]

For instance, in #8380 we could say that X "is a pullback" and derive that it's initial but we might as well have the pullback data as an explicit argument

[Adam Topaz]

One issue with using the existing is_limit thing is that it's cumbersome to say that C : cone F is a cone whose cone point is X.

[Bhavik Mehta]

My main issue with your code is that it's putting data into the typeclass system, I think it's less objectionable if those are passed around explicitly (or made into Props)

[Adam Topaz]

Yes, I understand, but we put data into classes all the time (e.g. any of the algebraic classes). We don't seem to care that I can put a different ring structure on $\mathbb{Z}$ by composing with some permutation of $\mathbb{Z}$.

[Bhavik Mehta]

Sure, but the statement you give involves equality of objects on paper anyway, right? So it's not a shock that its awkward to work with in Lean

[Bhavik Mehta]

In that case why are all the existing limit classes propositions?

[Bhavik Mehta]

In any case, do you have a specific example where you'd find this useful?

[Adam Topaz]

One example I can think of is for zero obejcts in an abelian category.

[Adam Topaz]

It would be really useful to be able to write [is_zero_object X].

[Bhavik Mehta]

That's reasonable, but in that case the solution is a lot easier since the cone here carries no information other than the raw object; you can adapt is_terminal for is_zero_object

[Adam Topaz]

@Bhavik Mehta I think all the annoying duplication in #8467 would be solved if we had something similar to what I outlined above.