OAI/AlgebraicGeometry/Seshadri/Blowup/LocalUniversal.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MaximalSeshadri.Geometry.rees_isBlowup line 14
  2. lemma OAI.MaximalSeshadri.InvertibleLocal.restricted_image_on_chart line 28
  3. lemma OAI.MaximalSeshadri.InvertibleLocal.local_equation_on_chart line 57
  4. lemma OAI.MaximalSeshadri.InvertibleLocal.local_equations line 86
  5. lemma OAI.MaximalSeshadri.InvertibleLocal.invertible_iff_local_equations line 99
  6. lemma OAI.MaximalSeshadri.InvertibleLocal.invertible_congr line 106
  7. lemma OAI.MaximalSeshadri.InvertibleLocal.presents_restrict_general line 118
  8. lemma OAI.MaximalSeshadri.InvertibleLocal.invertible_restrict_general line 131
  9. lemma OAI.MaximalSeshadri.InvertibleLocal.invertible_of_cover line 138
  10. lemma OAI.MaximalSeshadri.Geometry.IsBlowup.hom_ext line 170
  11. lemma OAI.MaximalSeshadri.Geometry.IsBlowup.postIso line 176
  12. lemma OAI.MaximalSeshadri.Geometry.IsBlowup.open_baseChange line 196
  13. def OAI.MaximalSeshadri.Geometry.IsBlowup.iso line 217
  14. lemma OAI.MaximalSeshadri.Geometry.IsBlowup.iso_hom_comp line 233
  15. lemma OAI.MaximalSeshadri.Geometry.IsBlowup.baseChangeSquare line 243
  16. lemma OAI.MaximalSeshadri.IdealPullback.specIdeal_comap_toSpec line 264
  17. lemma OAI.MaximalSeshadri.IdealPullback.comap_isoSpec_inv line 272
  18. abbrev OAI.MaximalSeshadri.AffineBlowup.scheme line 288
  19. def OAI.MaximalSeshadri.AffineBlowup.projection line 290
  20. theorem OAI.MaximalSeshadri.AffineBlowup.isBlowup line 293