OAI/NumberTheory/PiExponent/Cohomology/CechExtFinite.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PiExponent.GeometrySupport.CechExtFinite.schemeFreeOpen line 15
2. def OAI.PiExponent.GeometrySupport.CechExtFinite.ActualExt line 19
3. instance OAI.PiExponent.GeometrySupport.CechExtFinite.(instance at line 21) line 21
4. instance OAI.PiExponent.GeometrySupport.CechExtFinite.globalModule line 24
5. instance OAI.PiExponent.GeometrySupport.CechExtFinite.scalarModule line 28
6. def OAI.PiExponent.GeometrySupport.CechExtFinite.connecting line 31
7. lemma OAI.PiExponent.GeometrySupport.CechExtFinite.connecting_surjective line 40
8. def OAI.PiExponent.GeometrySupport.CechExtFinite.LocallyAcyclic line 46
9. lemma OAI.PiExponent.GeometrySupport.CechExtFinite.locallyAcyclic_quotient line 50
10. def OAI.PiExponent.GeometrySupport.CechExtFinite.descent line 61
11. lemma OAI.PiExponent.GeometrySupport.CechExtFinite.descent_lift line 76
12. def OAI.PiExponent.GeometrySupport.CechExtFinite.comparisonStep line 93
13. lemma OAI.PiExponent.GeometrySupport.CechExtFinite.comparisonStep_surjective line 99
14. lemma OAI.PiExponent.GeometrySupport.CechExtFinite.comparisonStep_boundary line 125
15. def OAI.PiExponent.GeometrySupport.CechExtFinite.mkZeroLinear line 146
16. theorem OAI.PiExponent.GeometrySupport.CechExtFinite.mkZeroLinear_apply line 160
17. def OAI.PiExponent.GeometrySupport.CechExtFinite.zeroComparison line 163
18. lemma OAI.PiExponent.GeometrySupport.CechExtFinite.zeroComparison_surjective line 171
19. lemma OAI.PiExponent.GeometrySupport.CechExtFinite.zeroComparison_middle line 181
20. theorem OAI.PiExponent.GeometrySupport.CechExtFinite.exists_comparison line 191
21. def OAI.PiExponent.GeometrySupport.CechExtFinite.sourceIso line 222
22. theorem OAI.PiExponent.GeometrySupport.CechExtFinite.affine_exists_comparison line 238