Explicit coproduct proof for Ab

Stream: new members

[Yakov Pechersky]

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]

the key is to also case split on f.

[Adam Topaz]

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

import Mathlib

open CategoryTheory Limits

def coproductCocone (G H : Type u) [AddCommGroup G] [AddCommGroup H] :
    BinaryCofan (C := AddCommGroupCat) (.of G) (.of H) :=
  BinaryCofan.mk (P := .of <| G × H) (AddMonoidHom.inl _ _) (AddMonoidHom.inr _ _)

def isColimitCoproductCocone (G H : Type u) [AddCommGroup G] [AddCommGroup H] :
    IsColimit (coproductCocone G H) :=
  BinaryCofan.IsColimit.mk _
    (fun a b => AddMonoidHom.coprod a b)
    sorry
    sorry
    sorry


lemma exercise33 {G H : Type _} [AddCommGroup G] [AddCommGroup H] :
    HasBinaryCoproduct (C := AddCommGroupCat) (.of G) (.of H) where
  exists_colimit := .intro <| .mk _ <| isColimitCoproductCocone G H

[Adam Topaz]

Also, just curious, where are these exercises from?

[Yakov Pechersky]

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]

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]

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.