Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

RP2 #847

Merged
merged 139 commits into from
Sep 12, 2022
Merged

RP2 #847

merged 139 commits into from
Sep 12, 2022

Conversation

thomas-lamiaux
Copy link
Contributor

Add RP2, in progress

thomas-lamiaux and others added 30 commits April 6, 2022 13:57
@thomas-lamiaux
Fix Direct-sum :
3f62a82 
The index and the groups were at the same level.
The should be at different one, for instance if the index is Nat, and the group something else
@thomas-lamiaux
Merge branch 'agda:master' into master
620bfc5
@thomas-lamiaux
add the definition of the cohomology ring
1f12e1f
@thomas-lamiaux
some progress for the graded property
3bee7f0
@thomas-lamiaux
module name changes
a075003
@thomas-lamiaux
Add gradedComm proof :
0ee0210 
-> Modify some notions in gradedCommutativity
-> new lemme for the "good" -h^
-> proof
@thomas-lamiaux
uniformisation of the notation
015710b
@thomas-lamiaux
Computation of H*(Unit) cong Z
ecad958
@thomas-lamiaux
Proof in a more general setting :
d4adcc7 
-> Because this case is so degenerated, things compute.
   This new proof is forgetting some of the computation
   to have proof that will rise better to non-degenerated case
@thomas-lamiaux
Simplification
37342d4
@thomas-lamiaux
Renaming
22f07e7
@thomas-lamiaux
correct trailing-whitespaces and one path
4e45548
@thomas-lamiaux
Fix dependencies :
67d21cf 
-> changing gradedComm by gradedCom' to account
   the previuous change
@thomas-lamiaux
Fix dependecies
d38d370
@thomas-lamiaux
fix dependecies
53d1962
@thomas-lamiaux
fix dependencies
c3ea1cb
@thomas-lamiaux
Fix dependency brunerie
cb88096
@thomas-lamiaux
Add a recursor for the special case A / < a, ..., c >
b21dc11
@thomas-lamiaux
moved files
39ccad1
@thomas-lamiaux
Add a special recursor for polynomes :
7721b8b 
-> There is a need of the special as on the left we need the
   CommRing to take A / < a, ..., b > and we nedd a ring on
   the right as H*(X) is not a CommRing but a gradedComm Ring
@thomas-lamiaux
delete trailing-white-spaces
3b1e38c
@thomas-lamiaux
Begining to build a general framework ot the example of unit
b4b3685
@thomas-lamiaux
H*-Unit->Z[x] is a ring morphism
1167e9c
@thomas-lamiaux
Add functions H* Unit <-> Z[X]/X
4df89fa
@thomas-lamiaux
Builds all the framework except e-sect
6c385a4
@thomas-lamiaux
Fix : commented a part
5696cae
@thomas-lamiaux
Compute H* Unit in a generalisable way
c24276c
@thomas-lamiaux
A simplification
86af319
@thomas-lamiaux
Add the functions for S1 in both sens and stat proving some properties
a1861b2
@thomas-lamiaux
Add the following :
f3d2c17 
-> A cleaner way to deal with the cup product
-> Finish all the structure except some cases of the cup-product
-> Prove the retraction property
@thomas-lamiaux
Copy link
Contributor Author

@aljungstrom I miss H4 RP2 to do my proof

@thomas-lamiaux
Copy link
Contributor Author

@mortberg
Hi, just to tell you that the proof are basically done up to

  • @aljungstrom add a full characterization of H^n (RP²), there is only 1-3 for the moment
  • I add the following lemma .
    Nothing very hard just annoying, I'll come back on that when Axel is done with what is missing

About working with the Z/k, I think this prove it stills works up to a few tricks.
Though it would be a bit more complicated in the general case as Axel used Bool for Z/2.
But this would only change some details.
The good news too, is that the scheme of the proof doesn't change and the additional properties can be proven relatively simply by level as before. Plus, having more then one object in the ideal quotienting doesn't change anything when working.

@thomas-lamiaux thomas-lamiaux marked this pull request as ready for review July 22, 2022 22:51
@thomas-lamiaux
Copy link
Contributor Author

@mortberg Finally done with that !

@mortberg mortberg self-requested a review August 10, 2022 14:06
@mortberg mortberg merged commit 22225ed into agda:master Sep 12, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@MatthiasHu MatthiasHu MatthiasHu left review comments

@mortberg mortberg mortberg approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@thomas-lamiaux @mortberg @MatthiasHu