OAI/AlgebraicGeometry/NumericalDimension/CurveProjection.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Curve Projection.

  1. theorem OAI.NumericalDimensionOne.properCurveDegree_comp_finite line 25
  2. theorem OAI.NumericalDimensionOne.curveFieldDegree_pos line 49
  3. lemma OAI.NumericalDimensionOne.dominantFunctionFieldMap_spec line 73
  4. theorem OAI.NumericalDimensionOne.valuationRing_stalk_of_smooth_curve line 99
  5. lemma OAI.NumericalDimensionOne.partial_fromFunctionField_eq line 133
  6. theorem OAI.NumericalDimensionOne.exists_extension_from_functionField_of_smooth_curve line 163
  7. theorem OAI.NumericalDimensionOne.curve_lift_through_proper_functionField_iso line 242
  8. lemma OAI.NumericalDimensionOne.reduced_ker_radical line 301
  9. theorem OAI.NumericalDimensionOne.exists_lift_closed_of_reduced line 311
  10. theorem OAI.NumericalDimensionOne.factor_dominant_pointClosure line 333
  11. theorem OAI.NumericalDimensionOne.curve_factors_through_normalized_image line 362
  12. theorem OAI.NumericalDimensionOne.surface_curve_degree_projection line 402
  13. theorem OAI.NumericalDimensionOne.pointClosure_map_functionField_bijective line 443
  14. lemma OAI.NumericalDimensionOne.curveFieldDegree_eq_one line 494
  15. lemma OAI.NumericalDimensionOne.dominantFunctionFieldMap_bijective_comp line 499
  16. lemma OAI.NumericalDimensionOne.dominantFunctionFieldMap_bijective_of_comp line 510
  17. lemma OAI.NumericalDimensionOne.IsCartierPullback.order_eq_of_equation line 529
  18. theorem OAI.NumericalDimensionOne.IsPulledCartierRepresentative.of_cartierPullback line 555
  19. theorem OAI.NumericalDimensionOne.properCurveDegree_ambientPullback line 597