product of two representable functors

Stream: Is there code for X?

[Kevin Buzzard]

Presumably under mild assumptions, the product of two representable functors is representable (by the product of the representing objects) and probably there are more general statements, such as finite limits of representable functors are representable. Or maybe I mean corepresentable, I am always confused by the ops here. But my question is whether we have the actual correct versions of these theorems? Presumably they are not too hard?

[Joël Riou]

I do not think we have these exact statements. We have some related material though:

• The RepresentableBy/IsRepresentable API in the file CategoryTheory.Yoneda
• yoneda_preservesLimit in CategoryTheory.Limits.Yoneda

Then, if you show that a diagram of representable functors is isomorphic to a composition F ⋙ yoneda, the result should follow.

(In order to even state what you want, you may also use the ClosedUnderLimitsOfShape API from CategoryTheory.Limits.FullSubcategory. Alternatively, if you would like to focus on the binary product case, it would be very reasonable to state and prove things very directly in terms of the RepresentableBy API.)

[Adam Topaz]

exact?% finds the following:

import Mathlib

open CategoryTheory Limits

example {C : Type*} [Category C] [HasLimits C] (X Y : C) :
   yoneda.obj (X ⨯ Y) ≅ yoneda.obj X ⨯ yoneda.obj Y :=
  PreservesLimitPair.iso yoneda X Y