## Stream: general

### Topic: New limits are not computable

#### 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.

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

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

#### Simon Hudon (Sep 24 2020 at 17:51):

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

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

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


#### 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!

#### Simon Hudon (Sep 24 2020 at 17:57):

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

No worries!

Any luck?

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


#### 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.

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

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

#### Bhavik Mehta (Sep 24 2020 at 18:51):

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

#### 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?

#### Markus Himmel (Sep 24 2020 at 19:04):

has_binary_products_of_has_limit_pair

#### 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!

#### Simon Hudon (Sep 24 2020 at 20:08):

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

#### Simon Hudon (Sep 24 2020 at 20:08):

To be exact, the binary products definitions

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

#### Simon Hudon (Sep 24 2020 at 20:12):

Can you elaborate?

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


#### Simon Hudon (Sep 24 2020 at 20:19):

Wow! So efficient!

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

#### Bhavik Mehta (Sep 24 2020 at 20:20):

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

#### Simon Hudon (Sep 24 2020 at 20:21):

And I keep taking the long way around!

#### Bhavik Mehta (Sep 24 2020 at 20:21):

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

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

#### Simon Hudon (Sep 24 2020 at 20:22):

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

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