Bifunctor whiskering

Stream: Is there code for X?

[Antoine Labelle]

Do we have this bifunctor version of docs#category_theory.whiskering_right?

variables {α β γ δ : Type*} [category α] [category β] [category γ] [category δ]
example (F : β ⥤ γ ⥤ δ) : (α ⥤ β) ⥤ (α ⥤ γ) ⥤ (α ⥤ δ) := sorry

This could probably even be functorial in F, though I don't think I need that for the application I have in mind.

[Antoine Labelle]

If we have the equivalence (α ⥤ β × γ) ≅ ((α ⥤ β) × (α ⥤ γ)) then this should follow from uncurrying, applying docs#category_theory.whiskering_right, applying this equivalence and then currying back.

[Andrew Yang]

We have docs#category_theory.functor.prod' , but I don't think we know that it is functorial / is an equivalence.

[Andrew Yang]

We do have docs#category_theory.nat_trans.prod though.

[Antoine Labelle]

I tried doing the equivalence (α ⥤ β × γ) ≅ ((α ⥤ β) × (α ⥤ γ)) but I'm stuck at giving unit_iso. Here is my code if someone wants to give it a shot.

import category_theory.products.basic

open category_theory

universes u₁ u₂ u₃ v₁ v₂ v₃

variables {A : Type u₁} [category.{v₁} A]
          {B : Type u₂} [category.{v₂} B]
          {C : Type u₃} [category.{v₃} C]

def functor_prod_functor_equiv : ((A ⥤ B) × (A ⥤ C)) ≌ (A ⥤ (B × C)) :=
{ functor :=
  { obj := λ F, F.1.prod' F.2,
    map := λ F G f, { app := λ X, (f.1.app X, f.2.app X) } },
  inverse :=
  { obj := λ F, ⟨F ⋙ (category_theory.prod.fst B C), F ⋙ (category_theory.prod.snd B C)⟩,
    map := λ F G α,
    ⟨{ app := λ X, (α.app X).1,
       naturality' := λ X Y f, by simp only [functor.comp_map, prod.fst_map, ←prod_comp_fst, α.naturality] },
     { app := λ X, (α.app X).2,
       naturality' := λ X Y f, by simp only [functor.comp_map, prod.snd_map, ←prod_comp_snd, α.naturality] }⟩ },
  unit_iso := sorry,
  counit_iso := sorry }

[Antoine Labelle]

I tried doing convert iso.refl (𝟭 ((A ⥤ B) × (A ⥤ C))) for the unit_iso field and then proving equality of functors through docs#category_theory.functor.ext, but I think that's probably a bad approach since the documentation for docs#category_theory.functor.ext explicitly says that this isn't something that you usually want to use.

[Adam Topaz]

I would use docs#category_theory.nat_iso.of_components

[Adam Topaz]

You (almost) never want to use equality of functors.

[Kevin Buzzard]

Is equality of natural transformations OK? Where are these arcane rules written down?

[Adam Topaz]

Yes those are okay! Because a natural transformation is just a family of morphisms satisfying some prop, and since it's okay to talk about equality of (a family of) morphisms, it's then okay to talk about equality of natural transformations.

[Adam Topaz]

If a functor didn't have some data related to objects then there would be no issue with equality of functors.

[Adam Topaz]

I think the general story is that in an n-category you should only talk about equality of n-cells

[Adam Topaz]

So all bets are off in an infinity category

[Antoine Labelle]

@Adam Topaz How would construct the following equivalence without appealing to equality of functors?

import category_theory.products.basic

open category_theory

universes u₁ u₂ u₃ v₁ v₂ v₃

variables {A : Type u₁} [category.{v₁} A]
          {B : Type u₂} [category.{v₂} B]
          {C : Type u₃} [category.{v₃} C]
          {D : Type u₄} [category.{v₄} D]

example (F : (A ⥤ B) × (C ⥤ D)) : F ≅ (F.1, F.2) := sorry

[Antoine Labelle]

Oh nevermind I can just do { hom := (𝟙 F.1, 𝟙 F.2), inv := (𝟙 F.1, 𝟙 F.2) }

[Antoine Labelle]

Actually I think the following should be added in category_theory.products.basic. What's a good name for it?

example (X : A × B) : X ≅ (X.1, X.2) := { hom := (𝟙 _, 𝟙 _), inv := (𝟙 _, 𝟙 _) }

[Antoine Labelle]

I managed to complete this equivalence. #15445

[Junyan Xu]

(x×y)^z is isomorphic to x^z×y^z in any docs#category_theory.cartesian_closed category according to Wikipedia; maybe we should do it in this generality? And it would give an isomorphism (involving functor equality), not just an equivalence. However I can't find this fact in category_theory.closed.cartesian, and mathlib doesn't know Cat is an example apparently.

[Junyan Xu]

Here are two versions of functor_prod_functor_equiv inspired by the adjunction between × and ⟶ in general cartesian closed categories; one version uses eq_to_iso and another one is closer to #15445. I'm not sure which one is faster and whether eq_to_iso will cause problems downstream.

import category_theory.functor.currying

open category_theory

universes u₁ u₂ u₃ v₁ v₂ v₃

variables (A : Type u₁) [category.{v₁} A]
          (B : Type u₂) [category.{v₂} B]
          (C : Type u₃) [category.{v₃} C]

@[simps] def prod_functor_to_functor_prod : (A ⥤ B) × (A ⥤ C) ⥤ A ⥤ B × C :=
curry_obj $ functor.prod'
  (uncurry.obj $ category_theory.prod.fst _ _)
  (uncurry.obj $ category_theory.prod.snd _ _)

@[simps] def functor_prod_to_prod_functor : (A ⥤ B × C) ⥤ (A ⥤ B) × (A ⥤ C) :=
functor.prod'
  (curry_obj $ uncurry.obj (𝟭 _) ⋙ category_theory.prod.fst B C)
  (curry_obj $ uncurry.obj (𝟭 _) ⋙ category_theory.prod.snd B C)

@[simp] lemma eq_to_hom_fst {X Y : B × C} (h : X = Y) :
  prod.fst (eq_to_hom h) = eq_to_hom (congr_arg prod.fst h) :=
eq_to_hom_map (category_theory.prod.fst B C) h

@[simp] lemma eq_to_hom_snd {X Y : B × C} (h : X = Y) :
  prod.snd (eq_to_hom h) = eq_to_hom (congr_arg prod.snd h) :=
eq_to_hom_map (category_theory.prod.snd B C) h

lemma hom_inv_id' : prod_functor_to_functor_prod A B C ⋙ functor_prod_to_prod_functor A B C = 𝟭 _ :=
begin
  dsimp [prod_functor_to_functor_prod, functor_prod_to_prod_functor, curry_obj, uncurry],
  apply category_theory.functor.ext,
  { intros, ext; simp },
  { rintro ⟨⟨_⟩, ⟨_⟩⟩, simp },
end

lemma inv_hom_id' : functor_prod_to_prod_functor A B C ⋙ prod_functor_to_functor_prod A B C = 𝟭 _ :=
begin
  dsimp [prod_functor_to_functor_prod, functor_prod_to_prod_functor, curry_obj, uncurry],
  apply category_theory.functor.ext,
  { intros, ext; simp }, { rintro ⟨⟩, dsimp, simp },
end

def functor_prod_functor_equiv : (A ⥤ B) × (A ⥤ C) ≌ A ⥤ B × C :=
{ functor := prod_functor_to_functor_prod A B C,
  inverse := functor_prod_to_prod_functor A B C,
  unit_iso := eq_to_iso (hom_inv_id' A B C).symm,
  counit_iso := eq_to_iso (inv_hom_id' A B C) }

@[simps]
def prod.eta_iso (X : B × C) : (X.1, X.2) ≅ X := { hom := (𝟙 _, 𝟙 _), inv := (𝟙 _, 𝟙 _) }

@[simps] def unit_iso :
  𝟭 _ ≅ prod_functor_to_functor_prod A B C ⋙ functor_prod_to_prod_functor A B C :=
nat_iso.of_components (λ F, (prod.eta_iso _ _ F).symm ≪≫ iso.prod
  (nat_iso.of_components (λ _, iso.refl _) $ by { dsimp [curry_obj], simp })
  (nat_iso.of_components (λ _, iso.refl _) $ by { dsimp [curry_obj], simp }))
  (by { intros, dsimp [curry_obj], ext; simp })

@[simps] def counit_iso :
  functor_prod_to_prod_functor A B C ⋙ prod_functor_to_functor_prod A B C ≅ 𝟭 _ :=
nat_iso.of_components
  (λ F, nat_iso.of_components (λ X, prod.eta_iso _ _ _) $
    by { intros, dsimp [curry_obj], ext; simp })
  (by { dsimp [curry_obj], tidy })

def functor_prod_functor_equiv' : (A ⥤ B) × (A ⥤ C) ≌ A ⥤ B × C :=
{ functor := prod_functor_to_functor_prod A B C,
  inverse := functor_prod_to_prod_functor A B C,
  unit_iso := unit_iso A B C,
  counit_iso := counit_iso A B C,
  functor_unit_iso_comp' := by { intro, dsimp [curry_obj], ext; simp } }

[Yaël Dillies]

Antoine Labelle said:

Actually I think the following should be added in category_theory.products.basic. What's a good name for it?

example (X : A × B) : X ≅ (X.1, X.2) := { hom := (𝟙 _, 𝟙 _), inv := (𝟙 _, 𝟙 _) }

The corresponding non-category statement is docs#prod.mk.eta.

[Junyan Xu]

And the original desired construction can be achieved more directly as

import category_theory.functor.currying
open category_theory
variables {α β γ δ : Type*} [category α] [category β] [category γ] [category δ]
example (F : β ⥤ γ ⥤ δ) : (α ⥤ β) ⥤ (α ⥤ γ) ⥤ (α ⥤ δ) :=
curry_obj $ curry_obj $ functor.prod'
  (uncurry.obj $ category_theory.prod.fst _ _)
  (uncurry.obj $ category_theory.prod.snd _ _) ⋙ uncurry.obj F

[Antoine Labelle]

Nice! It would be great to have the full functorial version though.

[Antoine Labelle]

#15504