OAI/AlgebraicGeometry/NumericalDimension/RelativeNegativity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Relative Negativity.

  1. lemma OAI.NumericalDimensionOne.nonconstant_curve_in_irreducible_closed_subset line 17
  2. theorem OAI.NumericalDimensionOne.contracted_curve_through_exceptional_point line 70
  3. lemma OAI.NumericalDimensionOne.exists_cartierStalkEquation_of_effective_near line 102
  4. lemma OAI.NumericalDimensionOne.cartierCurveDegree_nonneg_of_effective_near line 119
  5. lemma OAI.NumericalDimensionOne.cartierCurveDegree_pos_of_nonconstant line 152
  6. theorem OAI.NumericalDimensionOne.projective_cartier_negativity line 171
  7. theorem OAI.NumericalDimensionOne.projective_qCartier_negativity line 281
  8. theorem OAI.NumericalDimensionOne.higher_dimensional_negativity_missing line 303
  9. lemma OAI.NumericalDimensionOne.IsCanonicalMMPStep.effective_comparison_on_common_model line 315