OAI/NumberTheory/PiExponent/Ampleness/AdmissibleBlowupGeometry.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.AdmissibleBlowupGeometry.scale line 17
  2. abbrev OAI.PiExponent.AdmissibleBlowupGeometry.Index line 21
  3. abbrev OAI.PiExponent.AdmissibleBlowupGeometry.exponents line 22
  4. abbrev OAI.PiExponent.AdmissibleBlowupGeometry.constantIndex line 23
  5. abbrev OAI.PiExponent.AdmissibleBlowupGeometry.coordinateIndex line 24
  6. abbrev OAI.PiExponent.AdmissibleBlowupGeometry.pureIndex line 26
  7. instance OAI.PiExponent.AdmissibleBlowupGeometry.index_nonempty line 29
  8. abbrev OAI.PiExponent.AdmissibleBlowupGeometry.compactification line 31
  9. def OAI.PiExponent.AdmissibleBlowupGeometry.compactificationStructureMap line 33
  10. instance OAI.PiExponent.AdmissibleBlowupGeometry.compactificationStructureMap_proper line 36
  11. def OAI.PiExponent.AdmissibleBlowupGeometry.affineChart line 40
  12. instance OAI.PiExponent.AdmissibleBlowupGeometry.affineChart_isOpenImmersion line 45
  13. def OAI.PiExponent.AdmissibleBlowupGeometry.origin line 49
  14. instance OAI.PiExponent.AdmissibleBlowupGeometry.compactification_nonempty line 52
  15. instance OAI.PiExponent.AdmissibleBlowupGeometry.compactification_isIntegral line 53
  16. instance OAI.PiExponent.AdmissibleBlowupGeometry.compactification_isLocallyNoetherian line 54
  17. instance OAI.PiExponent.AdmissibleBlowupGeometry.compactification_compact line 56
  18. instance OAI.PiExponent.AdmissibleBlowupGeometry.compactification_isNoetherian line 58
  19. instance OAI.PiExponent.AdmissibleBlowupGeometry.affineChart_quasiCompact line 59
  20. theorem OAI.PiExponent.AdmissibleBlowupGeometry.affineChart_over line 61
  21. def OAI.PiExponent.AdmissibleBlowupGeometry.hyperplane line 67
  22. theorem OAI.PiExponent.AdmissibleBlowupGeometry.hyperplane_ample line 68
  23. def OAI.PiExponent.AdmissibleBlowupGeometry.logCutoff line 71
  24. theorem OAI.PiExponent.AdmissibleBlowupGeometry.logCutoff_strict line 74
  25. def OAI.PiExponent.AdmissibleBlowupGeometry.centerIdeal line 78
  26. theorem OAI.PiExponent.AdmissibleBlowupGeometry.centerIdeal_restrict line 81
  27. theorem OAI.PiExponent.AdmissibleBlowupGeometry.centerIdeal_support line 85
  28. theorem OAI.PiExponent.AdmissibleBlowupGeometry.centerIdeal_support_finite line 90
  29. theorem OAI.PiExponent.AdmissibleBlowupGeometry.centerIdeal_support_subset_chart line 95
  30. theorem OAI.PiExponent.AdmissibleBlowupGeometry.centerIdeal_coherent line 102
  31. theorem OAI.PiExponent.AdmissibleBlowupGeometry.origin_ne_center line 106
  32. theorem OAI.PiExponent.AdmissibleBlowupGeometry.origin_avoids_center line 115
  33. theorem OAI.PiExponent.AdmissibleBlowupGeometry.centerIdeal_support_ne_top line 130
  34. abbrev OAI.PiExponent.AdmissibleBlowupGeometry.blowup line 134
  35. abbrev OAI.PiExponent.AdmissibleBlowupGeometry.projection line 135
  36. def OAI.PiExponent.AdmissibleBlowupGeometry.structureMap line 137
  37. instance OAI.PiExponent.AdmissibleBlowupGeometry.projection_proper line 139
  38. instance OAI.PiExponent.AdmissibleBlowupGeometry.structureMap_proper line 140
  39. instance OAI.PiExponent.AdmissibleBlowupGeometry.blowup_isIntegral line 143
  40. instance OAI.PiExponent.AdmissibleBlowupGeometry.blowup_isLocallyNoetherian line 145
  41. instance OAI.PiExponent.AdmissibleBlowupGeometry.blowup_compact line 147
  42. instance OAI.PiExponent.AdmissibleBlowupGeometry.blowup_isNoetherian line 149
  43. def OAI.PiExponent.AdmissibleBlowupGeometry.A line 151
  44. abbrev OAI.PiExponent.AdmissibleBlowupGeometry.J line 152
  45. abbrev OAI.PiExponent.AdmissibleBlowupGeometry.exceptionalInclusion line 154
  46. theorem OAI.PiExponent.AdmissibleBlowupGeometry.exceptional_presents line 157
  47. theorem OAI.PiExponent.AdmissibleBlowupGeometry.isBlowup line 161
  48. abbrev OAI.PiExponent.AdmissibleBlowupGeometry.affinePolynomialIdeal line 164
  49. theorem OAI.PiExponent.AdmissibleBlowupGeometry.formalJet_packet_zero line 167