OAI/AlgebraicGeometry/Seshadri/Blowup/LocalEquations.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaximalSeshadri.UnitEndomorphism.unit line 13
2. def OAI.MaximalSeshadri.UnitEndomorphism.equation line 16
3. lemma OAI.MaximalSeshadri.UnitEndomorphism.app_eq_mul line 18
4. lemma OAI.MaximalSeshadri.UnitEndomorphism.image_principal line 24
5. lemma OAI.MaximalSeshadri.UnitEndomorphism.equation_regular line 35
6. lemma OAI.MaximalSeshadri.InvertibleLocal.image_eq_comap line 53
7. def OAI.MaximalSeshadri.InvertibleLocal.restrictedInclusion line 61
8. instance OAI.MaximalSeshadri.InvertibleLocal.restrictedInclusion_mono line 65
9. lemma OAI.MaximalSeshadri.InvertibleLocal.restricted_image line 78
10. lemma OAI.MaximalSeshadri.InvertibleLocal.local_equation line 104
11. lemma OAI.MaximalSeshadri.InvertibleLocal.affine_local_equation line 135
12. def OAI.MaximalSeshadri.InvertibleLocal.restrictLineBundle line 152
13. lemma OAI.MaximalSeshadri.InvertibleLocal.presents_restrict line 166
14. lemma OAI.MaximalSeshadri.InvertibleLocal.invertible_restrict line 177
15. lemma OAI.MaximalSeshadri.IdealPullback.specIdeal_coordinate line 191
16. lemma OAI.MaximalSeshadri.ReesGrading.invertible_unique line 208
17. lemma OAI.MaximalSeshadri.ReesGrading.local_lift line 221
18. theorem OAI.MaximalSeshadri.ReesGrading.affineBlowup_universal line 232