## Stream: maths

### Topic: problem with binary biproducts

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

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

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

#### Reid Barton (Jun 02 2020 at 11:31):

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

#### Markus Himmel (Jun 02 2020 at 11:38):

The instances are provably equal, just not definitionally equal

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

#### Reid Barton (Jun 02 2020 at 12:06):

However, it would be better to untangle the instances instead

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

#### Reid Barton (Jun 02 2020 at 12:16):

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

#### Reid Barton (Jun 02 2020 at 12:17):

Can you write it in math?

#### Reid Barton (Jun 02 2020 at 12:18):

What is prod.lift?

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

#### Markus Himmel (Jun 02 2020 at 12:23):

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

#### Reid Barton (Jun 02 2020 at 12:23):

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

Yes

#### Reid Barton (Jun 02 2020 at 12:46):

Well that's not good

Last updated: May 06 2021 at 18:20 UTC