OAI/AlgebraicGeometry/NumericalDimension/NormalDivisors.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Normal Divisors.

  1. def OAI.NumericalDimensionOne.denominatorIdeal line 14
  2. lemma OAI.NumericalDimensionOne.mem_denominatorIdeal line 18
  3. lemma OAI.NumericalDimensionOne.denominatorIdeal_ne_bot line 22
  4. lemma OAI.NumericalDimensionOne.denominatorIdeal_eq_top_iff line 33
  5. theorem OAI.NumericalDimensionOne.prime_denominator_height line 40
  6. lemma OAI.NumericalDimensionOne.quotient_annihilator_eq line 88
  7. theorem OAI.NumericalDimensionOne.normal_domain_height_one_criterion line 96
  8. class OAI.NumericalDimensionOne.StalkwiseNormal line 133
  9. abbrev OAI.NumericalDimensionOne.PrimeDivisor line 138
  10. abbrev OAI.NumericalDimensionOne.WeilDivisor line 139
  11. instance OAI.NumericalDimensionOne.nonempty_top_open line 141
  12. theorem OAI.NumericalDimensionOne.dvr_at_prime_divisor line 146
  13. def OAI.NumericalDimensionOne.IsDivisorSection line 161
  14. theorem OAI.NumericalDimensionOne.divisorSection_add line 164
  15. theorem OAI.NumericalDimensionOne.divisorSection_smul line 182
  16. def OAI.NumericalDimensionOne.divisorSections line 195
  17. theorem OAI.NumericalDimensionOne.finite_primeDivisors_in_closed line 206
  18. theorem OAI.NumericalDimensionOne.ord_finite_support line 247
  19. def OAI.NumericalDimensionOne.principalWeilDivisor line 263
  20. theorem OAI.NumericalDimensionOne.principalWeilDivisor_apply line 267
  21. theorem OAI.NumericalDimensionOne.ord_nonnegative_iff_regular line 272
  22. theorem OAI.NumericalDimensionOne.integrallyClosed_affine line 298
  23. theorem OAI.NumericalDimensionOne.affine_regular_iff_nonnegative_orders line 309
  24. lemma OAI.NumericalDimensionOne.germToFunctionField_restrict line 361
  25. theorem OAI.NumericalDimensionOne.global_regular_iff_nonnegative_orders line 367
  26. lemma OAI.NumericalDimensionOne.order_one line 408
  27. lemma OAI.NumericalDimensionOne.order_inv line 414
  28. def OAI.NumericalDimensionOne.IsCartierDivisor line 420
  29. lemma OAI.NumericalDimensionOne.isCartierDivisor_zero line 426
  30. lemma OAI.NumericalDimensionOne.isCartierDivisor_neg line 434
  31. lemma OAI.NumericalDimensionOne.isCartierDivisor_add line 443
  32. def OAI.NumericalDimensionOne.cartierDivisors line 455
  33. def OAI.NumericalDimensionOne.IsDivisorSectionOn line 461
  34. theorem OAI.NumericalDimensionOne.cartier_local_section_iff line 464
  35. theorem OAI.NumericalDimensionOne.divisorSection_mul line 480
  36. theorem OAI.NumericalDimensionOne.divisorSections_mono line 498
  37. lemma OAI.NumericalDimensionOne.dominant_genericPoint line 517
  38. def OAI.NumericalDimensionOne.dominantFunctionFieldMap line 523
  39. lemma OAI.NumericalDimensionOne.dominantFunctionFieldMap_algebraMap line 529
  40. def OAI.NumericalDimensionOne.IsCartierPullback line 548