OAI/AlgebraicGeometry/Seshadri/Blowup/BlowupIntegral.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.MaximalSeshadri.ProjectiveGeometry.homogeneous_isReduced line 17
2. instance OAI.MaximalSeshadri.ProjectiveGeometry.proj_isReduced line 22
3. def OAI.MaximalSeshadri.ProjectiveGeometry.genericPoint line 27
4. lemma OAI.MaximalSeshadri.ProjectiveGeometry.genericPoint_dense line 34
5. instance OAI.MaximalSeshadri.ProjectiveGeometry.proj_irreducible line 41
6. instance OAI.MaximalSeshadri.ProjectiveGeometry.proj_isIntegral line 48
7. abbrev OAI.MaximalSeshadri.Geometry.centreComplement line 59
8. lemma OAI.MaximalSeshadri.Geometry.ideal_comap_complement line 61
9. lemma OAI.MaximalSeshadri.Geometry.complement_nonempty line 69
10. def OAI.MaximalSeshadri.Geometry.IsBlowup.complementLift line 78
11. lemma OAI.MaximalSeshadri.Geometry.IsBlowup.complementLift_comp line 84
12. instance OAI.MaximalSeshadri.Geometry.(instance at line 91) line 91
13. lemma OAI.MaximalSeshadri.Geometry.IsBlowup.complementLift_range line 96
14. lemma OAI.MaximalSeshadri.Geometry.IsBlowup.nonempty_of_support_ne_top line 106
15. instance OAI.MaximalSeshadri.ReesGrading.polynomial_isReduced line 118
16. instance OAI.MaximalSeshadri.ReesGrading.affineBlowup_isReduced line 123
17. instance OAI.MaximalSeshadri.ReesGrading.affineBlowup_isIntegral line 128
18. instance OAI.MaximalSeshadri.AffineBlowup.scheme_isReduced line 143
19. instance OAI.MaximalSeshadri.AffineBlowup.scheme_isIntegral line 147
20. instance OAI.MaximalSeshadri.BlowupGluing.scheme_isReduced line 159
21. lemma OAI.MaximalSeshadri.Geometry.support_comap_ne_top_of_open line 173
22. lemma OAI.MaximalSeshadri.BlowupGluing.localScheme_isIntegral line 193
23. lemma OAI.MaximalSeshadri.BlowupGluing.cover_range line 201
24. lemma OAI.MaximalSeshadri.BlowupGluing.complement_dense line 207
25. lemma OAI.MaximalSeshadri.BlowupGluing.scheme_isIntegral line 240