New limits are not computable

Stream: general

[Simon Hudon]

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.

[Adam Topaz]

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

[Bhavik Mehta]

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

[Simon Hudon]

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

[Simon Hudon]

@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

[Simon Hudon]

@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

[Bhavik Mehta]

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

[Simon Hudon]

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

[Bhavik Mehta]

No worries!

[Simon Hudon]

Any luck?

[Markus Himmel]

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

[Markus Himmel]

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.

[Simon Hudon]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Simon Hudon]

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

[Markus Himmel]

has_binary_products_of_has_limit_pair

[Bhavik Mehta]

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

[Simon Hudon]

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

[Simon Hudon]

To be exact, the binary products definitions

[Bhavik Mehta]

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

[Simon Hudon]

Can you elaborate?

[Bhavik Mehta]

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))

[Simon Hudon]

Wow! So efficient!

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Simon Hudon]

And I keep taking the long way around!

[Bhavik Mehta]

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

[Simon Hudon]

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

[Simon Hudon]

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

[Simon Hudon]

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