OAI/AlgebraicGeometry/Seshadri/Blowup/Uniqueness.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaximalSeshadri.SpecMaps.coordinate line 13
2. lemma OAI.MaximalSeshadri.SpecMaps.coordinate_ext line 16
3. lemma OAI.MaximalSeshadri.SpecMaps.coordinate_comp line 20
4. lemma OAI.MaximalSeshadri.SpecMaps.coordinate_spec line 24
5. lemma OAI.MaximalSeshadri.SpecMaps.coordinate_comp_spec line 27
6. lemma OAI.MaximalSeshadri.SpecMaps.factor line 31
7. lemma OAI.MaximalSeshadri.SpecMaps.preimage_basicOpen line 37
8. lemma OAI.MaximalSeshadri.SpecMaps.isUnit_of_basicOpen_eq_top line 43
9. lemma OAI.MaximalSeshadri.SpecMaps.isUnit_coordinate_of_preimage_top line 50
10. lemma OAI.MaximalSeshadri.SpecMaps.ideal_unit_generator line 55
11. lemma OAI.MaximalSeshadri.ReesGrading.chart_scheme_ext line 81
12. lemma OAI.MaximalSeshadri.ReesGrading.ext_of_unit_generator line 93
13. lemma OAI.MaximalSeshadri.SchematicExt.ext_of_ker_eq_bot_of_isSeparated line 149
14. lemma OAI.MaximalSeshadri.SchematicExt.basicOpen_ker_eq_bot line 171
15. lemma OAI.MaximalSeshadri.ReesGrading.ext_on_generator_open line 196
16. lemma OAI.MaximalSeshadri.ReesGrading.ext_of_unit_ideal line 209
17. lemma OAI.MaximalSeshadri.ReesGrading.principal_basicOpen_unit_ideal line 221
18. lemma OAI.MaximalSeshadri.ReesGrading.principal_unique line 231