OAI/AlgebraicGeometry/Seshadri/Blowup/PrincipalCharts.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaximalSeshadri.ReesGrading.principalToLocalization line 15
2. lemma OAI.MaximalSeshadri.ReesGrading.principalToLocalization_base line 19
3. lemma OAI.MaximalSeshadri.ReesGrading.principalToLocalization_generator line 24
4. lemma OAI.MaximalSeshadri.ReesGrading.principalToLocalization_range line 36
5. lemma OAI.MaximalSeshadri.ReesGrading.principalLocalization_injective line 56
6. def OAI.MaximalSeshadri.ReesGrading.principalMap line 59
7. lemma OAI.MaximalSeshadri.ReesGrading.principalMap_spec line 74
8. lemma OAI.MaximalSeshadri.ReesGrading.principalMap_base line 79
9. lemma OAI.MaximalSeshadri.ReesGrading.principalMap_generator line 84
10. lemma OAI.MaximalSeshadri.ReesGrading.principalMap_irrelevant line 89
11. def OAI.MaximalSeshadri.ReesGrading.principalScheme line 108
12. lemma OAI.MaximalSeshadri.ReesGrading.principalScheme_projection line 113
13. lemma OAI.MaximalSeshadri.ReesGrading.principalScheme_preimage line 125
14. lemma OAI.MaximalSeshadri.ProjBase.basicOpenToSpec_eq line 143
15. lemma OAI.MaximalSeshadri.ProjBase.basicOpenToSpec_mem line 151
16. lemma OAI.MaximalSeshadri.ProjBase.toSpecZero_mem line 160
17. lemma OAI.MaximalSeshadri.ProjBase.toSpecZero_preimage line 171
18. instance OAI.MaximalSeshadri.ReesGrading.projection_separated line 186
19. lemma OAI.MaximalSeshadri.ReesGrading.projection_mem line 191
20. lemma OAI.MaximalSeshadri.ReesGrading.projection_preimage line 197
21. lemma OAI.MaximalSeshadri.ReesGrading.base_generator_comm line 203
22. lemma OAI.MaximalSeshadri.ReesGrading.projection_preimage_le_chart line 210
23. lemma OAI.MaximalSeshadri.ReesGrading.chartHom_ext line 223