OAI/NumberTheory/PiExponent/Cohomology/PencilCohomologyFiniteCharts.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponentSeshadri.Projective.pencil_polynomial_irrelevant_le line 14
  2. def OAI.PiExponentSeshadri.Projective.projectiveCoordinateCover line 26
  3. lemma OAI.PiExponentSeshadri.Projective.affine_evaluation_finite line 33
  4. lemma OAI.PiExponentSeshadri.Projective.normalized_evalAway_polyToChart line 46
  5. theorem OAI.PiExponentSeshadri.Projective.finite_sectionsMorphism_chart line 66
  6. instance OAI.PiExponentSeshadri.Projective.boolChartUnique line 100
  7. theorem OAI.PiExponentSeshadri.Projective.finite_pencil_chart line 104
  8. lemma OAI.PiExponentSeshadri.Projective.pencil_overlap_basic line 140
  9. lemma OAI.PiExponentSeshadri.Projective.pencil_overlap_reciprocal line 147