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 so can define the cocycles as the kernel of and the coboundaries as the image of ).
Last updated: May 06 2021 at 18:20 UTC