# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeJun 7th 2016

I have added also the statement of the two relative versions of the Serre spectral sequence (here). No details yet.

• CommentRowNumber2.
• CommentAuthorUrs
• CommentTimeJan 8th 2019

and implementation in Lean is in

and will add it also to spectral sequence and maybe elsewhere

• CommentRowNumber3.
• CommentAuthorAli Caglayan
• CommentTimeJan 8th 2019

@Urs it should be Floris et. al. There is a list of participents:

Participants Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead, Egbert Rijke, Mike Shulman.

Checking the contributors supports this fact too.

• CommentRowNumber4.
• CommentAuthorUrs
• CommentTimeJan 8th 2019
• (edited Jan 8th 2019)

all right, I added more of these names. I got the pointer from Floris’ talk at LeanTogether and somehow thought it was the pointer to his

• CommentRowNumber5.
• CommentAuthorUrs
• CommentTimeJul 5th 2021

have made more explicit (here) what it means for the cohomology Serre spectral sequence to converge

• CommentRowNumber6.
• CommentAuthorUrs
• CommentTimeJul 5th 2021

I have added a detailed example computation (here) of

$H^4 \big( S^{\mathbb{H}} \!\sslash\! G, \, \mathbb{Z} \big) \;\; \simeq \;\; \mathbb{Z} \oplus (\mathbb{Z}/\left\vert G \right\vert)$
• CommentRowNumber7.
• CommentAuthorDavidRoberts
• CommentTimeJul 6th 2021

In your proof, where it says’

we have for the given finite subgroup of SU(2) (by this Prop) that:

do you mean to give $H^n$ rather than $H^4$? Otherwise I don’t know what the parameter $n$ on the RHS of the equation is meant to be.

• CommentRowNumber8.
• CommentAuthorUrs
• CommentTimeJul 6th 2021

Thanks. Fixed the “4” to “$n$”.