OAI/AlgebraicGeometry/NumericalDimension/CanonicalPullbacks.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Canonical Pullbacks.

  1. lemma OAI.NumericalDimensionOne.rationalTopFormPullback_birational_bijective line 16
  2. lemma OAI.NumericalDimensionOne.exists_canonicalDivisorOf_nonzero line 35
  3. lemma OAI.NumericalDimensionOne.exists_canonicalDivisorOf_birational_pullback line 57
  4. lemma OAI.NumericalDimensionOne.CompatibleCanonicalData.iff_morphism line 80
  5. def OAI.NumericalDimensionOne.canonicalModelOfForm line 107
  6. lemma OAI.NumericalDimensionOne.exists_common_canonicalDivisor line 120
  7. lemma OAI.NumericalDimensionOne.exists_qCartierPullback line 163
  8. lemma OAI.NumericalDimensionOne.restricted_partialIso_map line 185
  9. lemma OAI.NumericalDimensionOne.common_model_on_partial_locus line 194
  10. lemma OAI.NumericalDimensionOne.common_model_prime_noExtraction line 255
  11. lemma OAI.NumericalDimensionOne.canonical_comparison_support_and_strictness line 282
  12. lemma OAI.NumericalDimensionOne.HasEffectiveCanonicalComparison.of_birational_morphism line 343
  13. lemma OAI.NumericalDimensionOne.IsQCartierPullback.add line 386
  14. lemma OAI.NumericalDimensionOne.IsQCartierPullback.neg line 413
  15. lemma OAI.NumericalDimensionOne.IsQCartierPullback.sub line 428
  16. lemma OAI.NumericalDimensionOne.IsQCartierPullback.mono line 433
  17. lemma OAI.NumericalDimensionOne.rationalWeilDivisor_injective line 450
  18. lemma OAI.NumericalDimensionOne.rationalWeilDivisor_nsmul line 457
  19. lemma OAI.NumericalDimensionOne.multiples_cross_equal line 463
  20. lemma OAI.NumericalDimensionOne.cartierCurveDegree_nsmul line 471
  21. lemma OAI.NumericalDimensionOne.isNefCartier_of_positive_multiple line 476
  22. theorem OAI.NumericalDimensionOne.isNefQDivisor_iff_one_multiple line 484
  23. lemma OAI.NumericalDimensionOne.isNefCartier_of_generated line 504
  24. lemma OAI.NumericalDimensionOne.isNefCartier_of_isAmple line 510
  25. theorem OAI.NumericalDimensionOne.isNefQDivisor_of_isAmple line 522
  26. structure OAI.NumericalDimensionOne.CartierMultiple line 540
  27. def OAI.NumericalDimensionOne.chooseCartierMultiple line 547
  28. def OAI.NumericalDimensionOne.CartierMultiple.degreeOn line 553
  29. def OAI.NumericalDimensionOne.qCartierCurveDegree line 558