Abelian infinity groups

[felixwellen]

This PR adds basic definitions for abelian infinity groups.
Type checking did not terminate for my definition of morphisms.

[mortberg]

What is the status of this PR? Did the slow type checking ever go away? If so, maybe we should merge it?

[felixwellen]

It went away, but it should not be merged. It is still too experimental and I want to think about the definitions again (maybe it is better to reorganize stuff). If you have the feeling there are too many PRs around, maybe we should work on how PRs are displayed (e.g. show drafts separately/ordered by most recent activity or something like that).

[UlrikBuchholtz]

Wouldn't it be better to define general spectra first, and then carve out the connective spectra (what you call abelian infinity groups) out from those? (When I read the title, I thought at first it referred to braided infinity groups; maybe it's a bit ambiguous?)

[felixwellen]

I guess braided means there are two deloopings? Would infinitely abelian infinity groups be a good name?
And I agree, it would be better to define (pre-)spectra first, since they will be needed at some point. I was just interested in one particular thing at the time...

[UlrikBuchholtz]

I guess braided means there are two deloopings? Would infinitely abelian infinity groups be a good name?

Exactly, braided is two and sylleptic is three, and then it's just E_k thereafter. Hence E_\infty would be a good name, but infinitely abelian or symmetric would also work. Or just: connective spectra. 😄

And I agree, it would be better to define (pre-)spectra first, since they will be needed at some point. I was just interested in one particular thing at the time...

Yes, since maps of spectra are just maps of the underlying prespectra, it's probably most efficient to do prespectra and then specialize to (loop) spectra and k-connected / n-truncated spectra whatever…

[felixwellen]

This PR will be obsoleted by #589 .