OAI/AlgebraicGeometry/NumericalDimension/MultiplierSheaves.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Multiplier Sheaves.

  1. theorem OAI.NumericalDimensionOne.divisorFunctionPresheaf_isSheaf line 29
  2. theorem OAI.NumericalDimensionOne.divisorFunctionLocal_iff line 34
  3. def OAI.NumericalDimensionOne.divisorFunctionSheaf line 87
  4. def OAI.NumericalDimensionOne.divisorSectionsToSheaf line 90
  5. theorem OAI.NumericalDimensionOne.divisorSectionsToSheaf_bijective line 122
  6. def OAI.NumericalDimensionOne.divisorGlobalSectionsEquiv line 136
  7. def OAI.NumericalDimensionOne.regularFunctionValues line 163
  8. lemma OAI.NumericalDimensionOne.regularFunctionValues_eq line 171
  9. instance OAI.NumericalDimensionOne.divisorFunctionRingModule line 176
  10. lemma OAI.NumericalDimensionOne.divisorFunction_smul_apply line 180
  11. lemma OAI.NumericalDimensionOne.divisorSectionOn_smul line 185
  12. lemma OAI.NumericalDimensionOne.divisorFunctionLocal_smul line 199
  13. def OAI.NumericalDimensionOne.divisorFunctionSubmodule line 216
  14. lemma OAI.NumericalDimensionOne.regularFunctionValues_res line 223
  15. def OAI.NumericalDimensionOne.divisorModulePresheaf line 229
  16. theorem OAI.NumericalDimensionOne.divisorModulePresheaf_isSheaf line 270
  17. def OAI.NumericalDimensionOne.divisorModuleSheaf line 274
  18. def OAI.NumericalDimensionOne.divisorSectionsToModuleSheaf line 277
  19. def OAI.NumericalDimensionOne.cartierSheafChartMap line 310
  20. theorem OAI.NumericalDimensionOne.cartierSheafChartMap_bijective line 356
  21. def OAI.NumericalDimensionOne.cartierSheafChartEquiv line 375
  22. def OAI.NumericalDimensionOne.IsDivisorGerm line 405
  23. lemma OAI.NumericalDimensionOne.isDivisorGerm_add line 408
  24. lemma OAI.NumericalDimensionOne.isDivisorGerm_smul line 416
  25. def OAI.NumericalDimensionOne.divisorRationalStalk line 430
  26. theorem OAI.NumericalDimensionOne.cartier_divisorGerm_iff line 459
  27. def OAI.NumericalDimensionOne.divisorStalkChartMap line 508
  28. theorem OAI.NumericalDimensionOne.divisorStalkChartMap_bijective line 551
  29. def OAI.NumericalDimensionOne.divisorStalkChartEquiv line 565
  30. theorem OAI.NumericalDimensionOne.cartier_divisorRationalStalk_flat line 572
  31. def OAI.NumericalDimensionOne.divisorSectionGermValue line 605
  32. def OAI.NumericalDimensionOne.divisorSheafStalkMap line 615
  33. lemma OAI.NumericalDimensionOne.divisorSheafStalkMap_germ line 625
  34. theorem OAI.NumericalDimensionOne.divisorSheafStalkMap_bijective line 658
  35. def OAI.NumericalDimensionOne.divisorSheafStalkEquiv line 694
  36. def OAI.NumericalDimensionOne.twistedMultiplierModuleSheaf line 720
  37. def OAI.NumericalDimensionOne.twistedMultiplierSectionsEquivOfKlt line 727