subquotients

Stream: maths

[Kevin Buzzard]

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 $d^2=0$ so can define the cocycles as the kernel of $d$ and the coboundaries as the image of $d$).