OAI/AlgebraicGeometry/Seshadri/Cohomology/RestrictionComparison.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaximalSeshadri.ExtSectionComparison.mapFrom line 18
2. lemma OAI.MaximalSeshadri.ExtSectionComparison.mapFrom_apply line 21
3. lemma OAI.MaximalSeshadri.ExtSectionComparison.mapFrom_mk₀ line 24
4. lemma OAI.MaximalSeshadri.ExtSectionComparison.mapFrom_comp line 28
5. theorem OAI.MaximalSeshadri.ExtSectionComparison.mapFrom_bijective line 35
6. lemma OAI.MaximalSeshadri.RestrictionCohomology.freeOpenEquiv_comp line 90
7. def OAI.MaximalSeshadri.RestrictionCohomology.restrictionSectionsIso line 95
8. def OAI.MaximalSeshadri.RestrictionCohomology.restrictionHomEquiv line 98
9. lemma OAI.MaximalSeshadri.RestrictionCohomology.restrictionHomEquiv_comp line 105
10. def OAI.MaximalSeshadri.RestrictionCohomology.restrictionGenerator line 126
11. lemma OAI.MaximalSeshadri.RestrictionCohomology.restrictionGenerator_comp line 130
12. theorem OAI.MaximalSeshadri.RestrictionCohomology.restriction_ext_bijective line 137
13. def OAI.MaximalSeshadri.ModuleMayerVietoris.freeOpenFunctor line 167
14. lemma OAI.MaximalSeshadri.ModuleMayerVietoris.freeOpen_isPushout line 170
15. def OAI.MaximalSeshadri.ModuleMayerVietoris.shortComplex line 185
16. instance OAI.MaximalSeshadri.ModuleMayerVietoris.shortComplex_mono line 196
17. lemma OAI.MaximalSeshadri.ModuleMayerVietoris.shortComplex_shortExact line 203
18. lemma OAI.MaximalSeshadri.ModuleMayerVietoris.union_ext_zero line 212