OAI/AlgebraicGeometry/Seshadri/Cohomology/ClosedPushforwardCohomology.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaximalSeshadri.ClosedPushforward.cohomologyMap line 22
2. lemma OAI.MaximalSeshadri.ClosedPushforward.globalHom_push line 28
3. lemma OAI.MaximalSeshadri.ClosedPushforward.cohomologyMap_zero_bijective line 36
4. lemma OAI.MaximalSeshadri.ClosedPushforward.pushforward_flasque line 63
5. lemma OAI.MaximalSeshadri.ClosedPushforward.cohomologyMap_comp line 70
6. theorem OAI.MaximalSeshadri.ClosedPushforward.cohomologyMap_bijective line 80