OAI/AlgebraicGeometry/Seshadri/Cohomology/CurveH0Finite.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MaximalSeshadri.Geometry.BaseSections.res_comp line 20
2. def OAI.MaximalSeshadri.Geometry.BaseSections.globalIntersection line 26
3. lemma OAI.MaximalSeshadri.Geometry.BaseSections.globalIntersection_injective line 36
4. def OAI.MaximalSeshadri.Geometry.BaseSections.globalSectionsLinear line 43
5. def OAI.MaximalSeshadri.Geometry.BaseSections.cohomologyZero line 55
6. theorem OAI.MaximalSeshadri.Geometry.finite_pencil_H0_finite line 75
7. theorem OAI.MaximalSeshadri.Geometry.projective_curve_H0_finite line 113