Representability of product

Stream: Is there code for X?

[Michał Mrugała]

Let C be a category satisfying [ChosenFiniteProducts C] and F G : Cᵒᵖ ⥤ Type v be functors representable by X Y respectively. Is there a theorem in mathlib that gives us the representability of A ↦ F(A) × G(A) by X ⊗ Y? Is this functor even defined in mathlib?

[Yaël Dillies]

(solved locally)

[Kevin Buzzard]

What's the answer? Ivan my Masters student asked me the same question last month.

[Michał Mrugała]

We only found the answer for how to define it. It's F ⊗ G (defined in general if the target category has finite products).

[Yaël Dillies]

It's proved, after an hour long battle

[Adam Topaz]

I’m pretty sure @Jack McKoen has done all of this somewhere

[Yaël Dillies]

I couldn't find any mention of RepresentableBy in Jack's public repos

[Adam Topaz]

Ok.

import Mathlib

open CategoryTheory MonoidalCategory

universe v u
variable {C : Type u} [Category.{v} C] [ChosenFiniteProducts C]

example (F G : Cᵒᵖ ⥤  Type v) (X Y : C)
    (hF : F.RepresentableBy X) (hG : G.RepresentableBy Y) : (F ⊗ G).RepresentableBy (X ⊗ Y) where
  homEquiv {Z} := {
    toFun := fun f => (hF.homEquiv <| f ≫ ChosenFiniteProducts.fst _ _ , hG.homEquiv <| f ≫ ChosenFiniteProducts.snd _ _)
    invFun := fun f => ChosenFiniteProducts.lift (hF.homEquiv.symm f.fst) (hG.homEquiv.symm f.snd)
    left_inv := by aesop_cat
    right_inv := by aesop_cat
  }
  homEquiv_comp := by
    intro Z W f g
    apply Prod.ext
    · simpa using hF.homEquiv_comp f (g ≫ ChosenFiniteProducts.fst _ _)
    · simpa using hG.homEquiv_comp f (g ≫ ChosenFiniteProducts.snd _ _)

[Joël Riou]

RepresentableBy is a relatively recent introduction to mathlib #17389. We do not have that many definitions that are phrased in terms of RepresentableBy yet. I would suggest the following:

import Mathlib.CategoryTheory.ChosenFiniteProducts.FunctorCategory
import Mathlib.CategoryTheory.Monoidal.Types.Basic

universe w v u

namespace CategoryTheory

open Limits MonoidalCategory

variable {C : Type u} [Category.{v} C]

@[simps apply]
def Limits.BinaryFan.IsLimit.homEquiv {X Y : C} {c : BinaryFan X Y} (hc : IsLimit c)
    {T : C} : (T ⟶ c.pt) ≃ (T ⟶ X) × (T ⟶ Y) where
  toFun f := ⟨f ≫ c.fst, f ≫ c.snd⟩
  invFun g := hc.lift (BinaryFan.mk g.1 g.2)
  left_inv f := BinaryFan.IsLimit.hom_ext hc (by simp) (by simp)
  right_inv g := by simp

def Functor.RepresentableBy.prod {F G : Cᵒᵖ ⥤ Type w} {X Y : C}
    (hF : F.RepresentableBy X) (hG : G.RepresentableBy Y)
    {c : BinaryFan X Y} (hc : IsLimit c) :
    (F ⊗ G).RepresentableBy c.pt where
  homEquiv := (BinaryFan.IsLimit.homEquiv hc).trans (hF.homEquiv.prodCongr hG.homEquiv)
  homEquiv_comp {T U} f g := by
    apply Prod.ext
    · change hF.homEquiv ((f ≫ g) ≫ c.fst) = F.map f.op (hF.homEquiv (g ≫ c.fst))
      simp only [Category.assoc, hF.homEquiv_comp]
    · change hG.homEquiv ((f ≫ g) ≫ c.snd) = G.map f.op (hG.homEquiv (g ≫ c.snd))
      simp only [Category.assoc, hG.homEquiv_comp]

end CategoryTheory

[Yaël Dillies]

:tada: And do you also have the general limit version somewhere?

[Joël Riou]

Not in terms of RepresentableBy, but otherwise it can be phrased by saying that yoneda preserves limits, which is known to mathlib.