OAI/AlgebraicGeometry/Seshadri/Blowup/PlaneCharts.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MaximalSeshadri.PlaneBlowup.PlaneRing line 12
2. abbrev OAI.MaximalSeshadri.PlaneBlowup.originIdeal line 13
3. def OAI.MaximalSeshadri.PlaneBlowup.coordinate line 15
4. def OAI.MaximalSeshadri.PlaneBlowup.chartSubstitution line 18
5. lemma OAI.MaximalSeshadri.PlaneBlowup.substitution_C line 21
6. lemma OAI.MaximalSeshadri.PlaneBlowup.substitution_self line 24
7. lemma OAI.MaximalSeshadri.PlaneBlowup.substitution_other line 27
8. lemma OAI.MaximalSeshadri.PlaneBlowup.substitution_ideal line 31
9. lemma OAI.MaximalSeshadri.PlaneBlowup.substitution_regular line 44
10. def OAI.MaximalSeshadri.PlaneBlowup.toPolynomial line 50
11. lemma OAI.MaximalSeshadri.PlaneBlowup.toPolynomial_base line 54
12. lemma OAI.MaximalSeshadri.PlaneBlowup.toPolynomial_ratio line 58
13. def OAI.MaximalSeshadri.PlaneBlowup.fromPolynomial line 71
14. lemma OAI.MaximalSeshadri.PlaneBlowup.fromPolynomial_C line 77
15. lemma OAI.MaximalSeshadri.PlaneBlowup.fromPolynomial_self line 81
16. lemma OAI.MaximalSeshadri.PlaneBlowup.fromPolynomial_other line 85
17. lemma OAI.MaximalSeshadri.PlaneBlowup.from_substitution line 89
18. lemma OAI.MaximalSeshadri.PlaneBlowup.to_from line 101
19. lemma OAI.MaximalSeshadri.PlaneBlowup.from_to line 109
20. def OAI.MaximalSeshadri.PlaneBlowup.chartEquiv line 121
21. def OAI.MaximalSeshadri.PlaneBlowup.planePresentation line 133
22. lemma OAI.MaximalSeshadri.PlaneBlowup.plane_standardSmooth line 148
23. def OAI.MaximalSeshadri.PlaneBlowup.planeCover line 155
24. def OAI.MaximalSeshadri.PlaneBlowup.structureMap line 158
25. lemma OAI.MaximalSeshadri.PlaneBlowup.chart_standardSmooth line 161
26. theorem OAI.MaximalSeshadri.PlaneBlowup.smooth_structureMap line 171
27. theorem OAI.MaximalSeshadri.PlaneBlowup.smooth_etale_baseChange line 197
28. theorem OAI.MaximalSeshadri.PointBlowup.exists_smooth_point_blowup_neighborhood line 235