# Zulip Chat Archive

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

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

Yes

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

Well that's not good

Last updated: May 06 2021 at 18:20 UTC