OAI/AlgebraicGeometry/SectionFields/Recovery.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Complete divisorial section fields, containment and conditional recovery.

  1. theorem OAI.RelativeDenominators.exists_stalk_element_of_ord_nonneg line 17
  2. theorem OAI.RelativeDenominators.exists_affine_section_of_ord_nonneg line 31
  3. theorem OAI.RelativeDenominators.exists_section_of_ord_nonneg line 70
  4. theorem OAI.RelativeDenominators.rational_function_descends_of_no_horizontal_poles line 109
  5. def OAI.RelativeDenominators.divisorialSections line 150
  6. def OAI.RelativeDenominators.sectionField line 155
  7. theorem OAI.RelativeDenominators.mem_divisorialSections_iff line 162
  8. theorem OAI.RelativeDenominators.mul_mem_divisorialSections line 184
  9. theorem OAI.RelativeDenominators.pow_mem_divisorialSections line 196
  10. theorem OAI.RelativeDenominators.sectionField_le_positive_multiple line 209
  11. theorem OAI.RelativeDenominators.divisorialSections_nonempty_positive_multiple line 227
  12. theorem OAI.RelativeDenominators.ord_nonneg_of_section line 236
  13. theorem OAI.RelativeDenominators.pullbackQCartier_effective line 245
  14. theorem OAI.RelativeDenominators.pullback_mem_divisorialSections line 278
  15. theorem OAI.RelativeDenominators.lift_section_of_exact_presentation line 298
  16. theorem OAI.RelativeDenominators.section_quotient_descends_of_exact_presentation line 317
  17. theorem OAI.RelativeDenominators.sectionField_le_base_of_exact_presentation line 343
  18. theorem OAI.RelativeDenominators.base_sectionField_le_of_exact_presentation line 366
  19. theorem OAI.RelativeDenominators.sectionField_eq_base_of_exact_presentation line 390
  20. theorem OAI.RelativeDenominators.positive_multiple_exact_presentation line 412
  21. theorem OAI.RelativeDenominators.multiples_recover_base_of_exact_presentation_and_base_system line 435
  22. def OAI.RelativeDenominators.allDegreeSectionField line 472
  23. theorem OAI.RelativeDenominators.sectionField_le_base_of_rational_presentation line 478
  24. theorem OAI.RelativeDenominators.sectionField_le_base_of_rationallyLinearlyEquivalent_pullback line 497
  25. theorem OAI.RelativeDenominators.allDegreeSectionField_le_base_of_rationallyLinearlyEquivalent_pullback line 516
  26. theorem OAI.RelativeDenominators.allDegreeSectionField_eq_base_of_exact_presentation_and_base_system line 531