Zulip Chat Archive

Stream: maths

Topic: get_limit_cone


view this post on Zulip Scott Morrison (Sep 21 2020 at 07:06):

Hi @Markus Himmel (and any other category theorists here at the moment!)

I'm running into some annoying problems with get_limit_cone --- just that there isn't a good simp normal form set up at the moment. I'm seeing things like (get_limit_cone F).cone.X appearing, which of course is definitionally equal to just limit X.

Options:

  1. I add the simp lemmas that reduce projections of get_limit_cone to the "canonical" ways of summoning these objects.
  2. I just remove the limit_cone structure entirely, in favour of a sigma type.

Any preferences?

view this post on Zulip Markus Himmel (Sep 21 2020 at 07:13):

Personally, I imagined that the library would slowly migrate from having parameters like {c : cone F} (hc : is_limit F) to (c : limit_cone F), so I'm in favor of having something called limit_cone. I'm not 100% sure how your sigma type idea would look.

view this post on Zulip Scott Morrison (Sep 21 2020 at 08:22):

Sounds good. I will add some simp lemmas as I need them.

view this post on Zulip Reid Barton (Sep 21 2020 at 10:37):

I wonder whether this will result in too many ways to say the same thing? You can't really get rid of is_limit since it's needed for most theorems where it appears in the conclusion. Of course for hypotheses this can't cause too much trouble, since you can always write \<c, hc\> where you would write hc before (or c could even be implicit in the limit_cone structure), though Lean's automation might find this slightly challenging.

view this post on Zulip Reid Barton (Sep 21 2020 at 10:46):

I'd guess that more than half the time when you know something is a limit, it's not because you got it from limit or from a hypothesis, but rather you had the cone already and then checked it was a limit, either directly, or using some theorem about a functor preserving/reflecting limits, or by pasting pullback squares, etc.

view this post on Zulip Scott Morrison (Sep 21 2020 at 13:34):

It turned out once I got myself straightened out this issue wasn't actually a problem for me today, so I haven't fixed it either way!


Last updated: May 11 2021 at 16:22 UTC