Stream: Is there code for X?
Kevin Buzzard (Mar 10 2021 at 19:02):
If I have types
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 (Mar 10 2021 at 19:11):
I guess I just quotient by the range
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
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?
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