OAI/AlgebraicGeometry/NumericalDimension/DivisorPresheaves.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Divisor Presheaves.

  1. theorem OAI.NumericalDimensionOne.uniform_ample_errors line 26
  2. def OAI.NumericalDimensionOne.IsKltBoundaryOn line 103
  3. lemma OAI.NumericalDimensionOne.principalWeilDivisor_zpow line 138
  4. lemma OAI.NumericalDimensionOne.isAmpleQDivisor_add_rational_principal line 147
  5. theorem OAI.NumericalDimensionOne.exists_fixed_twist_subunit_boundaries line 191
  6. def OAI.NumericalDimensionOne.MultiplierOrderCondition line 304
  7. lemma OAI.NumericalDimensionOne.multiplierOrderCondition_add line 309
  8. lemma OAI.NumericalDimensionOne.multiplierOrderCondition_mul line 336
  9. def OAI.NumericalDimensionOne.multiplierValuationIdeal line 354
  10. theorem OAI.NumericalDimensionOne.multiplierValuationIdeal_eq_top line 381
  11. structure OAI.NumericalDimensionOne.MultiplierDivisorialTest line 406
  12. def OAI.NumericalDimensionOne.MultiplierDivisorialTest.discrepancy line 425
  13. def OAI.NumericalDimensionOne.MultiplierDivisorialTest.valuationIdeal line 429
  14. def OAI.NumericalDimensionOne.MultiplierDivisorialTest.regularMap line 435
  15. def OAI.NumericalDimensionOne.valuativeMultiplierIdeal line 442
  16. lemma OAI.NumericalDimensionOne.mem_valuativeMultiplierIdeal line 447
  17. theorem OAI.NumericalDimensionOne.valuativeMultiplierIdeal_eq_top_of_klt line 473
  18. lemma OAI.NumericalDimensionOne.MultiplierDivisorialTest.regularMap_res line 507
  19. lemma OAI.NumericalDimensionOne.valuativeMultiplierIdeal_res line 515
  20. def OAI.NumericalDimensionOne.multiplierIdealSubfunctor line 524
  21. theorem OAI.NumericalDimensionOne.multiplierIdealSubfunctor_isSheaf line 549
  22. def OAI.NumericalDimensionOne.multiplierModulePresheaf line 587
  23. theorem OAI.NumericalDimensionOne.multiplierModulePresheaf_isSheaf line 623
  24. def OAI.NumericalDimensionOne.multiplierModuleSheaf line 629
  25. def OAI.NumericalDimensionOne.multiplierModuleEquivOfKlt line 633
  26. lemma OAI.NumericalDimensionOne.divisorSectionOn_res line 667
  27. lemma OAI.NumericalDimensionOne.divisorSectionOn_add line 673
  28. lemma OAI.NumericalDimensionOne.order_neg_value line 692
  29. lemma OAI.NumericalDimensionOne.divisorSectionOn_neg line 703
  30. def OAI.NumericalDimensionOne.divisorFunctionPrelocal line 711
  31. def OAI.NumericalDimensionOne.divisorFunctionLocal line 718
  32. lemma OAI.NumericalDimensionOne.divisorFunctionLocal_zero line 721
  33. lemma OAI.NumericalDimensionOne.divisorFunctionLocal_add line 725
  34. lemma OAI.NumericalDimensionOne.divisorFunctionLocal_neg line 738
  35. def OAI.NumericalDimensionOne.divisorFunctionGroup line 747
  36. def OAI.NumericalDimensionOne.divisorFunctionPresheaf line 753