Zulip Chat Archive

Stream: maths

Topic: problem with binary biproducts


view this post on Zulip Scott Morrison (Jun 02 2020 at 08:52):

@Markus Himmel , @Bhavik Mehta, I'm worried something is wrong with our binary biproducts setup.
I'd like to be able to prove

import category_theory.limits.shapes.biproducts

universes v u

open category_theory
open category_theory.limits

variables {C : Type u} [category.{v} C] [preadditive.{v} C]

lemma biprod.inl_map [has_preadditive_binary_biproducts.{v} C] {W X Y Z : C} {f : W  Y} {g : X  Z} :
  biprod.inl  biprod.map f g = f  biprod.inl := sorry

(or indeed the non-preadditive version), but I seem to be completely stuck. Would either of you be able to try this? biprod.map seems ... unusable, but I can't work out why.

view this post on Zulip Markus Himmel (Jun 02 2020 at 09:23):

So biprod.fst is defined via limit.\pi, which requires an instance of has_limit (pair X Y). This instance comes directly from has_binary_biproduct.has_limit_pair. On the other hand, biprod.map gets its instances via has_limits_of_shape (discrete walking_pair). This is a problem, because when we try to prove biprod.inl_map, we eventually want to use limit.map_\pi, which assumes that both map and pi got their instances via has_limits_of_shape, and it appears that the instance that biprod.fst uses is not definitionally equal to that one.

view this post on Zulip Reid Barton (Jun 02 2020 at 11:15):

It doesn't work to just write a big pile of instances and hope for the best. This isn't math, has_foo_limits_of_blah isn't a Prop.

view this post on Zulip Reid Barton (Jun 02 2020 at 11:31):

though I'm a little confused--surely this is provable assuming it typechecks at all

view this post on Zulip Markus Himmel (Jun 02 2020 at 11:38):

The instances are provably equal, just not definitionally equal

view this post on Zulip Reid Barton (Jun 02 2020 at 11:45):

But in any case they're both coproducts, right? So can't you just argue using universal properties?

view this post on Zulip Reid Barton (Jun 02 2020 at 12:06):

However, it would be better to untangle the instances instead

view this post on Zulip Markus Himmel (Jun 02 2020 at 12:09):

I'm sceptical that arguing using unversal properties would work here. In essence, that would amount to claiming that prod.lift f g \gg prod.fst = f, even if lift and fst come from different instances of has_limit, which is of course false in general.

view this post on Zulip Reid Barton (Jun 02 2020 at 12:16):

I'm so confused. Is the notation throwing me off again?

view this post on Zulip Reid Barton (Jun 02 2020 at 12:17):

Can you write it in math?

view this post on Zulip Reid Barton (Jun 02 2020 at 12:18):

What is prod.lift?

view this post on Zulip Markus Himmel (Jun 02 2020 at 12:19):

Given f : X \hom Y and g : Y \hom T, prod.lift f g is the unique map X \prod Y \hom T such that lift f g \gg prod.fst = f and lift f g \gg prod.snd = g.

view this post on Zulip Markus Himmel (Jun 02 2020 at 12:23):

Let's say that we have an object PP that has the universal property of the product of XX and YY in two different ways: With the projections π1:PX\pi_1 : P \to X and π2:PY\pi_2 : P \to Y and with the projections π1:PX\pi_1' : P \to X and π2:PY\pi_2' : P \to Y. Now let f:XTf : X \to T and g:YTg : Y \to T, then by the first universal property we have a unique map l:PTl : P \to T such that lπ1=fl \gg \pi_1 = f and lπ2=gl \gg \pi_2 = g. Then it will in general not be the case that lπ1=fl \gg \pi_1' = f and lπ2=gl \gg \pi_2' = g, which is what we would need to prove biprod.inl_map without sorting out the instances properly.

view this post on Zulip Reid Barton (Jun 02 2020 at 12:23):

Oh you're saying that the objects X×YX \times Y happen to agree, but not the cone maps?

view this post on Zulip Markus Himmel (Jun 02 2020 at 12:24):

Yes

view this post on Zulip Reid Barton (Jun 02 2020 at 12:46):

Well that's not good


Last updated: May 06 2021 at 18:20 UTC