OAI/NumberTheory/PiExponent/Geometry/ProjectiveEmbeddingCharts.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PiExponentSeshadri.Projective.normalized_evalAway_surjective line 18
  2. lemma OAI.PiExponentSeshadri.Projective.normalized_coordinates_closed line 56
  3. theorem OAI.PiExponentSeshadri.Geometry.closedImmersion_of_source_charts line 76
  4. def OAI.PiExponentSeshadri.Projective.projectiveConstants line 121
  5. def OAI.PiExponentSeshadri.Projective.projectiveBase line 128
  6. lemma OAI.PiExponentSeshadri.Projective.evalAway_constants_comp line 131
  7. theorem OAI.PiExponentSeshadri.Projective.coordinatesMap_over line 149
  8. theorem OAI.PiExponentSeshadri.Projective.sectionsMorphism_over line 159
  9. instance OAI.PiExponentSeshadri.Projective.projectiveBase_separated line 181
  10. instance OAI.PiExponentSeshadri.Projective.sectionsMorphism_proper line 185
  11. lemma OAI.PiExponentSeshadri.Projective.toSpec_scalarMap line 194
  12. lemma OAI.PiExponentSeshadri.Geometry.finiteType_coordinates line 207
  13. theorem OAI.PiExponentSeshadri.Geometry.affine_coordinate_generators line 224