problem with binary biproducts

Stream: maths

[Scott Morrison]

@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]

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]

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]

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

[Markus Himmel]

The instances are provably equal, just not definitionally equal

[Reid Barton]

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

[Reid Barton]

However, it would be better to untangle the instances instead

[Markus Himmel]

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]

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

[Reid Barton]

Can you write it in math?

[Reid Barton]

What is prod.lift?

[Markus Himmel]

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]

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]

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

[Markus Himmel]

Yes

[Reid Barton]

Well that's not good