OAI/AlgebraicGeometry/Seshadri/Cohomology/AffineVanishing.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaximalSeshadri.FlasqueCohomology.sectionsTopEquiv line 17
2. def OAI.MaximalSeshadri.FlasqueCohomology.globalHomEquiv line 34
3. lemma OAI.MaximalSeshadri.FlasqueCohomology.globalHomEquiv_comp line 38
4. theorem OAI.MaximalSeshadri.FlasqueCohomology.globalHom_surjective line 42
5. instance OAI.MaximalSeshadri.FlasqueCohomology.moduleSheafHasExt line 61
6. theorem OAI.MaximalSeshadri.FlasqueCohomology.flasque_ext_zero line 64
7. def OAI.MaximalSeshadri.AffineCohomology.structureSheafUnit line 105
8. def OAI.MaximalSeshadri.AffineCohomology.schemeGlobalHomEquiv line 108
9. lemma OAI.MaximalSeshadri.AffineCohomology.globalHom_tilde_surjective line 112
10. theorem OAI.MaximalSeshadri.AffineCohomology.tilde_ext_zero line 132
11. theorem OAI.MaximalSeshadri.AffineCohomology.quasicoherent_ext_zero line 177
12. instance OAI.MaximalSeshadri.RestrictionExact.restriction_mono line 196
13. instance OAI.MaximalSeshadri.RestrictionExact.restriction_preservesMonomorphisms line 204
14. instance OAI.MaximalSeshadri.RestrictionExact.restriction_additive line 208
15. instance OAI.MaximalSeshadri.RestrictionExact.restriction_preservesHomology line 211
16. instance OAI.MaximalSeshadri.RestrictionExact.restriction_preservesFiniteLimits line 215
17. instance OAI.MaximalSeshadri.RestrictionExact.restriction_flasque line 219
18. def OAI.MaximalSeshadri.AffineSchemeCohomology.restrictionEquivalence line 237
19. theorem OAI.MaximalSeshadri.AffineSchemeCohomology.affine_ext_zero line 246