OAI/AlgebraicGeometry/NumericalDimension/PolynomialCharts.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Polynomial Charts.

  1. abbrev OAI.NumericalDimensionOne.planeGrading line 20
  2. abbrev OAI.NumericalDimensionOne.planeChart line 21
  3. def OAI.NumericalDimensionOne.planeConstants line 23
  4. def OAI.NumericalDimensionOne.planeDehom line 30
  5. def OAI.NumericalDimensionOne.planeChartEval line 33
  6. def OAI.NumericalDimensionOne.planeChartCoordinate line 39
  7. def OAI.NumericalDimensionOne.planeChartInv line 44
  8. theorem OAI.NumericalDimensionOne.planeConstants_surjective line 49
  9. theorem OAI.NumericalDimensionOne.planeChartEval_mk line 55
  10. theorem OAI.NumericalDimensionOne.planeChartEval_constants line 65
  11. theorem OAI.NumericalDimensionOne.planeChartEval_coordinate line 74
  12. theorem OAI.NumericalDimensionOne.planeChartEval_inv line 79
  13. theorem OAI.NumericalDimensionOne.planeGrading_adjoin_X line 85
  14. theorem OAI.NumericalDimensionOne.planeChart_monomial line 97
  15. theorem OAI.NumericalDimensionOne.planeChartInv_bijective line 119
  16. theorem OAI.NumericalDimensionOne.proj_integral line 165
  17. theorem OAI.NumericalDimensionOne.planeXone_mem line 196
  18. def OAI.NumericalDimensionOne.complexAffineChart line 200
  19. theorem OAI.NumericalDimensionOne.planeChartEval_bijective line 205
  20. theorem OAI.NumericalDimensionOne.complexAffineChart_isOpenImmersion line 216
  21. theorem OAI.NumericalDimensionOne.planeAffineChart_toSpec line 223
  22. theorem OAI.NumericalDimensionOne.complexAffineChart_over line 235
  23. theorem OAI.NumericalDimensionOne.complexProjectiveLine_integral line 240
  24. theorem OAI.NumericalDimensionOne.complexProjectiveLine_nontrivial line 249
  25. def OAI.NumericalDimensionOne.curveFieldScalar line 274
  26. def OAI.NumericalDimensionOne.curveFunctionPolynomial line 278
  27. def OAI.NumericalDimensionOne.genericCurveFunctionMap line 282
  28. theorem OAI.NumericalDimensionOne.transcendental_of_not_constant line 287
  29. theorem OAI.NumericalDimensionOne.genericCurveFunctionMap_over line 297
  30. theorem OAI.NumericalDimensionOne.genericCurveFunctionMap_dominant line 309
  31. theorem OAI.NumericalDimensionOne.exists_finite_curveFunctionMap line 329
  32. theorem OAI.NumericalDimensionOne.mem_affine_chart_of_local_factor line 360
  33. def OAI.NumericalDimensionOne.curveStalkScalar line 403
  34. lemma OAI.NumericalDimensionOne.curveStalkScalar_comp_field line 406
  35. theorem OAI.NumericalDimensionOne.curveFunction_mem_chart_of_regular line 419
  36. theorem OAI.NumericalDimensionOne.exists_affine_finite_chart line 458
  37. structure OAI.NumericalDimensionOne.PolynomialCurveChart line 517
  38. lemma OAI.NumericalDimensionOne.exists_polynomialCurveChart line 529
  39. lemma OAI.NumericalDimensionOne.polynomialCurveChart_cover line 546
  40. lemma OAI.NumericalDimensionOne.PolynomialCurveChart.normal line 557
  41. lemma OAI.NumericalDimensionOne.exists_pow_mul_integer_of_integral_inverse line 578