OAI/AlgebraicGeometry/Seshadri/Projective/AmpleEmbedding.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MaximalSeshadri.Geometry.LineBundle.ample_projective_sections line 19
  2. lemma OAI.MaximalSeshadri.Geometry.constantsInDegreeZero_bijective line 50
  3. def OAI.MaximalSeshadri.Geometry.constantsInDegreeZeroIso line 64
  4. instance OAI.MaximalSeshadri.Geometry.constantsInDegreeZero_isIso line 68
  5. instance OAI.MaximalSeshadri.Geometry.projectiveSpaceToSpec_proper line 72
  6. instance OAI.MaximalSeshadri.Geometry.Surface.proper line 87
  7. instance OAI.MaximalSeshadri.Geometry.Surface.compact line 91
  8. instance OAI.MaximalSeshadri.Geometry.Surface.locallyNoetherian line 94
  9. instance OAI.MaximalSeshadri.Geometry.Surface.noetherian line 97
  10. theorem OAI.MaximalSeshadri.Geometry.Surface.ample_embedding line 108
  11. lemma OAI.MaximalSeshadri.Projective.normalized_eval₂_of_evalAway line 128
  12. lemma OAI.MaximalSeshadri.Projective.affine_evaluation_surjective line 142
  13. theorem OAI.MaximalSeshadri.Projective.sectionsMorphism_chart_generators line 155
  14. lemma OAI.MaximalSeshadri.Projective.eval₂_surjective_reindex line 193
  15. theorem OAI.MaximalSeshadri.Projective.sectionsMorphism_reindex_closed line 204
  16. theorem OAI.MaximalSeshadri.Geometry.Surface.ample_embedding_fin line 231