OAI/AlgebraicGeometry/NumericalDimension/RelativeAmpleness.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Relative Ampleness.

  1. lemma OAI.NumericalDimensionOne.PolynomialCurveChart.fromSpec_germ line 17
  2. lemma OAI.NumericalDimensionOne.PolynomialCurveChart.projective_generic line 24
  3. lemma OAI.NumericalDimensionOne.PolynomialCurveChart.extension_agrees line 32
  4. lemma OAI.NumericalDimensionOne.exists_curveCoordinateMap line 55
  5. lemma OAI.NumericalDimensionOne.PolynomialCurveChart.basicOpen_le_inverse_chart line 99
  6. lemma OAI.NumericalDimensionOne.PolynomialCurveChart.inverse_chart_fromSpec line 120
  7. lemma OAI.NumericalDimensionOne.stalkMap_surjective_of_affine_immersion line 142
  8. lemma OAI.NumericalDimensionOne.isClosedImmersion_of_proper_two_charts line 151
  9. lemma OAI.NumericalDimensionOne.exists_nonconstant_curveFunction line 188
  10. lemma OAI.NumericalDimensionOne.curveCoordinateMap_preimage line 231
  11. lemma OAI.NumericalDimensionOne.exists_closedImmersion_of_smooth_proper_curve line 257
  12. def OAI.NumericalDimensionOne.properSmoothCurveVariety line 290
  13. def OAI.NumericalDimensionOne.surfacePrimeCurveOn line 298
  14. lemma OAI.NumericalDimensionOne.surfaceCartierPrimeDegree_eq_cartierCurveDegree line 311
  15. lemma OAI.NumericalDimensionOne.surfaceIntersection_nonneg_of_nef_effective line 317
  16. lemma OAI.NumericalDimensionOne.order_stalk_positive_iff line 339
  17. lemma OAI.NumericalDimensionOne.CartierStalkEquation.not_isUnit_of_mem_support line 353
  18. lemma OAI.NumericalDimensionOne.complexWeilDegree_positive_of_effective line 366
  19. lemma OAI.NumericalDimensionOne.cartierCurveDegree_positive_of_effective_meeting line 372
  20. lemma OAI.NumericalDimensionOne.primeDivisor_ne_generic line 408
  21. lemma OAI.NumericalDimensionOne.CurveOn.isClosed_prime_image line 415
  22. lemma OAI.NumericalDimensionOne.cartierCurveDegree_principal line 423
  23. lemma OAI.NumericalDimensionOne.cartierCurveDegree_positive_of_ample line 431
  24. lemma OAI.NumericalDimensionOne.qCartierCurveDegree_positive_of_ample line 467
  25. lemma OAI.NumericalDimensionOne.IsRelativelyAmpleQ.curveDegree_pos line 477
  26. lemma OAI.NumericalDimensionOne.canonical_difference_negative_on_curve line 496