Zulip Chat Archive

Stream: maths

Topic: Instance confusion


view this post on Zulip Bhavik Mehta (Jul 06 2020 at 14:18):

Here's where I'm at right now, and presumably this suggests something has been set up wrong, can anyone help?

import category_theory.adjunction.limits
import category_theory.closed.cartesian

universes v u₁ u₂

namespace category_theory
open category limits
variables {C : Type u₁} [category.{v} C] [has_finite_products C] [cartesian_closed C]
variables {D : Type u₂} [category.{v} D] [has_finite_products D] [cartesian_closed D]
variables (F : C  D)

class cartesian_closed_functor [preserves_limits_of_shape (discrete walking_pair) F] :=
(comparison_iso :  A B, is_iso (exp_comparison F A B))

variables {F} {L : D  C}

def frobenius_map (A : C) (B : D) (adj : L  F) : L.obj (B  F.obj A)  L.obj B  A :=
prod_comparison _ _ _  limits.prod.map (𝟙 _) (adj.counit.app A)

instance (adj : L  F) : preserves_limits_of_shape (discrete walking_pair) F :=
begin
  haveI := adjunction.right_adjoint_preserves_limits adj,
  apply_instance,
end

instance (adj : L  F) [ A B, is_iso (frobenius_map A B adj)] : cartesian_closed_functor F :=
begin

end

view this post on Zulip Bhavik Mehta (Jul 06 2020 at 14:23):

Actually I suppose the point here is that in maths the question of if a functor is cartesian closed first needs binary products to be preserved, and in my case it's a right adjoint so that's fine

view this post on Zulip Bhavik Mehta (Jul 06 2020 at 14:24):

But in lean this inference isn't immediate so it would be sensible to have preservation of binary prods as part of the definition of cartesian closed functor

view this post on Zulip Johan Commelin (Jul 06 2020 at 14:24):

What exactly is the problem? Do you get an error?

view this post on Zulip Johan Commelin (Jul 06 2020 at 14:24):

Also, should the haveI be a letI?

view this post on Zulip Bhavik Mehta (Jul 06 2020 at 14:25):

The instance at the bottom doesn't have a valid statement

view this post on Zulip Bhavik Mehta (Jul 06 2020 at 14:26):

Potentially, I'm not sure it makes a huge difference though since preserving limits is subsingleton

view this post on Zulip Bhavik Mehta (Jul 06 2020 at 14:27):

I've got to step away for a little - I'll continue trying later


Last updated: May 09 2021 at 10:11 UTC