Using the fact that a functor preserves limits

Stream: new members

[Jack J Garzella]

Hello, again as part of #maths > Definition of presheaf of modules I'm trying to use the fact that a functor preserves limits to conclude that binary products are isomorphic. I am able to come up with a term of type preserves_limits_of_size G for my functor G, but I have no clue how to use this to conclude something about objects. The tactics tidy, obviously, and simp, and apply_instance don't seem to automatically do this.

I know this should be quite simple, but I'm just very new to the category theory library. Can someone educate me?

Here's the #mwe:

import category_theory.limits.preserves.basic
import category_theory.limits.has_limits
import category_theory.adjunction.basic
import category_theory.closed.cartesian

noncomputable theory

universes u v

open category_theory
open category_theory.limits
open category_theory.adjunction

variables {C : Type u} [category.{v} C] [has_limits C]
variables {D : Type u} [category.{v} D] [has_limits D]
variables (F : C ⥤ D) (G : D ⥤ C) [adj : F ⊣ G]
include adj

lemma RAPL_binary_products (a b : D) : G.obj (a ⨯ b) ≅ (G.obj a) ⨯ (G.obj b)
:=
begin
  have pres : preserves_limits_of_size G,
    by exact right_adjoint_preserves_limits adj,
  -- What goes here?
  -- Pretty sure I should not be unfolding the definition into limit cones
end

[Andrew Yang]

The content of src/category_theory/limits/preserves/shapes/binary_products.lean should help you.

[Junyan Xu]

lemma RAPL_binary_products (a b : D) : G.obj (a ⨯ b) ≅ (G.obj a) ⨯ (G.obj b)
:=
begin
  letI pres : preserves_limits_of_size.{0 0} G := right_adjoint_preserves_limits adj,
  apply category_theory.limits.preserves_limit_pair.iso,
end

[Junyan Xu]

(I used set_option pp.universes true to figure out that I need to put {0 0}.)

[Jack J Garzella]

Ok, when I use set_optoin pp.universes true, I get the error message

invalid apply tactic, failed to synthesize type class instance for
  preserves_limit.{0 0 v v u u} (pair.{v u} a b) G

I see the 0 0 there, but how would I know I need to put it in preserves_limits_of_size?

[Junyan Xu]

You mean you get the error when you omit .{0 0}? If you omit it, you'll see pres : preserves_limits_of_size.{?l_1 ?l_2 v v u u} G in the infoview, and from the error message, you know you want to fill in ?l_1 = 0 and ?l_2 = 0, so you just add .{0 0} to preserves_limits_of_size.

[Jack J Garzella]

I see, it seems I didn't check the assumption. Thanks!