OAI/AlgebraicGeometry/NumericalDimension/CurveDegrees.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Curve Degrees.

  1. abbrev OAI.NumericalDimensionOneCurveAux.PrimeDivisor line 16
  2. abbrev OAI.NumericalDimensionOneCurveAux.WeilDivisor line 17
  3. def OAI.NumericalDimensionOneCurveAux.complexWeilDegree line 19
  4. lemma OAI.NumericalDimensionOneCurveAux.coheight_eq_one_on_curve line 21
  5. lemma OAI.NumericalDimensionOneCurveAux.affine_point_of_nonzero_prime line 33
  6. def OAI.NumericalDimensionOneCurveAux.polynomialFiberPoint line 51
  7. lemma OAI.NumericalDimensionOneCurveAux.polynomialFiberPoint_injective line 61
  8. def OAI.NumericalDimensionOneCurveAux.polynomialFiberDivisor line 70
  9. lemma OAI.NumericalDimensionOneCurveAux.polynomialFiberDivisor_degree line 79
  10. lemma OAI.NumericalDimensionOneCurveAux.polynomial_liesOver_iff line 99
  11. lemma OAI.NumericalDimensionOneCurveAux.polynomialFiberDivisor_apply_outside line 120
  12. lemma OAI.NumericalDimensionOneCurveAux.polynomialFiberDivisor_apply_inside line 134
  13. theorem OAI.NumericalDimensionOneCurveAux.finite_primeDivisors_in_closed line 188
  14. theorem OAI.NumericalDimensionOneCurveAux.ord_finite_support line 227
  15. def OAI.NumericalDimensionOneCurveAux.principalWeilDivisor line 243
  16. theorem OAI.NumericalDimensionOneCurveAux.principalWeilDivisor_apply line 246
  17. lemma OAI.NumericalDimensionOneCurveAux.dvr_stalk_of_smooth_curve line 260
  18. lemma OAI.NumericalDimensionOneCurveAux.curve_scalar_order_zero line 279
  19. lemma OAI.NumericalDimensionOneCurveAux.affine_polynomial_germ line 291
  20. theorem OAI.NumericalDimensionOneCurveAux.proper_curve_principal_degree_zero line 307
  21. lemma OAI.NumericalDimensionOne.pulledCartierRepresentative_difference line 394
  22. lemma OAI.NumericalDimensionOne.principal_degree_zero line 420
  23. lemma OAI.NumericalDimensionOne.pulledCartierRepresentative_degree_eq line 426
  24. lemma OAI.NumericalDimensionOne.divisor_degree_nonnegative line 439
  25. lemma OAI.NumericalDimensionOne.IsPulledCartierRepresentative.add line 461
  26. lemma OAI.NumericalDimensionOne.isPulledCartierRepresentative_zero line 492
  27. lemma OAI.NumericalDimensionOne.cartierCurveDegree_add line 510
  28. lemma OAI.NumericalDimensionOne.cartierCurveDegree_zero line 520
  29. def OAI.NumericalDimensionOne.cartierCurveDegreeHom line 528