Cokers of morphisms of add_comm_groups

Stream: Is there code for X?

[Kevin Buzzard]

If I have types G and H with add comm group substances and f : G ->+ H a group hom, do we have the cokernel as a type Q equipped with a quotient.lift`-like construction?

@Scott Morrison can this be done with your category theory magic?

[Kevin Buzzard]

I guess I just quotient by the range

[Scott Morrison]

@Kevin Buzzard :

import algebra.category.Group.abelian

noncomputable theory

open category_theory.limits

example (G H : AddCommGroup) (f : G ⟶ H) : H ⟶ cokernel f := cokernel.π f

example (G H K : AddCommGroup) (f : G ⟶ H) (g : H ⟶ K) (w : f ≫ g = 0) : cokernel f ⟶ K :=
cokernel.desc f g w

example (G H K : AddCommGroup) (f : G ⟶ H) (g : H ⟶ K) (w : f ≫ g = 0) :
  cokernel.π f ≫ cokernel.desc f g w = g :=
by simp

[Kevin Buzzard]

What's going on here is that quotients in the category of abelian groups are in some sense a bit easier than general quotients. For general quotients of a type you need to quotient by a relation on the type. For add comm groups you can quotient out by a morphism from another type, because you just quotient by the range of the map (the image, as some call it) in the sense of quotient groups -- the range is normal because everything is abelian. This means that there's some modified universal property which is actually more appropriate when doing some diagram chasing. Then I realised I'd invented the theory of cokernels.

I think that the theory of explicit H^1(G,A) comes out nicely this way. You have cochains (functions from G to A) which contain cocycles (the kernel of a map from the cochains) and then the coboundaries (the image of a map from A, the 0-cochains). The big question is how best to set this package of data up -- should cocycles and coboundaries be types or terms? Subgroups or groups?

[Kevin Buzzard]

I've gone for H1 being the cokernel of the map from A to the type of cocycles, which I've made as a subtype with coercion to function (interestingly I had to avoid lean's subtype because it kept giving me the wrong coercion, it would just coerce to the main type, which was a function, and this confused simp)