OAI/AlgebraicGeometry/Seshadri/Projective/ClosedEmbedding.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MaximalSeshadri.Projective.polynomial_irrelevant_le line 20
  2. lemma OAI.MaximalSeshadri.Projective.projective_coordinate_cover line 32
  3. def OAI.MaximalSeshadri.Projective.projectiveCoordinateCover line 36
  4. lemma OAI.MaximalSeshadri.Projective.normalized_evalAway_surjective line 41
  5. lemma OAI.MaximalSeshadri.Projective.normalized_coordinates_closed line 79
  6. theorem OAI.MaximalSeshadri.Projective.sectionsMorphism_isClosedImmersion line 102
  7. theorem OAI.MaximalSeshadri.Geometry.closedImmersion_of_source_charts line 146
  8. def OAI.MaximalSeshadri.Projective.projectiveBase line 191
  9. lemma OAI.MaximalSeshadri.Projective.evalAway_constants line 194
  10. theorem OAI.MaximalSeshadri.Projective.coordinatesMap_over line 212
  11. theorem OAI.MaximalSeshadri.Projective.sectionsMorphism_over line 222
  12. theorem OAI.MaximalSeshadri.Projective.sectionsMorphism_closed_on_cover line 247
  13. instance OAI.MaximalSeshadri.Projective.projectiveBase_separated line 291
  14. instance OAI.MaximalSeshadri.Projective.sectionsMorphism_proper line 295
  15. lemma OAI.MaximalSeshadri.Projective.toSpec_scalarMap line 304
  16. lemma OAI.MaximalSeshadri.Geometry.finiteType_coordinates line 319
  17. theorem OAI.MaximalSeshadri.Geometry.affine_coordinate_generators line 336