Clean the summary file for pi_4(S^3) = Z/2Z and prove two small general lemmas that were left as holes #707
Conversation
|
Nice! Merge away, I'll fix the conflicts:-) And yes, keeping the module as is and instantiating it later sounds like good idea. |
| open import Cubical.Algebra.Group | ||
| renaming (ℤ to ℤGroup ; Bool to BoolGroup ; Unit to UnitGroup) | ||
| open import Cubical.Algebra.Group.ZAction | ||
| -- TODO: ideally this would not be off by one in the definition of π'Gr |
There was a problem hiding this comment.
@aljungstrom How hard would it be to change this?
|
I don't think divisibility could help much. Only when a systematic treatment of finitely presented abelian group shows up (even for groups generated by one element), these results would find natural places to settle and they can be deduced quickly from general results... |
You're probably right. I'll leave these results in the ZActions file for now then and hopefully one day develop some more general theory |
Proving the "mini lemmas" required me to prove some lemmas that I think could be done nicer with some of the theory of #705. Also a lot of the results I proved ended up in ZActions, but should probably be moved and better integrated with the new theory about divisibility for Z. Maybe @kangrongji would be up for doing this?
@aljungstrom : This will cause some conflicts in the Summary file with #698. I think it would be easier to merge this PR first and then just fix the conflicts in this one file of your bigger PR, what do you think?
It could also be nice to keep the summary module with its arguments and just instantiate the main result afterwards. This way the summary file could be used as a connection between the formalization and the main results in Guillaume's thesis. What do you think?