Cohomology Ring of S2 \/ S4

[thomas-lamiaux]

PR to compute the cohomology ring of S2 / S4 which should be Z[X,Y]/<XY, X², Y²>

For CP2 / S2 / S4, this should give an example where the groups are the same but the ring are different. This is example can be seen as better than Torus / S2 / S1 / S1 as :

• H*(T^2) is complicated and not yet formalized
• I don't know any nice form of H*(S2 / S1 / S1)
• H*(CP2) and H*(S2 / S4) are nice

[thomas-lamiaux]

@aljungstrom @mortberg On this proof, the function gets more complicated, as there is 2 variables, there is 3 trivial cases This annoying because, the proof of the cup-product become hard to follow. Indeed, most cases are pointless, but we have to open the term (rec) for stuff to compute, to 0 \equiv 0.

Maybe add a partition on the direct sense ? But then it would be complicated to prove retraction. So there is probably nothing more to do without tactics, except proving had hoc lemma which wouldn't really change much

[thomas-lamiaux]

Hi @mortberg and @aljungstrom, I have spend two days computing S2 \/ S4 because it is a simpler example. So the ring is Z[X,Y]/<XY, X², Y²>.

Though I have a very weird issue. When I am working, I import the equivalence and introduce notation e₀ = invGroupIso H⁰-S²⋁S⁴≅ℤ, ϕ₀, ϕ₀str, ϕ₀⁻¹, ϕ₀⁻¹str, ϕ₀-sect, ϕ₀-retr so it is easier to work.

When proving retraction, I have to prove ϕ₄⁻¹ (ϕ₄ a) = a, so I just want to call ϕ₄-retr. But weirdly he never manage to refine. Even weirder, it works for ϕ₀, and ϕ₂, and for ϕ₄-sect ! So I have checked, the RAM doesn't get saturated or anything, so it is type checking. So I have tried the following

Foo : a -> ϕ₄⁻¹ (ϕ₄ a) = a, 
Foo = { leftInv }

And this won't refine ! So I have tried adding the type explicitly which I wasn't doing before . Doesn't change a things, it looks like it is unfolding the phi function and retyping it to see if indeed they are of the form A -> B // B -> A. But even so, why would it work for the phi 0 and 2, the definition are basically the same. Maybe the recursive call increase the size but the RAM doesn't move at all so the term shouldn't be that big, et from the definition, I would have said it would increase by not much more than x4. So I shouldn't see the difference. So I don't get it

At the end, I finished by putting everything in a ad hoc module and just pass it as a parameter as it seems that the issue is in leftInv. Work perfectly, but why ???

I mean, the file work this way, so it can be kept this way but this annoying as you loses the computation of phi_4 when doing that, hopefully I don't need them here but still

[mortberg]

I fixed the conflicts. Will merge once the CI is finished