OAI/AlgebraicGeometry/SectionFields/NormalDivisors.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Normal local rings, height-one orders, divisors and descent of rational functions.

  1. theorem OAI.RelativeDenominators.maximalIdeal_isPrincipal_of_fraction_witness line 17
  2. theorem OAI.RelativeDenominators.exists_prime_colon_over line 66
  3. theorem OAI.RelativeDenominators.mem_localization_iff_denominator line 97
  4. theorem OAI.RelativeDenominators.height_eq_one_of_prime_denominator_ideal line 121
  5. theorem OAI.RelativeDenominators.exists_algebraMap_eq_of_mem_height_one_localizations line 180
  6. theorem OAI.RelativeDenominators.integrallyClosed_affine_sections line 203
  7. theorem OAI.RelativeDenominators.dvr_stalk_of_normal_codimOne line 221
  8. abbrev OAI.RelativeDenominators.PrimeDivisor line 244
  9. abbrev OAI.RelativeDenominators.WeilDivisor line 247
  10. theorem OAI.RelativeDenominators.finite_codimOne_outside_open line 251
  11. theorem OAI.RelativeDenominators.finite_support_ord line 288
  12. def OAI.RelativeDenominators.principalDivisor line 304
  13. theorem OAI.RelativeDenominators.principalDivisor_apply line 309
  14. theorem OAI.RelativeDenominators.exists_stalk_unit_of_ord_eq_zero line 315
  15. theorem OAI.RelativeDenominators.exists_affine_section_of_ord_eq_zero line 330
  16. theorem OAI.RelativeDenominators.germToFunctionField_map line 369
  17. instance OAI.RelativeDenominators.nonempty_top_of_integral line 377
  18. theorem OAI.RelativeDenominators.exists_section_of_ord_eq_zero line 381
  19. theorem OAI.RelativeDenominators.exists_global_section_of_ord_eq_zero line 419
  20. theorem OAI.RelativeDenominators.exists_section_unit_of_ord_eq_zero line 428
  21. theorem OAI.RelativeDenominators.rational_function_eq_global_unit_of_divisor_zero line 455
  22. theorem OAI.RelativeDenominators.genericPoint_eq_of_dominant line 467
  23. def OAI.RelativeDenominators.functionFieldPullback line 475
  24. instance OAI.RelativeDenominators.nonempty_preimage_of_dominant line 481
  25. theorem OAI.RelativeDenominators.functionFieldPullback_germ line 492
  26. def OAI.RelativeDenominators.IsVerticalDivisor line 507
  27. theorem OAI.RelativeDenominators.exists_open_avoiding_vertical_divisor line 513
  28. theorem OAI.RelativeDenominators.rational_function_descends_of_vertical_divisor line 535