# Zulip Chat Archive

## Stream: new members

### Topic: Explicit coproduct proof for Ab

#### Yakov Pechersky (Aug 22 2023 at 01:58):

I'm trying to learn the category theory formalization in mathlib, and am struggling through the `BinaryCofan`

and `WalkingPair`

constructions. What's the right way to fill in the sorries here?

```
lemma exercise33 {G H : Type _} [AddCommGroup G] [AddCommGroup H] :
HasBinaryCoproduct (C := AddCommGroupCat) (.of G) (.of H) := by
constructor
refine' ⟨⟨.of (G × H), _⟩, _⟩
· refine' ⟨_, _⟩
· rintro (_|_)
· exact AddMonoidHom.inl _ _
· exact AddMonoidHom.inr _ _
· rintro (_|_) (_|_) f
· simp
· simp
ext g
sorry
· simp
ext h
simp
sorry
· simp
· sorry
```

The maths proof here is I think captured by these two lemmas:

```
lemma exercise33' {G H X : Type _} [AddCommGroup G] [AddCommGroup H] [AddCommGroup X]
(f : G →+ X) (g : H →+ X) : ((AddMonoidHom.coprod f g).comp (AddMonoidHom.inl _ _)) = f := by
simp only [AddMonoidHom.coprod_comp_inl]
lemma exercise33'' {G H X : Type _} [AddCommGroup G] [AddCommGroup H] [AddCommGroup X]
(f : G →+ X) (g : H →+ X) : ((AddMonoidHom.coprod f g).comp (AddMonoidHom.inr _ _)) = g := by
simp only [AddMonoidHom.coprod_comp_inr]
```

#### Adam Topaz (Aug 22 2023 at 02:15):

the key is to also case split on `f`

.

#### Adam Topaz (Aug 22 2023 at 02:33):

BTW, here's how I would go about this (the first two sorries are the other two exercises).

#### Adam Topaz (Aug 22 2023 at 02:33):

Also, just curious, where are these exercises from?

#### Yakov Pechersky (Aug 22 2023 at 02:41):

I tried it this way:

```
lemma exercise33 {G H : Type _} [AddCommGroup G] [AddCommGroup H] :
HasBinaryCoproduct (C := AddCommGroupCat) (.of G) (.of H) := by
constructor
refine' ⟨⟨.of (G × H), _⟩, _⟩
· refine' ⟨_, _⟩
· rintro (_|_)
· exact AddMonoidHom.inl _ _
· exact AddMonoidHom.inr _ _
· rintro (_|_) (_|_) ⟨⟨⟨⟩⟩⟩
· simp
· simp
· refine' BinaryCofan.IsColimit.mk _ _ _ _ _
· intro T f f'
exact AddMonoidHom.coprod f f'
· intro T f f'
exact AddMonoidHom.coprod_comp_inl f f'
· intro T f f'
exact AddMonoidHom.coprod_comp_inr f f'
· rintro T f f' g rfl rfl
sorry -- AddMonoidHom.coprod_inl_inr somehow
```

#### Yakov Pechersky (Aug 22 2023 at 02:44):

I'm glad I worked out to use the `IsColimit.mk`

-- what is tripping me up is that it seems very API-intrusive to resolve some complex

```
⊢ BinaryCofan.inl
{ pt := AddCommGroupCat.of (G × H),
ι :=
NatTrans.mk fun X ↦
WalkingPair.rec (AddMonoidHom.inl (↑(AddCommGroupCat.of G)) H) (AddMonoidHom.inr G ↑(AddCommGroupCat.of H))
X.as } ≫
AddMonoidHom.coprod f f' =
f
```

with just an `exact AddMonoidHom.coprod_comp_inl f f'`

. I understand _why_ it works, I just wish there was some more syntactic-level simplification going on.

#### Adam Topaz (Aug 22 2023 at 02:52):

I think the issue is that you're applying `BinaryCofan.inl`

to a cocone (the stuff in `{...}`

. Binary cofans are defined as some cocones, but there is a special API for them. So this really mixes two APIs, one of which is essentially an alias for the other in a specific case. I also this this is a consequence of using `by constructor ...`

as opposed to building a binary cofan with `BinaryCofan.mk`

.

Last updated: Dec 20 2023 at 11:08 UTC