OAI/AlgebraicGeometry/Seshadri/Cohomology/FiniteSupportCohomology.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MaximalSeshadri.FiniteSupport.discrete_restriction_surjective line 15
2. lemma OAI.MaximalSeshadri.FiniteSupport.discrete_flasque line 56
3. lemma OAI.MaximalSeshadri.FiniteSupport.proper_finite_discrete line 63
4. lemma OAI.MaximalSeshadri.FiniteSupport.pushforward_flasque line 74
5. theorem OAI.MaximalSeshadri.FiniteSupport.finite_pushforward_ext_zero line 83
6. def OAI.MaximalSeshadri.FiniteSupport.pushforwardUnitSections line 90
7. theorem OAI.MaximalSeshadri.FiniteSupport.finite_pushforward_euler line 105