Zulip Chat Archive

Stream: Is there code for X?

Topic: Cokers of morphisms of add_comm_groups


view this post on Zulip Kevin Buzzard (Mar 10 2021 at 19:02):

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?

view this post on Zulip Kevin Buzzard (Mar 10 2021 at 19:11):

I guess I just quotient by the range

view this post on Zulip Scott Morrison (Mar 10 2021 at 22:34):

@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

view this post on Zulip Kevin Buzzard (Mar 11 2021 at 07:23):

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?

view this post on Zulip Kevin Buzzard (Mar 11 2021 at 07:30):

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)


Last updated: May 17 2021 at 15:13 UTC