Ring properties of cup product

agda / cubical

An experimental library for Cubical Agda

https://agda.github.io/cubical/Cubical.README.html

Other

454 stars 139 forks source link

Ring properties of cup product #869

Closed aljungstrom closed 2 years ago

aljungstrom commented 2 years ago

This PR contains

Associativity, unit laws and finished distributivity proofs for the gernalised cup product K(G,n) × K(H,m) → K(G⊗H,n+m). This stuff used to be in Algebra.Group.EilenbergMacLane.CupProduct.agda but has been moved to Algebra.Group.EilenbergMacLane.CupProductTensor.agda. Unfortunately, Github thinks all the code is new, but the relevant lines are (apart from some minor changes): 245-321 and 621-
Introduction of the standard cup product over a ring K(G,n) × K(G,m) → K(G,n+m) the ring laws for a general ring - not necessarily a commutative one (graded commutativity will have to wait a bit). This stuff is now in Algebra.Group.EilenbergMacLane.CupProduct.agda. (This will be the relevant stuff for @thomas-lamiaux)
A bunch of other lemmas, all relating to the above in one way or another.

thomas-lamiaux commented 2 years ago

I was looking at it to define the general cohomology ring. It is a bit of a mess to have that in Algebra. Should this be put in a way or another in a reorganise (and rename) ZCohomology folder ?

thomas-lamiaux commented 2 years ago

Btw, I think that the file with 1500 lines could gain clarity from a (small) header explaining why an operation with tensor is needed to compute the cup product and what is done in the file. Yes it is packed in module, but there is 1500 lines...

thomas-lamiaux commented 2 years ago

@mortberg @aljungstrom Before merging, should we look were to put this ? Because, the Eilengerb-MacLane up to G (so this) is in group, but the same stuff for G = Z is in ZCohomology/RingStructure ? If we want to compute G-cohomology were should we do that ?

aljungstrom commented 2 years ago

@mortberg @aljungstrom Before merging, should we look were to put this ? Because, the Eilengerb-MacLane up to G (so this) is in group, but the same stuff for G = Z is in ZCohomology/RingStructure ? If we want to compute G-cohomology were should we do that ?

I'll put this in Homotopy, because Eilenberg-MacLane spaces do have more applications than just cohomology. Then I'll make an Eilenberg-MacLane folder in Cohomology for the corresponding cohomology theory (as opposed to the stuff that's there now)