OAI/AlgebraicGeometry/Seshadri/Blowup/FiniteCenters.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MaximalSeshadri.FinitePointBlowup.comap_mul_open line 13
  2. lemma OAI.MaximalSeshadri.FinitePointBlowup.comap_prod_open line 25
  3. lemma OAI.MaximalSeshadri.FinitePointBlowup.comap_eq_top_of_disjoint line 33
  4. def OAI.MaximalSeshadri.FinitePointBlowup.pointCentre line 44
  5. def OAI.MaximalSeshadri.FinitePointBlowup.pointOpen line 46
  6. def OAI.MaximalSeshadri.FinitePointBlowup.outsideOpen line 49
  7. lemma OAI.MaximalSeshadri.FinitePointBlowup.pointOpen_comap_other line 52
  8. lemma OAI.MaximalSeshadri.FinitePointBlowup.pointOpen_comap_centre line 60
  9. lemma OAI.MaximalSeshadri.FinitePointBlowup.outside_comap_centre line 68
  10. lemma OAI.MaximalSeshadri.FinitePointBlowup.mem_finite_iSup_closed line 72
  11. lemma OAI.MaximalSeshadri.FinitePointBlowup.mem_pointOpen line 84
  12. lemma OAI.MaximalSeshadri.FinitePointBlowup.mem_centre_support line 90
  13. lemma OAI.MaximalSeshadri.FinitePointBlowup.point_support line 118
  14. lemma OAI.MaximalSeshadri.FinitePointBlowup.point_mem_own_open line 133
  15. def OAI.MaximalSeshadri.FinitePointBlowup.pointCover line 144
  16. theorem OAI.MaximalSeshadri.FinitePointBlowup.smooth_finite_point_blowup line 159
  17. theorem OAI.MaximalSeshadri.FinitePointBlowup.exceptional_invertible line 209
  18. theorem OAI.MaximalSeshadri.FinitePointBlowup.finite_point_power_contraction line 260
  19. lemma OAI.MaximalSeshadri.FinitePointBlowup.point_ideals_sup line 312
  20. def OAI.MaximalSeshadri.FinitePointBlowup.idealEvaluation line 320
  21. theorem OAI.MaximalSeshadri.FinitePointBlowup.point_powers_prod_eq_inf line 328
  22. theorem OAI.MaximalSeshadri.FinitePointBlowup.point_centre_power_eq_inf line 344
  23. lemma OAI.MaximalSeshadri.IdealPullback.comap_mul line 356
  24. lemma OAI.MaximalSeshadri.IdealPullback.comap_prod line 378
  25. lemma OAI.MaximalSeshadri.FinitePointBlowup.pointOpen_comap_weighted line 395
  26. lemma OAI.MaximalSeshadri.FinitePointBlowup.outside_comap_point line 407
  27. lemma OAI.MaximalSeshadri.FinitePointBlowup.outside_comap_weighted line 413
  28. theorem OAI.MaximalSeshadri.FinitePointBlowup.weighted_power_contraction line 425