Functor preserving binary products

Stream: Is there code for X?

[Adam Topaz]

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)))

[Scott Morrison]

See the file preserves_binary_products.lean.

[Adam Topaz]

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

[Adam Topaz]

(It's in the shapes.constructions folder)

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Reid Barton]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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