OAI/AlgebraicGeometry/NumericalDimension/IndexedTransfer.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Indexed Transfer.

  1. theorem OAI.NumericalDimensionOne.exponent_le_kappaSigma line 36
  2. theorem OAI.NumericalDimensionOne.divisorSectionLimsup_eq_zero_of_kappaSigma_eq_one line 44
  3. theorem OAI.NumericalDimensionOne.le_limsup_of_eventually_le_on_multiples line 58
  4. theorem OAI.NumericalDimensionOne.positive_limsup_of_quadratic_growth_on_multiples line 66
  5. theorem OAI.NumericalDimensionOne.no_quadratic_growth_on_multiples_of_kappaSigma_eq_one line 81
  6. theorem OAI.NumericalDimensionOne.sectionDimension_le_of_injective line 95
  7. theorem OAI.NumericalDimensionOne.sectionDimension_le_of_nonzero_section line 109
  8. theorem OAI.NumericalDimensionOne.exists_fixed_ample_twist_sectionDimension_le line 130
  9. theorem OAI.NumericalDimensionOne.no_quadratic_growth_with_fixed_twist line 139
  10. def OAI.NumericalDimensionOne.birationalPrimeLift line 185
  11. lemma OAI.NumericalDimensionOne.birationalPrimeLift_spec line 188
  12. lemma OAI.NumericalDimensionOne.birationalPrimeLift_injective line 194
  13. def OAI.NumericalDimensionOne.birationalWeilPushforward line 202
  14. lemma OAI.NumericalDimensionOne.birationalWeilPushforward_apply line 205
  15. theorem OAI.NumericalDimensionOne.birationalWeilPushforward_single_of_contracted line 208
  16. theorem OAI.NumericalDimensionOne.birationalWeilPushforward_cartierPullback line 224
  17. theorem OAI.NumericalDimensionOne.divisorSection_birational_descent line 236
  18. theorem OAI.NumericalDimensionOne.birational_sections_linear_injection line 265
  19. theorem OAI.NumericalDimensionOne.sectionDimension_le_birationalWeilPushforward line 296
  20. theorem OAI.NumericalDimensionOne.exists_fixed_ample_twist_on_birational_model line 301
  21. theorem OAI.NumericalDimensionOne.no_quadratic_growth_on_birational_model line 313
  22. theorem OAI.NumericalDimensionOne.sectionDimension_mono line 355
  23. theorem OAI.NumericalDimensionOne.sectionDimension_le_of_cartierPullback line 363
  24. theorem OAI.NumericalDimensionOne.exists_fixed_ample_twist_of_effective_comparison line 372
  25. theorem OAI.NumericalDimensionOne.no_quadratic_growth_under_effective_comparison line 395
  26. theorem OAI.NumericalDimensionOne.exists_fixed_ample_twist_of_indexed_effective_comparison line 444
  27. theorem OAI.NumericalDimensionOne.no_quadratic_growth_under_indexed_effective_comparison line 462
  28. theorem OAI.NumericalDimensionOne.exists_indexed_ample_twist_of_rational_comparison line 520