Zulip Chat Archive

Stream: maths

Topic: subquotients

view this post on Zulip Kevin Buzzard (Feb 13 2020 at 12:07):

structure add_subquotient (G : Type*) [add_group G] :=
(bottom : add_subgroup G)
(top : add_subgroup G)
(incl : bottom  top)

instance : has_coe_to_sort (add_subquotient G) := ...

Is this a sensible idea? @Shenyang Wu has a big group of cochains and he wants to take the quotient of the subgroup of cocycles by the subgroup of coboundaries. I think I had an extensive conversation with @Mario Carneiro about the relative merits of this construction a while ago. It's in his repo as of today, so we will find out soon enough :-) (he's proved d2=0d^2=0 so can define the cocycles as the kernel of dd and the coboundaries as the image of dd).

Last updated: May 06 2021 at 18:20 UTC