OAI/AlgebraicGeometry/NumericalDimension/SurfaceIntersection.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Surface Intersection.

  1. lemma OAI.NumericalDimensionOne.length_sup_span_eq_ord_quotient line 16
  2. lemma OAI.NumericalDimensionOne.primeDivisor_effective line 34
  3. lemma OAI.NumericalDimensionOne.primeCartierStalkIdeal line 41
  4. theorem OAI.NumericalDimensionOne.primeCurveMultiplicity_eq_ord line 67
  5. lemma OAI.NumericalDimensionOne.primeCurve_equation_ne_zero line 94
  6. theorem OAI.NumericalDimensionOne.primeCurveMultiplicity_eq_normalizedBranches line 119
  7. def OAI.NumericalDimensionOne.surfaceCartierPrimeDegree line 156
  8. lemma OAI.NumericalDimensionOne.surfaceCartierPrimeDegree_add line 171
  9. lemma OAI.NumericalDimensionOne.surfaceCartierPrimeDegree_zero line 186
  10. def OAI.NumericalDimensionOne.surfaceIntersection line 201
  11. lemma OAI.NumericalDimensionOne.surfaceIntersection_add_left line 204
  12. lemma OAI.NumericalDimensionOne.surfaceIntersection_add_right line 209
  13. lemma OAI.NumericalDimensionOne.surfaceIntersection_zero_left line 215
  14. lemma OAI.NumericalDimensionOne.surfaceIntersection_zero_right line 218
  15. def OAI.NumericalDimensionOne.surfaceIntersectionHom line 222
  16. lemma OAI.NumericalDimensionOne.pointClosure_generic line 239
  17. lemma OAI.NumericalDimensionOne.prime_point_outside_support line 244
  18. lemma OAI.NumericalDimensionOne.finite_support_pulled_orders line 256
  19. lemma OAI.NumericalDimensionOne.fiber_composite_stalk_element line 283
  20. theorem OAI.NumericalDimensionOne.surfacePrimeDegree_eq_multiplicities line 304
  21. lemma OAI.NumericalDimensionOne.finsum_comp_injective_supported line 367
  22. lemma OAI.NumericalDimensionOne.prime_multiplicity_support line 392
  23. lemma OAI.NumericalDimensionOne.prime_multiplicities_finsum line 425
  24. def OAI.NumericalDimensionOne.smoothSurfaceWeilCartier line 454
  25. def OAI.NumericalDimensionOne.smoothSurfacePrimeCartier line 461
  26. theorem OAI.NumericalDimensionOne.surfacePrimePrime_comm line 464
  27. lemma OAI.NumericalDimensionOne.finsupp_bilinear_comm line 499
  28. lemma OAI.NumericalDimensionOne.surfaceIntersection_prime_left line 533
  29. theorem OAI.NumericalDimensionOne.surfaceIntersection_comm line 541
  30. lemma OAI.NumericalDimensionOne.isPulledCartierRepresentative_principal line 569
  31. lemma OAI.NumericalDimensionOne.properCurveDegree_principal line 582