OAI/NumberTheory/PiExponent/Ampleness/BlowupSchemeExt.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponentSeshadri.SpecMaps.coordinate line 14
2. lemma OAI.PiExponentSeshadri.SpecMaps.coordinate_ext line 17
3. lemma OAI.PiExponentSeshadri.SpecMaps.coordinate_comp line 21
4. lemma OAI.PiExponentSeshadri.SpecMaps.coordinate_spec line 25
5. lemma OAI.PiExponentSeshadri.SpecMaps.coordinate_comp_spec line 28
6. lemma OAI.PiExponentSeshadri.SpecMaps.factor line 32
7. lemma OAI.PiExponentSeshadri.SpecMaps.preimage_basicOpen line 38
8. lemma OAI.PiExponentSeshadri.SpecMaps.isUnit_of_basicOpen_eq_top line 44
9. lemma OAI.PiExponentSeshadri.SpecMaps.isUnit_coordinate_of_preimage_top line 51
10. lemma OAI.PiExponentSeshadri.SpecMaps.ideal_unit_generator line 56
11. lemma OAI.PiExponentSeshadri.SchematicExt.ext_of_ker_eq_bot_of_isSeparated line 79
12. lemma OAI.PiExponentSeshadri.SchematicExt.basicOpen_ker_eq_bot line 101