OAI/AlgebraicGeometry/NumericalDimension/ProjectiveCurves.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Projective Curves.

  1. abbrev OAI.NumericalDimensionOneCurveAux.planeGrading line 18
  2. abbrev OAI.NumericalDimensionOneCurveAux.planeChart line 19
  3. def OAI.NumericalDimensionOneCurveAux.planeConstants line 21
  4. def OAI.NumericalDimensionOneCurveAux.planeDehom line 28
  5. def OAI.NumericalDimensionOneCurveAux.planeChartEval line 31
  6. def OAI.NumericalDimensionOneCurveAux.planeChartCoordinate line 37
  7. def OAI.NumericalDimensionOneCurveAux.planeChartInv line 42
  8. theorem OAI.NumericalDimensionOneCurveAux.planeConstants_surjective line 47
  9. theorem OAI.NumericalDimensionOneCurveAux.planeChartEval_mk line 53
  10. theorem OAI.NumericalDimensionOneCurveAux.planeChartEval_constants line 63
  11. theorem OAI.NumericalDimensionOneCurveAux.planeChartEval_coordinate line 72
  12. theorem OAI.NumericalDimensionOneCurveAux.planeChartEval_inv line 77
  13. theorem OAI.NumericalDimensionOneCurveAux.planeGrading_adjoin_X line 83
  14. theorem OAI.NumericalDimensionOneCurveAux.planeChart_monomial line 95
  15. theorem OAI.NumericalDimensionOneCurveAux.planeChartInv_bijective line 117
  16. theorem OAI.NumericalDimensionOneCurveAux.proj_integral line 162
  17. theorem OAI.NumericalDimensionOneCurveAux.planeXone_mem line 192
  18. def OAI.NumericalDimensionOneCurveAux.complexAffineChart line 196
  19. theorem OAI.NumericalDimensionOneCurveAux.planeChartEval_bijective line 201
  20. theorem OAI.NumericalDimensionOneCurveAux.complexAffineChart_isOpenImmersion line 212
  21. theorem OAI.NumericalDimensionOneCurveAux.planeAffineChart_toSpec line 219
  22. theorem OAI.NumericalDimensionOneCurveAux.complexAffineChart_over line 231
  23. theorem OAI.NumericalDimensionOneCurveAux.complexProjectiveLine_integral line 236
  24. theorem OAI.NumericalDimensionOneCurveAux.complexProjectiveLine_nontrivial line 245
  25. theorem OAI.NumericalDimensionOneCurveAux.ringKrullDim_le_of_quasiFinite line 268
  26. def OAI.NumericalDimensionOneCurveAux.schemeOpenScalar line 296
  27. def OAI.NumericalDimensionOneCurveAux.schemeOpenAlgebra line 301
  28. theorem OAI.NumericalDimensionOneCurveAux.exists_standard_smooth_chart line 304
  29. theorem OAI.NumericalDimensionOneCurveAux.coheight_le_of_smooth_dimension line 334
  30. theorem OAI.NumericalDimensionOneCurveAux.isIntegrallyClosed_of_etale_domain line 365
  31. theorem OAI.NumericalDimensionOneCurveAux.isIntegrallyClosed_of_smooth_field_domain line 413
  32. theorem OAI.NumericalDimensionOneCurveAux.integrallyClosed_stalk_of_smooth_field line 447
  33. theorem OAI.NumericalDimensionOneCurveAux.valuationRing_stalk_of_smooth_curve line 479
  34. lemma OAI.NumericalDimensionOneCurveAux.partial_fromFunctionField_eq line 512
  35. theorem OAI.NumericalDimensionOneCurveAux.exists_extension_from_functionField_of_smooth_curve line 541