OAI/AlgebraicGeometry/NumericalDimension/CartierIntersection.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Cartier Intersection.

  1. lemma OAI.NumericalDimensionOne.proper_principal_degree_zero line 21
  2. lemma OAI.NumericalDimensionOne.proper_representative_degree_eq line 26
  3. def OAI.NumericalDimensionOne.properCurveDegree line 37
  4. lemma OAI.NumericalDimensionOne.properCurveDegree_eq line 43
  5. lemma OAI.NumericalDimensionOne.properCurveDegree_add line 49
  6. lemma OAI.NumericalDimensionOne.properCurveDegree_zero line 59
  7. def OAI.NumericalDimensionOne.properCurveDegreeHom line 62
  8. lemma OAI.NumericalDimensionOne.properCurveDegree_eq_cartierCurveDegree line 67
  9. theorem OAI.NumericalDimensionOne.ringKrullDim_le_of_quasiFinite line 80
  10. theorem OAI.NumericalDimensionOne.coheight_le_of_smooth_dimension line 107
  11. lemma OAI.NumericalDimensionOne.finite_closed_of_closed_points line 140
  12. lemma OAI.NumericalDimensionOne.eq_of_specializes_of_equal_finite_coheight line 155
  13. lemma OAI.NumericalDimensionOne.isClosed_point_of_max_coheight line 165
  14. lemma OAI.NumericalDimensionOne.closed_point_of_distinct_prime_intersection line 179
  15. theorem OAI.NumericalDimensionOne.finite_divisorSupport_intersection line 197
  16. theorem OAI.NumericalDimensionOne.finite_divisorSupport_intersection_smooth line 211
  17. def OAI.NumericalDimensionOne.IsGeneratedAt line 228
  18. lemma OAI.NumericalDimensionOne.coefficient_zero_on_divisorComplement line 233
  19. lemma OAI.NumericalDimensionOne.section_regular_stalk line 244
  20. lemma OAI.NumericalDimensionOne.section_unit_stalk line 255
  21. lemma OAI.NumericalDimensionOne.IsPulledCartierRepresentative.exists_nonzero_section line 274
  22. theorem OAI.NumericalDimensionOne.cartierCurveDegree_nonneg_of_generatedAt line 305
  23. lemma OAI.NumericalDimensionOne.section_nonvanishing_of_local_unit line 328
  24. lemma OAI.NumericalDimensionOne.stalkPrime_eq_comap_closedPoint line 357
  25. lemma OAI.NumericalDimensionOne.fromSpecStalk_mem_support_of_mem_prime line 373
  26. theorem OAI.NumericalDimensionOne.localIntersection_isFiniteLength line 396
  27. structure OAI.NumericalDimensionOne.CartierStalkEquation line 465
  28. lemma OAI.NumericalDimensionOne.exists_cartierStalkEquation line 474
  29. lemma OAI.NumericalDimensionOne.cartierStalkEquation_ideal_eq line 482
  30. def OAI.NumericalDimensionOne.effectiveCartierStalkIdeal line 492
  31. lemma OAI.NumericalDimensionOne.effectiveCartierStalkIdeal_eq line 497
  32. def OAI.NumericalDimensionOne.effectiveCartierMultiplicity line 503
  33. lemma OAI.NumericalDimensionOne.effectiveCartierMultiplicity_comm line 510
  34. lemma OAI.NumericalDimensionOne.effectiveCartierStalkIdeal_eq_top line 521
  35. lemma OAI.NumericalDimensionOne.effectiveCartierMultiplicity_eq_zero line 536
  36. lemma OAI.NumericalDimensionOne.effectiveCartierMultiplicity_ne_top line 549
  37. lemma OAI.NumericalDimensionOne.effectiveCartierMultiplicity_finite_support line 564