OAI/AlgebraicGeometry/NumericalDimension/CurveOrders.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Curve Orders.

  1. theorem OAI.NumericalDimensionOneCurveAux.isClosed_point_of_curve_coheight line 17
  2. theorem OAI.NumericalDimensionOneCurveAux.finite_closed_of_curve_coheight line 42
  3. theorem OAI.NumericalDimensionOneCurveAux.finite_of_proper_dominant_from_smooth_curve line 60
  4. def OAI.NumericalDimensionOneCurveAux.curveFieldScalar line 108
  5. def OAI.NumericalDimensionOneCurveAux.curveFunctionPolynomial line 112
  6. def OAI.NumericalDimensionOneCurveAux.genericCurveFunctionMap line 116
  7. theorem OAI.NumericalDimensionOneCurveAux.transcendental_of_not_constant line 121
  8. theorem OAI.NumericalDimensionOneCurveAux.genericCurveFunctionMap_over line 131
  9. theorem OAI.NumericalDimensionOneCurveAux.genericCurveFunctionMap_dominant line 143
  10. theorem OAI.NumericalDimensionOneCurveAux.exists_finite_curveFunctionMap line 163
  11. theorem OAI.NumericalDimensionOneCurveAux.exists_affine_finite_chart line 193
  12. theorem OAI.NumericalDimensionOneCurveAux.exists_finite_polynomial_presentation line 253
  13. theorem OAI.NumericalDimensionOneCurveAux.mem_affine_chart_of_local_factor line 292
  14. def OAI.NumericalDimensionOneCurveAux.curveStalkScalar line 334
  15. lemma OAI.NumericalDimensionOneCurveAux.curveStalkScalar_comp_field line 337
  16. theorem OAI.NumericalDimensionOneCurveAux.curveFunction_mem_chart_of_regular line 350
  17. lemma OAI.NumericalDimensionOneCurveAux.order_one line 389
  18. lemma OAI.NumericalDimensionOneCurveAux.order_neg line 394
  19. lemma OAI.NumericalDimensionOneCurveAux.order_inv line 404
  20. lemma OAI.NumericalDimensionOneCurveAux.order_div line 410
  21. lemma OAI.NumericalDimensionOneCurveAux.order_nonnegative_iff_local line 415
  22. lemma OAI.NumericalDimensionOneCurveAux.order_add_one_of_negative line 438
  23. theorem OAI.NumericalDimensionOneCurveAux.inertiaDegree_one_of_algClosed_residue line 462
  24. theorem OAI.NumericalDimensionOneCurveAux.sum_local_order_eq_finrank line 470
  25. def OAI.NumericalDimensionOneCurveAux.polynomialPoint line 491
  26. instance OAI.NumericalDimensionOneCurveAux.polynomialPoint_isMaximal line 494
  27. def OAI.NumericalDimensionOneCurveAux.polynomialPoint_residueFieldEquiv line 498
  28. instance OAI.NumericalDimensionOneCurveAux.polynomialPoint_residueField_algClosed line 505
  29. theorem OAI.NumericalDimensionOneCurveAux.polynomial_fiber_order_eq_rank line 509
  30. theorem OAI.NumericalDimensionOneCurveAux.ringOrder_equiv line 532
  31. theorem OAI.NumericalDimensionOneCurveAux.scheme_order_of_stalk_element line 538
  32. theorem OAI.NumericalDimensionOneCurveAux.scheme_order_on_affine_chart line 552