OAI/AlgebraicGeometry/Seshadri/Projective/PolynomialCharts.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MaximalSeshadri.Projective.homogeneous_eval₂_scale line 14
  2. abbrev OAI.MaximalSeshadri.Projective.PolyGrade line 30
  3. lemma OAI.MaximalSeshadri.Projective.poly_X_mem line 31
  4. abbrev OAI.MaximalSeshadri.Projective.PolyChart line 33
  5. abbrev OAI.MaximalSeshadri.Projective.ChartVariables line 34
  6. def OAI.MaximalSeshadri.Projective.chartConstants line 36
  7. def OAI.MaximalSeshadri.Projective.chartCoordinate line 44
  8. def OAI.MaximalSeshadri.Projective.dehomogenize line 47
  9. lemma OAI.MaximalSeshadri.Projective.dehomogenize_X_self line 50
  10. def OAI.MaximalSeshadri.Projective.chartToPoly line 54
  11. def OAI.MaximalSeshadri.Projective.polyToChart line 57
  12. lemma OAI.MaximalSeshadri.Projective.chartToPoly_mk line 60
  13. lemma OAI.MaximalSeshadri.Projective.chartToPoly_constants line 68
  14. lemma OAI.MaximalSeshadri.Projective.chartToPoly_coordinate line 73
  15. lemma OAI.MaximalSeshadri.Projective.chartToPoly_comp_polyToChart line 79
  16. lemma OAI.MaximalSeshadri.Projective.chart_val_mk line 88
  17. lemma OAI.MaximalSeshadri.Projective.chart_val_constants line 99
  18. lemma OAI.MaximalSeshadri.Projective.chart_val_coordinate line 105
  19. lemma OAI.MaximalSeshadri.Projective.chart_dehomogenize_val line 111
  20. lemma OAI.MaximalSeshadri.Projective.polyToChart_comp_chartToPoly line 129
  21. def OAI.MaximalSeshadri.Projective.polynomialChartEquiv line 149
  22. def OAI.MaximalSeshadri.Projective.projectiveChartIso line 155
  23. def OAI.MaximalSeshadri.Projective.linearEquation line 169
  24. lemma OAI.MaximalSeshadri.Projective.linearEquation_homogeneous line 171
  25. lemma OAI.MaximalSeshadri.Projective.linearEquation_chart line 175
  26. lemma OAI.MaximalSeshadri.Projective.hyperplane_chart_preimage line 190
  27. lemma OAI.MaximalSeshadri.Projective.chartCoordinate_self line 198
  28. lemma OAI.MaximalSeshadri.Projective.hyperplane_affine_preimage line 203
  29. lemma OAI.MaximalSeshadri.Projective.hyperplane_affine_preimage_reindexed line 217
  30. theorem OAI.MaximalSeshadri.Projective.projective_affine_factor line 240
  31. def OAI.MaximalSeshadri.Projective.projectiveConstants line 275
  32. def OAI.MaximalSeshadri.Projective.projectiveToSpec line 283
  33. lemma OAI.MaximalSeshadri.Projective.chart_toSpec line 288
  34. lemma OAI.MaximalSeshadri.Projective.projective_affine_constants line 296
  35. def OAI.MaximalSeshadri.BertiniIntegral.projectiveHyperplane line 320
  36. theorem OAI.MaximalSeshadri.BertiniIntegral.smooth_integral_hyperplane_of_etale_atlas line 326