OAI/NumberTheory/PiExponent/Geometry/ProjectiveCharts.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PiExponentSeshadri.Projective.homogeneous_eval₂_scale line 14
  2. abbrev OAI.PiExponentSeshadri.Projective.PolyGrade line 30
  3. lemma OAI.PiExponentSeshadri.Projective.poly_X_mem line 31
  4. abbrev OAI.PiExponentSeshadri.Projective.PolyChart line 33
  5. abbrev OAI.PiExponentSeshadri.Projective.ChartVariables line 34
  6. def OAI.PiExponentSeshadri.Projective.chartConstants line 36
  7. def OAI.PiExponentSeshadri.Projective.chartCoordinate line 44
  8. def OAI.PiExponentSeshadri.Projective.dehomogenize line 47
  9. lemma OAI.PiExponentSeshadri.Projective.dehomogenize_X_self line 50
  10. def OAI.PiExponentSeshadri.Projective.chartToPoly line 54
  11. def OAI.PiExponentSeshadri.Projective.polyToChart line 57
  12. lemma OAI.PiExponentSeshadri.Projective.chartToPoly_mk line 60
  13. lemma OAI.PiExponentSeshadri.Projective.chartToPoly_constants line 68
  14. lemma OAI.PiExponentSeshadri.Projective.chartToPoly_coordinate line 73
  15. lemma OAI.PiExponentSeshadri.Projective.chartToPoly_comp_polyToChart line 79
  16. lemma OAI.PiExponentSeshadri.Projective.chart_val_mk line 88
  17. lemma OAI.PiExponentSeshadri.Projective.chart_val_constants line 99
  18. lemma OAI.PiExponentSeshadri.Projective.chart_val_coordinate line 105
  19. lemma OAI.PiExponentSeshadri.Projective.chart_dehomogenize_val line 111
  20. lemma OAI.PiExponentSeshadri.Projective.polyToChart_comp_chartToPoly line 129
  21. def OAI.PiExponentSeshadri.Projective.polynomialChartEquiv line 149
  22. def OAI.PiExponentSeshadri.Projective.projectiveChartIso line 155
  23. def OAI.PiExponentSeshadri.Projective.chartSectionRingEquiv line 169
  24. lemma OAI.PiExponentSeshadri.Projective.standardChart_isAffineOpen line 176
  25. lemma OAI.PiExponentSeshadri.Projective.standardChart_cover line 180