OAI/NumberTheory/PiExponent/Ampleness/BlowupProperIntegral.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.PiExponentSeshadri.AffineBlowup.projection_proper line 13
  2. instance OAI.PiExponentSeshadri.BlowupGluing.projection_proper line 19
  3. instance OAI.PiExponentSeshadri.ProjectiveGeometry.homogeneous_isReduced line 41
  4. instance OAI.PiExponentSeshadri.ProjectiveGeometry.proj_isReduced line 46
  5. def OAI.PiExponentSeshadri.ProjectiveGeometry.genericPoint line 51
  6. lemma OAI.PiExponentSeshadri.ProjectiveGeometry.genericPoint_dense line 58
  7. instance OAI.PiExponentSeshadri.ProjectiveGeometry.proj_irreducible line 65
  8. instance OAI.PiExponentSeshadri.ProjectiveGeometry.proj_isIntegral line 72
  9. abbrev OAI.PiExponentSeshadri.Geometry.centreComplement line 81
  10. lemma OAI.PiExponentSeshadri.Geometry.ideal_comap_complement line 83
  11. lemma OAI.PiExponentSeshadri.Geometry.complement_nonempty line 91
  12. def OAI.PiExponentSeshadri.Geometry.IsBlowup.complementLift line 100
  13. lemma OAI.PiExponentSeshadri.Geometry.IsBlowup.complementLift_comp line 106
  14. instance OAI.PiExponentSeshadri.Geometry.(instance at line 113) line 113
  15. lemma OAI.PiExponentSeshadri.Geometry.IsBlowup.complementLift_range line 118
  16. lemma OAI.PiExponentSeshadri.Geometry.IsBlowup.nonempty_of_support_ne_top line 128
  17. instance OAI.PiExponentSeshadri.ReesGrading.polynomial_isReduced line 138
  18. instance OAI.PiExponentSeshadri.ReesGrading.affineBlowup_isReduced line 143
  19. instance OAI.PiExponentSeshadri.ReesGrading.affineBlowup_isIntegral line 148
  20. instance OAI.PiExponentSeshadri.AffineBlowup.scheme_isReduced line 161
  21. instance OAI.PiExponentSeshadri.AffineBlowup.scheme_isIntegral line 165
  22. instance OAI.PiExponentSeshadri.BlowupGluing.scheme_isReduced line 175
  23. lemma OAI.PiExponentSeshadri.Geometry.support_comap_ne_top_of_open line 187
  24. lemma OAI.PiExponentSeshadri.BlowupGluing.localScheme_isIntegral line 205
  25. lemma OAI.PiExponentSeshadri.BlowupGluing.cover_range line 213
  26. lemma OAI.PiExponentSeshadri.BlowupGluing.complement_dense line 219
  27. lemma OAI.PiExponentSeshadri.BlowupGluing.scheme_isIntegral line 252