OAI/NumberTheory/PiExponent/Ampleness/GlobalExceptionalComparison.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PiExponentSeshadri.BlowupGluing.affineCenterIdeal line 13
  2. theorem OAI.PiExponentSeshadri.BlowupGluing.affineRestrictionIso_hom_reesProjection line 16
  3. def OAI.PiExponentSeshadri.BlowupGluing.restrictedExceptionalLineBundle line 24
  4. def OAI.PiExponentSeshadri.BlowupGluing.restrictedExceptionalInclusion line 27
  5. def OAI.PiExponentSeshadri.BlowupGluing.affineExceptionalOnRestriction line 33
  6. def OAI.PiExponentSeshadri.BlowupGluing.affineExceptionalInclusionOnRestriction line 38
  7. theorem OAI.PiExponentSeshadri.BlowupGluing.restrictedExceptional_presents line 46
  8. theorem OAI.PiExponentSeshadri.BlowupGluing.affineExceptionalOnRestriction_presents line 53
  9. def OAI.PiExponentSeshadri.BlowupGluing.exceptionalAffineIso line 63
  10. theorem OAI.PiExponentSeshadri.BlowupGluing.exceptionalAffineIso_hom_inclusion line 69
  11. def OAI.PiExponentSeshadri.BlowupGluing.exceptionalAffinePowerIso line 74
  12. theorem OAI.PiExponentSeshadri.BlowupGluing.exceptionalAffinePowerIso_hom_inclusion line 79
  13. def OAI.PiExponentSeshadri.BlowupGluing.restrictedExceptionalPowerAffineIso line 87