General Eilenberg-MacLane spaces (+ some theory)

[aljungstrom]

This PR contains a bunch of generalisation of the stuff in ZCohomology to general Eilenberg-MacLane spaces, K(G,n). There's not that much new really -- all proofs go through in an almost identical manner. There's some stuff left to translate, but it was probably time for a PR...

Here's some of the stuff

• A construction of the tensor product of abelian groups and a proof that it has the universal property. There's commutativity and associativity of tensor products.
• General Eilenberg-MacLane spaces, K(G,n).
• A direct proof of the "wedge connectivity lemma" for these spaces.
• The "group structure" on K(G,n).
• A proof that Ω K(G,n+1) ≃ K(G,n) (for n > 0 -- the case n = 0 was already done by @felixwellen)
• The cup product, defined as a function K(G,n) → K(H,m) → K(G ⊗ H , (n + m)). I'll wait with the non tensor version.
• Left and right distributivity of the cup product. I'll do associativity and graded commutativity later.
• A version of →∙Homogeneous≡ for constructing squares in A →∙ B

[felixwellen]

Very nice! The proof you mentioned was actually done by Ulrik, though....
Are the coefficients constant everywhere? I think it would be a good idea to use dependent coefficients whenever possible. And it is probably a good time to rename 'ZCohomology' to 'Cohomology'. But I guess both can be treated as separate issues.

[aljungstrom]

Very nice! The proof you mentioned was actually done by Ulrik, though.... Are the coefficients constant everywhere? I think it would be a good idea to use dependent coefficients whenever possible. And it is probably a good time to rename 'ZCohomology' to 'Cohomology'. But I guess both can be treated as separate issues.

Damn sorry, I kind of forgot about this PR. Do you remember what you meant by this? I'm a bit uncertain about what dependent coefficients could mean in this context.

[felixwellen]

I'll write an issue.

[felixwellen]

Here it is #616 . I don't think it should be done in this PR, sorry if that stopped anyone from reviewing it.

[ecavallo]

I'm going to review this, but could you merge from master first? I suspect some things are out of date by now.

[ecavallo]

Looks like there's some conflict where isGroupHomInv is now defined in multiple places.

[aljungstrom]

Sorry, should be ok now

[ecavallo]

Have some mainly minor suggestions. I tried to figure out some bigger simplifications but ended up in over my head, haha...

[aljungstrom]

@ecavallo Thanks for the review, and sorry I have been so slow with this. I'll clean this up as soon as this whole pi4s3 business is over.

[ecavallo]

No problem, I was not fast reviewing it either!

[aljungstrom]

FIXED!

░░░░░░░░░░░░░░░░░░░░░░█████████░░░░░░░░░
░░███████░░░░░░░░░░███▒▒▒▒▒▒▒▒███░░░░░░░
░░█▒▒▒▒▒▒█░░░░░░░███▒▒▒▒▒▒▒▒▒▒▒▒▒███░░░░
░░░█▒▒▒▒▒▒█░░░░██▒▒▒▒▒▒▒▒▒▒▒▒▒▒▒▒▒▒▒██░░
░░░░█▒▒▒▒▒█░░░██▒▒▒▒▒██▒▒▒▒▒▒██▒▒▒▒▒███░
░░░░░█▒▒▒█░░░█▒▒▒▒▒▒████▒▒▒▒████▒▒▒▒▒▒██
░░░█████████████▒▒▒▒▒▒▒▒▒▒▒▒▒▒▒▒▒▒▒▒▒▒██
░░░█▒▒▒▒▒▒▒▒▒▒▒▒█▒▒▒▒▒▒▒▒▒█▒▒▒▒▒▒▒▒▒▒▒██
░██▒▒▒▒▒▒▒▒▒▒▒▒▒█▒▒▒██▒▒▒▒▒▒▒▒▒▒██▒▒▒▒██
██▒▒▒███████████▒▒▒▒▒██▒▒▒▒▒▒▒▒██▒▒▒▒▒██
█▒▒▒▒▒▒▒▒▒▒▒▒▒▒▒█▒▒▒▒▒▒████████▒▒▒▒▒▒▒██
██▒▒▒▒▒▒▒▒▒▒▒▒▒▒█▒▒▒▒▒▒▒▒▒▒▒▒▒▒▒▒▒▒▒▒██░
░█▒▒▒███████████▒▒▒▒▒▒▒▒▒▒▒▒▒▒▒▒▒▒▒██░░░
░██▒▒▒▒▒▒▒▒▒▒████▒▒▒▒▒▒▒▒▒▒▒▒▒▒▒▒▒█░░░░░
░░████████████░░░█████████████████░░░░░░

[ecavallo]

fine