OAI/NumberTheory/PiExponent/Cohomology/ReesSheafCechRecovery.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PiExponent.ReesSheafCechRecovery.schemeFreeOpen line 26
2. def OAI.PiExponent.ReesSheafCechRecovery.gradedCycles line 36
3. instance OAI.PiExponent.ReesSheafCechRecovery.gradedCyclesGroup line 46
4. def OAI.PiExponent.ReesSheafCechRecovery.groupAddZero line 49
5. def OAI.PiExponent.ReesSheafCechRecovery.groupAddZeroClass line 53
6. instance OAI.PiExponent.ReesSheafCechRecovery.(instance at line 57) line 57
7. instance OAI.PiExponent.ReesSheafCechRecovery.(instance at line 60) line 60
8. def OAI.PiExponent.ReesSheafCechRecovery.cyclesEquiv line 64
9. def OAI.PiExponent.ReesSheafCechRecovery.ordinaryAugmentation line 77
10. def OAI.PiExponent.ReesSheafCechRecovery.globalCyclesEquiv line 85
11. def OAI.PiExponent.ReesSheafCechRecovery.ordinarySectionHom line 94
12. def OAI.PiExponent.ReesSheafCechRecovery.ordinaryGlobalSection line 98
13. theorem OAI.PiExponent.ReesSheafCechRecovery.ordinarySectionHom_restriction line 103
14. theorem OAI.PiExponent.ReesSheafCechRecovery.ordinarySectionHom_chartValue line 118
15. theorem OAI.PiExponent.ReesSheafCechRecovery.ordinarySectionHom_frozenChartValue line 130
16. theorem OAI.PiExponent.ReesSheafCechRecovery.eventually_recovery_and_primitives line 145
17. theorem OAI.PiExponent.ReesSheafCechRecovery.eventually_recovery line 181
18. theorem OAI.PiExponent.ReesSheafCechRecovery.eventually_recovery_and_cohomology line 188