OAI/NumberTheory/PiExponent/Cohomology/PencilCohomology.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponentSeshadri.Geometry.BaseSections.two_chart_intersection_finite line 15
  2. def OAI.PiExponentSeshadri.Geometry.BaseSections.twoBaseIntersection line 53
  3. theorem OAI.PiExponentSeshadri.Geometry.BaseSections.finite_pencil_intersection line 58
  4. lemma OAI.PiExponentSeshadri.Geometry.BaseSections.res_comp line 109
  5. def OAI.PiExponentSeshadri.Geometry.BaseSections.globalIntersection line 116
  6. lemma OAI.PiExponentSeshadri.Geometry.BaseSections.globalIntersection_injective line 126
  7. def OAI.PiExponentSeshadri.Geometry.BaseSections.globalSectionsLinear line 133
  8. def OAI.PiExponentSeshadri.Geometry.BaseSections.cohomologyZero line 145
  9. theorem OAI.PiExponentSeshadri.Geometry.finite_pencil_H0_finite line 165
  10. theorem OAI.PiExponentSeshadri.Geometry.BaseSections.finite_pencil_cokernel line 210
  11. theorem OAI.PiExponentSeshadri.Geometry.finite_pencil_H1_finite line 260