Zulip Chat Archive

Stream: Is there code for X?

Topic: has_limits of has_limits and creates_limits


view this post on Zulip Adam Topaz (Sep 24 2020 at 02:14):

Is there a way to make the following work?

import category_theory.limits.creates
import category_theory.monad.limits

open category_theory

universes u v
variables (C D : Type u) [category.{v} C] [category.{v} D]
variables (F : C  D)
variables [limits.has_limits D] [creates_limits F]

example : limits.has_limits C := by apply_instance -- fails

view this post on Zulip Adam Topaz (Sep 24 2020 at 02:26):

I know I can't expect typeclass search to work, since it has no way of knowing about F, but I would be happy with a def that I can use for the example.

view this post on Zulip Adam Topaz (Sep 24 2020 at 03:02):

Okay, I completed the example with the following:

example : limits.has_limits C :=
λ J I, by letI := I; exact λ G, has_limit_of_created G F ⟩⟩

Is this in mathlib somewhere?

view this post on Zulip Scott Morrison (Sep 24 2020 at 03:29):

Not to my knowledge! Shims like this are definitely useful.

view this post on Zulip Adam Topaz (Sep 24 2020 at 03:30):

I'm playing with it now. It works out well too, e.g. the functor F automatically gets a preserves_limits instance.

view this post on Zulip Bhavik Mehta (Sep 24 2020 at 14:14):

Yeah I agree this should be there as a def

view this post on Zulip Adam Topaz (Sep 24 2020 at 14:26):

@Bhavik Mehta @Scott Morrison #4239


Last updated: May 07 2021 at 22:14 UTC