OAI/AlgebraicGeometry/NumericalDimension/MultiplierDescent.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Multiplier Descent.

  1. lemma OAI.NumericalDimensionOne.open_regular_iff_nonnegative_orders line 30
  2. lemma OAI.NumericalDimensionOne.roundup_section_descends_regular line 72
  3. theorem OAI.NumericalDimensionOne.multiplier_sections_iff_roundup_sections line 117
  4. lemma OAI.NumericalDimensionOne.regularFunctionValues_pullback line 181
  5. def OAI.NumericalDimensionOne.multiplierToRoundupApp line 208
  6. def OAI.NumericalDimensionOne.multiplierToRoundup line 258
  7. lemma OAI.NumericalDimensionOne.multiplierToRoundupApp_bijective line 300
  8. theorem OAI.NumericalDimensionOne.multiplierModuleSheaf_iso_pushforward_on_snc_model line 381
  9. lemma OAI.NumericalDimensionOne.divisorSectionOn_pullback line 436
  10. lemma OAI.NumericalDimensionOne.divisorSectionOn_mul line 459
  11. lemma OAI.NumericalDimensionOne.divisorFunctionLocal_pullback line 473
  12. lemma OAI.NumericalDimensionOne.divisorFunctionLocal_mul line 492
  13. lemma OAI.NumericalDimensionOne.cartier_open_section_iff line 508
  14. def OAI.NumericalDimensionOne.cartierOpenChartMap line 521
  15. lemma OAI.NumericalDimensionOne.cartierOpenChartMap_bijective line 544
  16. def OAI.NumericalDimensionOne.cartierOpenChartEquiv line 563