OAI/AlgebraicGeometry/Seshadri/Blowup/ExceptionalIdeal.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MaximalSeshadri.Geometry.lineBundleOfCover line 11
  2. def OAI.MaximalSeshadri.Geometry.idealLineBundle line 18
  3. def OAI.MaximalSeshadri.ReesGrading.exceptionalIdeal line 36
  4. def OAI.MaximalSeshadri.ReesGrading.chartEquation line 39
  5. lemma OAI.MaximalSeshadri.ReesGrading.exceptional_chart line 42
  6. lemma OAI.MaximalSeshadri.ReesGrading.chartEquation_regular line 53
  7. def OAI.MaximalSeshadri.ReesGrading.exceptionalLineBundle line 64
  8. def OAI.MaximalSeshadri.ReesGrading.exceptionalInclusion line 68
  9. instance OAI.MaximalSeshadri.ReesGrading.exceptionalInclusion_mono line 71
  10. lemma OAI.MaximalSeshadri.ReesGrading.exceptional_presents line 80
  11. theorem OAI.MaximalSeshadri.ReesGrading.exceptional_invertible line 87
  12. def OAI.MaximalSeshadri.BlowupLift.coefficient line 101
  13. lemma OAI.MaximalSeshadri.BlowupLift.mul_coefficient line 105
  14. lemma OAI.MaximalSeshadri.BlowupLift.coefficients_span line 111