limits and choice

Stream: maths

[Johan Commelin]

Currently limit-like classes in category theory are defs, because they care some data (things like has_limits, has_kernels, and all their friends). However, we also proclaim the category-theoretical philosophy, that really you shouldn't care how those limits are constructed/defined.
Would it be an option to make all those classes Props and simply use classical.choice to extract objects/morphisms. This would solve all the diamond and inheritance issues.
We would then need things like is_product Type (X \times Y) to relate the "nice" objects/definitions to whatever classical.choice spits out. But that isn't different from today, because currently X \times Y is not the categorical product in Type.
(I think Reid at some point suggested to me that we might want to consider something like :up:)

[Johan Commelin]

@Scott Morrison @Markus Himmel @Bhavik Mehta @Reid Barton

[Markus Himmel]

Why would we need is_product? Right now we use is_limit for this (i.e., is_limit says that some cone is a limit cone. has_limit then says that we have chosen a particular limit cone). Are you suggesting to change/remove is_limit?

[Johan Commelin]

Sure, but we also need specialised versions, because you don't want to build a cone for a product by hand, you just want to give two morphisms.

[Markus Himmel]

Right, but I think this is orthogonal to the question whether has_limit should be a Prop.

[Johan Commelin]

Right... but it becomes more important because we really can't fall back on the definition anymore.

[Johan Commelin]

And making has_limit a Prop will solve a bunch of defeq issues.

[Bhavik Mehta]

I disagree that this matches the category theoretical philosophy, since that usually tries to avoid choice anyway. I also haven't had any issues with defeq in has_limit, so I don't see much of an advantage to this, and it has the cost of making the category library different from the standard maths way of doing it

[Bhavik Mehta]

Plus as you say, there would need to be statements relating the nice definitions to the ones choice gives, which is no nicer than what we have now

[Bhavik Mehta]

I think the right way of doing this is just to make it easy to move along equivalences and isomorphisms (some of Scott's recent PRs do this already)

[Johan Commelin]

It would be nicer for type class inference

[Bhavik Mehta]

But I haven't had any problems with type class inference - my point of view is that I've used the category theory library a lot, and I've done at least graduate level maths using it and at no point did I have any issues like these

[Johan Commelin]

That's partly because we are making things defs that could be instances in the Prop scenario, I guess.

[Bhavik Mehta]

Right - my point is it hasn't made doing the maths any harder than it would be outside of Lean

[Reid Barton]

It has though

[Reid Barton]

For example, https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/typeclass.20instances.20help/near/195185198

[Johan Commelin]

Thanks for digging that one up

[Bhavik Mehta]

Right, but that was me not understanding what extends does rather than something fundamental about Prop

[Reid Barton]

Huh? wasn't it a standard example of too many instances?

[Bhavik Mehta]

I don't think so - I fixed it just by shuffling how I used extends and everything worked like I wanted

[Reid Barton]

This is just by chance though

[Bhavik Mehta]

Perhaps, but it's not an example of the proof being harder than outside lean, it's an example of me working with extends for the first time

[Reid Barton]

There's no shortage of other examples but I don't feel like digging them up.

[Reid Barton]

Seems like almost every category theory PR adds another bad instance. It's obvious that the people writing the library think they want these instances but it simply won't work unless you make these classes Props or delete all the instances.

[Reid Barton]

Also, regarding choice, I think it's incorrect to say that we know how to do category theory without choice, but I don't want to go through this argument again.

[Reid Barton]

In any case, it is a lot less convenient than using choice.

[Johan Commelin]

@Scott Morrison What do you think about this? How much value do you see in data-carrying instances over Prop-versions?

[Bhavik Mehta]

I think it could be valuable to have a branch of mathlib in which the Prop-versions are used to see how they compare - my view right now is that I don't see any advantage to switching since in my experience I haven't had any issues, but there could well be disadvantages which we're not yet aware of, and of course the code breakage that would come with a refactor

[Scott Morrison]

Sorry, I'll be off zulip for a couple of days. I think we should investigate this, though.

[Scott Morrison]

Something I would like to do soon is refactor the limits/limits.lean file, separating the "is" and "has" stuff into (at least) to files. Perhaps after that it will be easier to try things out.

[Scott Morrison]

I'm absolutely sympathetic to Reid's complaints, but also don't really know how to "get from here to there" --- I'm happy to take suggestions about concrete things to try out that would start improving the situation.

[Markus Himmel]

I started experimenting on the prop_limits branch. I went with the following: The class that is called has_limits on master was changed into a structure limit_data (which should probably be ranamed to limit_cone):

structure limit_data (F : J ⥤ C) :=
(cone : cone F)
(is_limit : is_limit cone)

has_limits now refers to the fact that there is some limit_data:

class has_limit (F : J ⥤ C) : Prop :=
mk' :: (exists_limit : nonempty (limit_data F))

Using choice, we can then recover the usual API:

def get_limit_data (F : J ⥤ C) [has_limit F] : limit_data F :=
classical.choice has_limit.exists_limit

def limit.cone (F : J ⥤ C) [has_limit F] : cone F := (get_limit_data F).cone

def limit.is_limit (F : J ⥤ C) [has_limit F] : is_limit (limit.cone F) :=
(get_limit_data F).is_limit

There is also a new convenience function has_limit.mk:

def has_limit.mk {F : J ⥤ C} (d : limit_data F) : has_limit F :=
⟨nonempty.intro d⟩

Now, as long as no definitional properties are used, everything stays the same, except that

1. we have to write instance : has_limit F := has_limit.mk { ... } instead of instance : has_limit F := { ... }.
2. every definition that uses a limit in some way becomes noncomputable.

I have fixed all errors in category_theory/limits/* and also some other files. Observations:

• Few things break

• So far, I have found three areas that would need serious attention:

  1. Biproducts were set up in a way that relies heavily on definitional properties of low-priority instances for has_product and has_coproduct. Personally, I think this abused the limits API, but I admit that it allowed to reuse some simp lemmas from binary_products.lean. I have rewritten this file to use is_limit rather than has_limit (after all, this is what is_limit is for: we care about a specific limit cone) and it works fine.
  2. Concrete limits might have to be rewritten (again). I only looked at algebra/category/Mon/limits.lean, but it uses lemmas like types.types_limit_\pi, who make general statement about has_limit in Type which simply don't make sense if we interpret has_limit as "there is some limit". In my opinion these lemmas should be rephrased to concern the is_limit we explicitly construct for Type, and then Mon/limits.lean would have to be rewritten to use is_limit rather than has_limit from Type.
  3. Similarly, monoidal/of_has_finite_products.lean doesn't make any sense any more and would have to be rewritten to be monoidal/of_is_finite_product.lean.

[Markus Himmel]

Personally, I believe that finishing this refactor would be worthwhile, but I realize that my interpretation of has_limit is rather extreme and that the fact that everything is noncomputable might be a problem for some people (it isn't for me). I'd be happy to hear everyone's thoughts.

[Bhavik Mehta]

One advantage of this is that we can get the result that binary products + terminal gives finite products

[Bhavik Mehta]

If this change goes through, will is_left_adjoint also change to an exists? I would think so, so that we can express the equivalence between having limits and the diagonal having an adjoint

[Bhavik Mehta]

Relatedly for ess_surj (though I'm in favour of this becoming a Prop regardless of whether has_limits is a Prop)

[Kevin Buzzard]

In some weird way I like the idea that limits should be noncomputable, won't this encourage people to use only their universal properties? Which is what we want when we want to rewrite along canonical isomorphisms

[Bhavik Mehta]

It makes stuff like prod_functor noncomputable though, which means cartesian_closed needs choice to be defined

[Markus Himmel]

If you want your definition of cartesian_closed to depend on a specific product, you can still change the definition to take the limit cones you want rather than requiring has_finite_products

[Bhavik Mehta]

Yeah I think this is a good option conceptually, I wonder how nice it would be in practice though

[Jalex Stark]

isn't making it irreducible enough to make people use the universal properties?

[Markus Himmel]

Yes, but the advantage of also making it a Prop is that we can stop worrying about typeclass diamonds or multiple instances in general

[Bhavik Mehta]

Another consequence of this is that it would make the monadicity theorems (in particular both 1.3 and crude version here: https://ncatlab.org/nlab/show/monadicity+theorem, and my Lean implementation of the latter here) use the axiom of choice - I highlight this example in particular because most category theory texts state this without saying that choice is used while explicitly singling out the use of choice to show that full faithful essentially surjective functors define an equivalence

[Scott Morrison]

@Markus Himmel, thank you for this experiment! It sounds really promising, and I'd love to see it finished.

[Scott Morrison]

I'm not exactly sure from your report where you're up to. I'm very happy if you want to take charge --- and if there are concrete things I can do on a branch "rewrite this file to do XYZ", please tell me!

[Markus Himmel]

@Scott Morrison I've been thinking about biproducts.lean and monoidal/of_finite_products.lean. When I started working on the refactor, I thought that the only "correct" way to use has_limit is to express that there exists some limit, and we're not going to assume any definitional properties about it. However now I realize that another way to interpret has_limit is to just use it to avoid having to pass in limit cones as explicit parameters all the time. This is how it is used in the two files mentioned above.

I converted biproducts.lean to pass in the limit cones explicitly, and it wasn't horrible, but one thing we did lose is that some lemmas that formerly could just be reused from finite (co)products had to be restated for biproducts.

So far, I haven't been able to come up with a construction that also allows for the second use case of has_limit (i.e., a new type class called something like chose_limit) that avoids having to state the entire API twice (or three times, depending on whether you count the theorems stated in terms of is_limit). If you can think of some way to do this, I'd be very interested to hear it.

The alternative would be to explore how tedious it really is to pass in all limit cones. I think starting to rewrite monoidal/* (starting with monoidal/of_finite_products.lean) could be a good indicator of whether this approach is feasible, but I'm not at all familiar with that directory, so if you could have a look, that would be very helpful. If you do have a look at this, make sure to merge master first; there was a bug in the simps tactic that was triggered by the new has_limit typeclass, but it is fixed in master.

[Scott Morrison]

Sorry I haven't got to this yet. I haven't forgotten, and would really like to see if we can make this work!

[Scott Morrison]

I just merged master and resolved conflicts.

[Scott Morrison]

Hmm... Yeah. While I'm absolutely sympathetic to the idea that we want to distinguish between merely existing limits and chosen limits, I don't think we're going to be able to survive entirely without chosen limits.

[Kevin Buzzard]

I definitely want to be able to choose limits sometimes. It should be like localisation -- we should follow @Amelia Livingston . One should be able to choose limits but also have an existence statement, an API for limits developed entirely from the universal property, and a proof that the limits satisfy the universal property. I am hoping that this covers all use cases in a reasonable way.

[Reid Barton]

The question is whether you want a type class that provides chosen limits, and if so, is there any way to get people to stop writing instances for that class.

[Scott Morrison]

How about we

1. keep has_limit as in Markus' branch, as a Prop
2. introduce a chosen_limit typeclass
3. write all the limit F and friends definitions in terms of chosen_limit (don't panic yet!)
4. provide an instance has_limit ---> chosen_limit that uses choice
5. forbid (perhaps even in the linter) creating any other global instances of chosen_limit

This would mean that when you just write limit F, Lean will go looking for a chosen_limit F, and in most circumstances obtain this from a has_limit F class.

However you would have the option, in a single file, to introduce some particular chosen_limit instances locally, and then limit F would be definitionally whatever is provided by those?

[Reid Barton]

So how would this work in the context of something like cartesian_closed? We take a category with has_products and not chosen_products right?

[Reid Barton]

in the definition of cartesian_closed itself

[Reid Barton]

Otherwise, when you go and prove that Type is cartesian closed, you're liable to inadvertently leak your chosen_products in the instance argument of cartesian_closed

[Reid Barton]

@Kevin Buzzard The analogy that comes to my mind is fintype: locally we might want to know what instance we have so that we can compute explicitly, but globally we know the choices don't matter and don't want to be bothered with the coherence issues.
In category theory the coherence issues ought to be even worse because the different possible instances of has_limits are not even equal; but we haven't seen them in practice because category theory is not used much compared to fintype.

[Kevin Buzzard]

I think that I am fully aware as a mathematician that the two universal modules for trilinear maps are $(M\otimes N)\otimes P$ and $M\otimes (N\otimes P)$ and that I have to be careful because these things are not equal. Isn't there a whole theory of coherence here, which people actually do research into instead of just being annoyed by?

I can see that in theory has_limits has the potential to be annoying. However it doesn't seem to have annoyed people in practice yet, in contrast to fintype, and the "fix" is clear -- for unsubtle coherence issues the trick is to build the API so that it works on anything with the right universal property, and for subtle ones you're interested in the lack of coherence anyway.

[Reid Barton]

It's annoyed me a heck of a lot

[Kevin Buzzard]

e.g. for schemes we used R[1/fg] and then when we needed R[1/f][1/g] we just showed that it satisfied the universal property of R[1/fg] and because we weren't pushing things too far it worked fine. But we really needed concrete limits to define affine schemes; the thought of trying to make them well-defined "up to isomorphism" sounds a bit terrifying.

[Kevin Buzzard]

I see -- so you're using category theory in your own work and are seeing problems? :-/

[Reid Barton]

No, it seems clear to me that the same story as with fintype will play out but I was apparently unable to prevent people from going down this path, so I pretty much gave up on formalizing category theory for now.

[Reid Barton]

Let's say a category is "good" if binary products commute with colimits in each variable--surely there are no subtle coherence issues here, and this is just a property of a category. But in Lean the meaning of this statement depends on which colimits and which products are the "chosen" ones. If you somehow end up with a different choice of products, then you've got coherence problems.

[Reid Barton]

And there are loads of instances like "any category with X and Y limits also has Z limits", so it's quite likely you could end up with different instances.

[Reid Barton]

To be fair there really is an easy theorem to be proved here, namely that this property doesn't depend on the choice of products and colimits.

[Bhavik Mehta]

When I've used statements like this, the point is just to state them in terms of is_limit and is_colimit - which is the usual mathematical meaning of this sort of statement anyway, for instance: https://ncatlab.org/nlab/show/pullback-stable+colimit, alternatively here

[Reid Barton]

I agree that the is_* notions are in general much better, but this was just a random example and I'm not sure it is really always convenient to phrase things in terms of them--take cartesian_closed for example

[Reid Barton]

Let me be clear that I don't know what the best way is to handle these issues with limits, and in general things that are determined uniquely (up to unique isomorphism) by universal properties; and there are real problems to be solved about how to express and/or automate the invariance of notions under isomorphism. I only know that the current mathlib approach of writing loads of overlapping instances and using priorities and local instance is the wrong one.

[Kevin Buzzard]

I see -- with these recent messages I've now understood far better what the situation is.

In the definition of the Picard group of a ring you first make the category of modules over that ring, and then quotient it by isomorphism, so you lose information here but you do gain a monoid structure. All your limits are defeq in this quotient structure. Aah.

[Scott Morrison]

I'm not sure if you saw, @Reid Barton, but things did hopefully get a bit better recently in #3603, which removed lots of the has_X typeclasses, replacing them with abbreviations for pi-types producing a has_limit.

[Scott Morrison]

Have you had a look at the prop_limits branch?

[Scott Morrison]

It seems pretty close to working. The two things that we'll lose / have to redo from scratch are:

1. the constructions of limits in Mon/Group/Ring, etc, (which relies on looking at the definition of limits in Type)
2. the equivalence Mon_ (Type) ~ Mon, which relies on looking at the particular choice of binary products and terminal object used when putting a monoidal structure on Type.

[Scott Morrison]

Otherwise it looks like prop_limits is viable. I'm guessing you agree it would be a step in the right direction?

[Scott Morrison]

Of course there's no harm in just ditching Mon_ (Type) ~ Mon at this point; it's a new addition not used anywhere.

[Scott Morrison]

We can redo it by building a bit more API around limits in concrete categories, I guess, and just rely on the universal properties without using the definition of the tensor product in Type as cartesian product.

[Scott Morrison]

If you wanted to have a look at how we could redo the constructions of limits in concrete categories in the prop_limits branch, that would be great!

[Scott Morrison]

Oh, and I guess there are still problems in

3. cartesian_closed, which I didn't look at.

[Scott Morrison]

Reid Barton said:

So how would this work in the context of something like cartesian_closed? We take a category with has_products and not chosen_products right?

Yes.

But on the other hand in monoidal_of_has_finite_products I think we would want chosen_products, so that when someone uses that def to make a particular instance, they can specify definitionally exactly which product they want to use.

[Scott Morrison]

@Reid Barton, I'm not sure if I should proceed with my suggestion (that is, a propositional has_limit, and an evil non-unique data-carrying chosen_limit, with instance using classical.choice from has_limit to chosen_limit, but other instances forbidden, except for local overrides).

I would really like to get this all to a state you're happy with, but if I'm going to be writing the code it would be good to know ahead of time if you think it's a plausible route.

The other alternative as I understand is to _only_ have a propositional has_limit, which will then require complete rewrites of the has_limits instances for algebraic categories, and (very minor) redoing Mon_ (Type) ~ Mon.

[Scott Morrison]

Obviously I'd do this in a branch forking off Markus' prop_limits branch, so there's no commitment, I just want to know whether I'd be wasting my time.

[Scott Morrison]

In the meantime, I'll see if I can get algebra/category/Mon/limits.lean to work with the purely propositional version of has_limits. It seems doable, but I've get derailed in debugging a problem with transport.

[Scott Morrison]

I'm not there yet, but I'm now pretty confident that algebra/category/Mon/limits.lean and all its descendants will work just fine with the propositional has_limit.

[Bhavik Mehta]

Vaguely related to this, is there a reason equivalence_of_fully_faithfully_ess_surj uses a definition of essentially surjective which contains the data of an inverse functor rather than the mere existence as "essentially surjective" usually means? More specifically, are there any objections to changing this to match the standard definition?

[Scott Morrison]

None at all.

[Bhavik Mehta]

In that case: https://github.com/leanprover-community/mathlib/pull/3821

[Scott Morrison]

I've now managed to make all the constructions of limits in concrete categories avoid needing to look at the definitions of limits at prior steps. This works in the prop_limits branch, but I also just made #3860 which backports these changes (without touching the definition of has_limits). Hopefully this makes it easier to work on and test prop_limits` or alternatives.

[Johan Commelin]

Thanks so much for doing this!

[Scott Morrison]

The prop_limits branch itself still has a way to go, I think. I'll try to look at it more soon and write a summary of the remaining obstacles, but if anyone feels like hacking on it, that would be fantastic!

[Johan Commelin]

I wish I could help, but there are too many projects going on atm

[Scott Morrison]

Looks like I made life unnecessarily difficult for myself, and @Markus Himmel has explained a simpler way. I'll try again later. :-)

[Scott Morrison]

Okay, this is done properly, per Markus's suggestion, at #3873.