OAI/AlgebraicGeometry/NumericalDimension/AmpleAbsorption.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Ample Absorption.

  1. lemma OAI.NumericalDimensionOne.canonical_difference_nonpos_shared_fiber line 31
  2. lemma OAI.NumericalDimensionOne.canonical_difference_negative_shared_fiber line 50
  3. lemma OAI.NumericalDimensionOne.surfacePrimePair_zero_outside_fiber_open line 90
  4. lemma OAI.NumericalDimensionOne.surfacePrimePair_zero_distinct_fibers line 101
  5. def OAI.NumericalDimensionOne.surfaceWeilPrimeDegreeHom line 121
  6. lemma OAI.NumericalDimensionOne.surfaceWeilDegree_local_nonneg line 126
  7. lemma OAI.NumericalDimensionOne.surface_exceptional_row_le line 155
  8. lemma OAI.NumericalDimensionOne.exists_primeDivisor_curve line 202
  9. lemma OAI.NumericalDimensionOne.surface_prime_morphism_generic line 209
  10. lemma OAI.NumericalDimensionOne.surfaceCartierPrimeDegree_positive_of_ample line 216
  11. lemma OAI.NumericalDimensionOne.surfaceIntersection_positive_of_ample_effective line 232
  12. lemma OAI.NumericalDimensionOne.linearSystem_avoid_finite_of_witnesses line 261
  13. theorem OAI.NumericalDimensionOne.principalWeilDivisor_mul line 319
  14. theorem OAI.NumericalDimensionOne.principalWeilDivisor_one line 324
  15. theorem OAI.NumericalDimensionOne.principalWeilDivisor_inv line 329
  16. theorem OAI.NumericalDimensionOne.principalWeilDivisor_pow line 334
  17. theorem OAI.NumericalDimensionOne.isCartierDivisor_principal line 341
  18. lemma OAI.NumericalDimensionOne.principal_shift_identity line 360
  19. lemma OAI.NumericalDimensionOne.divisorSection_iff_effective line 369
  20. lemma OAI.NumericalDimensionOne.isAmpleDivisor_add_principal line 374
  21. theorem OAI.NumericalDimensionOne.isAmpleDivisor_add_principal_iff line 391
  22. lemma OAI.NumericalDimensionOne.prime_eq_of_specializes line 413
  23. lemma OAI.NumericalDimensionOne.prime_mem_divisorSupport_iff line 423
  24. lemma OAI.NumericalDimensionOne.generic_not_divisorSupport line 436
  25. lemma OAI.NumericalDimensionOne.divisorSupport_nsmul line 447
  26. lemma OAI.NumericalDimensionOne.sectionNonvanishing_pow line 457
  27. lemma OAI.NumericalDimensionOne.isAmpleDivisor_nsmul line 466
  28. theorem OAI.NumericalDimensionOne.exists_ample_twist_dominating line 484
  29. lemma OAI.NumericalDimensionOne.exists_effective_ample_avoiding_primes line 545