Zulip Chat Archive

Stream: Is there code for X?

Topic: Functor preserving binary products


view this post on Zulip Adam Topaz (Sep 21 2020 at 13:52):

Is there a preferred way to say that a functor preserves binary products?
Something like this?

def preserves_binary_products {A B : Type*} [category A] [category B]
  [has_binary_products A] [has_binary_products B] (G : A  B) :=
  Π (X Y : A), is_iso (prod.lift (G.map (limits.prod.fst : X  Y  X)) (G.map (limits.prod.snd : X  Y  Y)))

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

See the file preserves_binary_products.lean.

view this post on Zulip Adam Topaz (Sep 21 2020 at 14:17):

Ah thanks. I looked in the preserves folder and didn't find anything.

view this post on Zulip Adam Topaz (Sep 21 2020 at 14:17):

(It's in the shapes.constructions folder)

view this post on Zulip Scott Morrison (Sep 21 2020 at 14:18):

Indeed. That's ... suboptimal. :-)

view this post on Zulip Scott Morrison (Sep 21 2020 at 14:20):

It seems I made the limits/preserves/ subfolder, without being aware that file was already in limits/shapes/constructions/.

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

If you're using either of those files, feel free to clean up / relocate, etc. I may get to it someday. :-)

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

Yeah I've been thinking about moving these files as well - there's quite a bit I want to add about functors preserving things so I think it might be a good idea to shift everything into preserves

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

Also, since we have abbreviations for a category having equalizers etc, do we want abbreviations for a functor to preserve them? So far I've been using preserves_limits_of_shape walking_parallel_pair F and \fo J, preserves_limits_of_shape (discrete J) F etc but they're pretty cumbersome

view this post on Zulip Reid Barton (Sep 21 2020 at 14:49):

Like notation `⇉` := walking_parallel_pair? :upside_down:

view this post on Zulip Bhavik Mehta (Sep 21 2020 at 15:04):

I was thinking more like preserves_equalizers := preserves_limits_of_shape walking_parallel_pair F but I guess preserves_limits_of_shape ⇉ F works and for pullbacks we can use preserves_limits_of_shape →← F

view this post on Zulip Bhavik Mehta (Sep 21 2020 at 15:07):

By the way @Adam Topaz you might like to be aware of: https://github.com/leanprover-community/mathlib/pull/4163

view this post on Zulip Bhavik Mehta (Sep 21 2020 at 15:08):

After that's sorted I've also got a proof of preserves binary products + preserves terminal => preserves finite products too


Last updated: May 19 2021 at 03:22 UTC