Zulip Chat Archive

Stream: general

Topic: New limits are not computable


view this post on Zulip Simon Hudon (Sep 24 2020 at 17:39):

The new limits in the category theory library are (intentionally I think) non-computable. Now, I'm working on a concrete category that has binary products I can't figure out how to prove:

lemma prod.mk_le  {X Y : ωCPO.{u}} (x x' : X) (y y' : Y) :
  prod.mk x y  prod.mk x' y'  x  x'  y  y' :=

with the definition

noncomputable def prod.mk {X Y : ωCPO.{u}} (x : X) (y : Y) : (X  Y) :=
let a : ωCPO.of punit.{u+1}  X  Y := limits.prod.lift (continuous_hom.const x) (continuous_hom.const y) in
a punit.star

The issue is that it's not clear what the actual type of a product value is.

view this post on Zulip Adam Topaz (Sep 24 2020 at 17:45):

I was thinking about this too recently. Presumably one can use the fact that the forgetful functor to Type preserves limits, and the fact that the usual product of types satisfies the universal property of the categorical product. I havent had a chance to try it out though

view this post on Zulip Bhavik Mehta (Sep 24 2020 at 17:47):

Could you provide a MWE? I can't seem to get the right imports to get your example to work

view this post on Zulip Simon Hudon (Sep 24 2020 at 17:51):

Yes, sorry about that. I'll make one up.

view this post on Zulip Simon Hudon (Sep 24 2020 at 17:52):

@Adam Topaz I think when you move the problem to the category of types, you still have the issue that binary products are not constructive there either

view this post on Zulip Simon Hudon (Sep 24 2020 at 17:55):

@Bhavik Mehta Is this better:

import order.category.omega_complete_partial_order

universes u

namespace category_theory

open omega_complete_partial_order limits

instance : has_binary_products ωCPO.{u} :=
{ has_limit := λ F,
  { exists_limit :=
   { cone := { X := ωCPO.of (F.obj walking_pair.left × F.obj walking_pair.right),
                π := { app := λ X, match X with
                                   | walking_pair.left  := continuous_hom.of_mono preorder_hom.prod.fst (λ c, rfl)
                                   | walking_pair.right := continuous_hom.of_mono preorder_hom.prod.snd (λ c, rfl)
                                   end } },
    is_limit :=
    { lift := λ s, ⟨λ x, (s.π.app _ x, s.π.app _ x), λ x y h, (s.π.app walking_pair.left).monotone h, (s.π.app walking_pair.right).monotone h,
                    λ c, by ext; dsimp; rw continuous_hom.continuous; refl,
      fac' := by rintros s  ; ext; refl,
      uniq' := by intros; ext; dsimp; simp [category_theory.limits.has_binary_products._match_1,  w]; refl } }  } }

noncomputable def prod.mk {X Y : ωCPO.{u}} (x : X) (y : Y) : (X  Y) :=
let a : ωCPO.of punit.{u+1}  X  Y := limits.prod.lift (continuous_hom.const x) (continuous_hom.const y) in
a punit.star

lemma prod.mk_le  {X Y : ωCPO.{u}} (x x' : X) (y y' : Y) :
  prod.mk x y  prod.mk x' y'  x  x'  y  y' := _

end category_theory

view this post on Zulip Bhavik Mehta (Sep 24 2020 at 17:56):

I think you're missing an import - maybe import category_theory.limits.shapes.binary_products at the top - but with that it works, thanks!

view this post on Zulip Simon Hudon (Sep 24 2020 at 17:57):

Ah! Sorry about that, my copy of mathlib isn't clean

view this post on Zulip Bhavik Mehta (Sep 24 2020 at 17:57):

No worries!

view this post on Zulip Simon Hudon (Sep 24 2020 at 18:33):

Any luck?

view this post on Zulip Markus Himmel (Sep 24 2020 at 18:34):

The following might get you on the right track. I'm sorry about how messy it is.

import order.category.omega_complete_partial_order
import category_theory.limits.shapes.binary_products

universes u

namespace category_theory

open omega_complete_partial_order limits

def product_cone (F : discrete walking_pair  ωCPO.{u}) : cone F :=
{ X := ωCPO.of (F.obj walking_pair.left × F.obj walking_pair.right),
                π := { app := λ X, match X with
                                   | walking_pair.left  := continuous_hom.of_mono preorder_hom.prod.fst (λ c, rfl)
                                   | walking_pair.right := continuous_hom.of_mono preorder_hom.prod.snd (λ c, rfl)
                                   end } }

def product_cone_is_limit (F : discrete walking_pair  ωCPO.{u}) : is_limit (product_cone F) :=
{ lift := λ s, λ x, (s.π.app _ x, s.π.app _ x), λ x y h, ⟨(s.π.app walking_pair.left).monotone h, (s.π.app walking_pair.right).monotone h⟩,
                    λ c, by ext; dsimp; rw continuous_hom.continuous; refl⟩,
      fac' := by rintros s  ; ext; refl,
      uniq' := by intros; ext; dsimp; simp [product_cone._match_1,  w]; refl }

instance : has_binary_products ωCPO.{u} :=
{ has_limit := λ F, has_limit.mk _, product_cone_is_limit F }

noncomputable def prod_lift {X Y : ωCPO.{u}} (x : X) (y : Y) : ωCPO.of punit.{u + 1}  X  Y :=
limits.prod.lift (continuous_hom.const x) (continuous_hom.const y)

noncomputable def prod.mk {X Y : ωCPO.{u}} (x : X) (y : Y) : (X  Y) :=
prod_lift x y punit.star

lemma prod.mk_le  {X Y : ωCPO.{u}} (x x' : X) (y y' : Y) :
  prod.mk x y  prod.mk x' y'  x  x'  y  y' :=
begin
  let i : X  Y  ωCPO.of (X × Y) :=
    limits.is_limit.cone_point_unique_up_to_iso (limit.is_limit _) (product_cone_is_limit (pair X Y)),
  split,
  { intro h,
    have : i.hom (prod.mk x y)  i.hom (prod.mk x' y'),
    { exact i.hom.monotone h },
    split,
    { have ha := ((product_cone (pair X Y)).π.app walking_pair.left).monotone this,
      change (i.hom  (product_cone (pair X Y)).π.app walking_pair.left) (prod.mk x y) 
              (i.hom  (product_cone (pair X Y)).π.app walking_pair.left) (prod.mk x' y') at ha,
      simp only [is_limit.cone_point_unique_up_to_iso_hom_comp, binary_fan.π_app_left, prod.mk] at ha,
      change (prod_lift x y  binary_fan.fst _) punit.star 
        (prod_lift x' y'  binary_fan.fst _) punit.star at ha,
      dsimp only [prod_lift] at ha,
      erw [prod.lift_fst, prod.lift_fst] at ha,
      exact ha },
    sorry, },
  sorry,
end

end category_theory

view this post on Zulip Markus Himmel (Sep 24 2020 at 18:36):

There are obviously several (simp) lemmas missing here. Adding them should hopefully make this much less painful. Some of the messiness is also due to the fact that I was discovering what the wCPO category does on the fly.

view this post on Zulip Simon Hudon (Sep 24 2020 at 18:37):

Thanks for putting the time! Actually, we could have gone with the category of preorders without losing the main points

view this post on Zulip Bhavik Mehta (Sep 24 2020 at 18:51):

fwiw, you can do product_cone for cone (pair X Y) and then use one of the constructors for has_binary_products to get the general case, which makes some of the definitions at the beginning easier

view this post on Zulip Bhavik Mehta (Sep 24 2020 at 18:51):

I agree though that constructing an explicit nice limit cone is the way to go

view this post on Zulip Simon Hudon (Sep 24 2020 at 18:57):

If you do it that way, in has_binary_products how to you convert from the limit shape F and pair X Y?

view this post on Zulip Markus Himmel (Sep 24 2020 at 19:04):

has_binary_products_of_has_limit_pair

view this post on Zulip Bhavik Mehta (Sep 24 2020 at 19:31):

Yeah - this is what I meant by one of the constructors - I just couldn't remember the name off the top of my head!

view this post on Zulip Simon Hudon (Sep 24 2020 at 20:08):

Ok I managed to reformulate @Markus Himmel's solution to use cone (pair X Y)

view this post on Zulip Simon Hudon (Sep 24 2020 at 20:08):

To be exact, the binary products definitions

view this post on Zulip Bhavik Mehta (Sep 24 2020 at 20:09):

You can then use binary_fan.mk to make it a bit nicer instead of needing an inline match

view this post on Zulip Simon Hudon (Sep 24 2020 at 20:12):

Can you elaborate?

view this post on Zulip Bhavik Mehta (Sep 24 2020 at 20:17):

I mean you can define product_cone like this:

def product_cone (X Y : ωCPO.{u}) : binary_fan X Y :=
binary_fan.mk
  (continuous_hom.of_mono preorder_hom.prod.fst (λ c, rfl) : ωCPO.of (X × Y)  _)
  (continuous_hom.of_mono preorder_hom.prod.snd (λ c, rfl))

view this post on Zulip Simon Hudon (Sep 24 2020 at 20:19):

Wow! So efficient!

view this post on Zulip Bhavik Mehta (Sep 24 2020 at 20:20):

I notice now it's pretty annoying to need the type signature of one of the morphisms to specify the cone point - maybe it's worth having P as an explicit argument to binary_fan.mk

view this post on Zulip Bhavik Mehta (Sep 24 2020 at 20:20):

But yes there are lots of convenience constructors around these things!

view this post on Zulip Simon Hudon (Sep 24 2020 at 20:21):

And I keep taking the long way around!

view this post on Zulip Bhavik Mehta (Sep 24 2020 at 20:21):

Perhaps this is a sign that we need better documentation :)

view this post on Zulip Simon Hudon (Sep 24 2020 at 20:22):

We could probably have the same binary products for every concrete category, provided that the defining property is closed under products

view this post on Zulip Simon Hudon (Sep 24 2020 at 20:22):

On my side, I tempt to not read a lot of documentation

view this post on Zulip Simon Hudon (Sep 25 2020 at 01:38):

Ok I managed to shrink @Markus Himmel's proof to:

lemma prod.mk_le {X Y : ωCPO.{u}} (x x' : X) (y y' : Y) :
  prod.mk x y  prod.mk x' y'  x  x'  y  y' :=
begin
  let i : X  Y  ωCPO.of (X × Y) :=
    ωCPO.of_prod_iso _ _,
  split,
  { intro h,
    have : i.hom (prod.mk x y)  i.hom (prod.mk x' y'),
    { exact i.hom.monotone h },
    have ha := ((product_cone X Y).π.app walking_pair.left).monotone this,
    have hb := ((product_cone X Y).π.app walking_pair.right).monotone this,
    simp only [continuous_hom.const_apply, prod_lift_binary_fst, prod_lift_binary_snd,  coe_comp, is_limit.cone_point_unique_up_to_iso_hom_comp, binary_fan.π_app_left, prod.mk, category.assoc, ωCPO.of_prod_iso, i] at ha hb,
    simp [ha, hb], },
  { rintro h₀, h₁⟩,
    suffices : i.hom (prod.mk x y)  i.hom (prod.mk x' y'),
    { replace this := i.inv.monotone this,
      simpa using this },
    change _  _,
    simp [prod.mk],
    simp only [continuous_hom.const_apply, prod_lift_binary_fst, prod_lift_binary_snd,  coe_comp, is_limit.cone_point_unique_up_to_iso_hom_comp, binary_fan.π_app_left, prod.mk, category.assoc],
    simp only [ preorder_hom.prod.fst_to_fun,  omega_complete_partial_order.continuous_hom.prod.fst_to_fun],
    simp only [ preorder_hom.prod.snd_to_fun,  omega_complete_partial_order.continuous_hom.prod.snd_to_fun],
    simp only [ @coe_comp ωCPO _ _ _ (ωCPO.of (X × Y)) Y _ continuous_hom.prod.snd star,  @coe_comp ωCPO _ _ _ (ωCPO.of (X × Y)) X _ continuous_hom.prod.fst star],
    simp only [category.assoc, i, ωCPO.of_prod_iso_prod_fst, ωCPO.of_prod_iso_prod_snd, prod_lift_prod_fst, prod_lift_prod_snd, continuous_hom.const_apply, *],
    exact trivial, trivial }
end

With a few lemmas on top. I could probably shrink it further but I'd like to move on to my main proof


Last updated: May 11 2021 at 23:11 UTC