OAI/AlgebraicGeometry/NumericalDimension/MultiplierIdeals.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Multiplier Ideals.

  1. def OAI.NumericalDimensionOne.ceilQWeilDivisor line 30
  2. lemma OAI.NumericalDimensionOne.ceilQWeilDivisor_apply line 33
  3. theorem OAI.NumericalDimensionOne.valuativeMultiplierIdeal_model_section line 37
  4. lemma OAI.NumericalDimensionOne.divisorSectionOn_dominant_pullback line 106
  5. lemma OAI.NumericalDimensionOne.snc_model_section_discrepancy_bound line 134
  6. lemma OAI.NumericalDimensionOne.canonical_coefficient_of_stalk_iso_scheme line 233
  7. lemma OAI.NumericalDimensionOne.exists_canonicalDivisorOf_nonzero_scheme line 310
  8. theorem OAI.NumericalDimensionOne.lift_near_prime_divisor_of_proper_birational line 333
  9. lemma OAI.NumericalDimensionOne.MultiplierDivisorialTest.regularMap_fraction line 389
  10. lemma OAI.NumericalDimensionOne.valuativeMultiplierIdeal_identity_inequality line 400
  11. theorem OAI.NumericalDimensionOne.mem_valuativeMultiplierIdeal_iff_section_on_snc_model line 433