## 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 (_|_)
· 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

(f : G →+ X) (g : H →+ X) : ((AddMonoidHom.coprod f g).comp (AddMonoidHom.inr _ _)) = g := by


#### 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 (_|_)
· rintro (_|_) (_|_) ⟨⟨⟨⟩⟩⟩
· simp
· simp
· refine' BinaryCofan.IsColimit.mk _ _ _ _ _
· intro T f f'
· intro T f f'
· intro T f f'
· rintro T f f' g rfl rfl


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

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