OAI/NumberTheory/PiExponent/Ampleness/BlowupIdeal.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponentSeshadri.Geometry.sectionImageIdeal line 14
  2. def OAI.PiExponentSeshadri.Geometry.PresentsPullbackIdeal line 22
  3. def OAI.PiExponentSeshadri.Geometry.InvertiblePullbackIdeal line 28
  4. def OAI.PiExponentSeshadri.Geometry.IsBlowup line 31
  5. def OAI.PiExponentSeshadri.IdealModule.sectionFamily line 44
  6. def OAI.PiExponentSeshadri.IdealModule.fromSection line 51
  7. lemma OAI.PiExponentSeshadri.IdealModule.fromSection_app line 54
  8. lemma OAI.PiExponentSeshadri.IdealModule.fromSection_inclusion_app line 58
  9. lemma OAI.PiExponentSeshadri.IdealModule.isIso_fromSection line 73
  10. def OAI.PiExponentSeshadri.IdealModule.restrictedInclusion line 110
  11. instance OAI.PiExponentSeshadri.IdealModule.restrictedInclusion_mono line 115
  12. lemma OAI.PiExponentSeshadri.IdealModule.restrictedInclusion_app line 123
  13. lemma OAI.PiExponentSeshadri.IdealModule.restricted_image line 128
  14. lemma OAI.PiExponentSeshadri.IdealModule.frame_restriction line 151
  15. def OAI.PiExponentSeshadri.IdealModule.frameOnRange line 176
  16. lemma OAI.PiExponentSeshadri.IdealPullback.map_top line 191
  17. lemma OAI.PiExponentSeshadri.IdealPullback.comap_top line 196
  18. def OAI.PiExponentSeshadri.IdealPullback.specIdeal line 218
  19. lemma OAI.PiExponentSeshadri.IdealPullback.specIdeal_top line 221
  20. lemma OAI.PiExponentSeshadri.IdealPullback.specIdeal_comap line 226
  21. lemma OAI.PiExponentSeshadri.IdealPullback.comap_ι_top line 238
  22. lemma OAI.PiExponentSeshadri.IdealPullback.comap_ideal line 246
  23. lemma OAI.PiExponentSeshadri.InvertibleLocal.invertible_of_local_equations line 267
  24. theorem OAI.PiExponentSeshadri.InvertibleLocal.invertible_of_affine_equations line 289