OAI/NumberTheory/PiExponent/Ampleness/GlobalBlowupRestriction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponentSeshadri.BlowupGluing.exceptionalLineBundle line 10
2. def OAI.PiExponentSeshadri.BlowupGluing.exceptionalInclusion line 12
3. theorem OAI.PiExponentSeshadri.BlowupGluing.exceptional_presents line 15
4. def OAI.PiExponentSeshadri.BlowupGluing.restrictionIso line 19
5. theorem OAI.PiExponentSeshadri.BlowupGluing.restrictionIso_hom_projection line 24
6. def OAI.PiExponentSeshadri.BlowupGluing.affineRestrictionIso line 28
7. theorem OAI.PiExponentSeshadri.BlowupGluing.affineRestrictionIso_hom_projection line 33