OAI/AlgebraicGeometry/Seshadri/Sheaves/AffineLocalizing.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MaximalSeshadri.Geometry.quasicoherent_pushforward_iso line 18
  2. abbrev OAI.MaximalSeshadri.Geometry.affineToSpecModule line 30
  3. instance OAI.MaximalSeshadri.Geometry.affineToSpecModule_quasicoherent line 33
  4. theorem OAI.MaximalSeshadri.Geometry.affine_sections_localize line 37
  5. def OAI.MaximalSeshadri.Geometry.affineSpecSections line 44
  6. def OAI.MaximalSeshadri.Geometry.openSectionsCongr line 70
  7. lemma OAI.MaximalSeshadri.Geometry.openSectionsCongr_restriction line 75
  8. theorem OAI.MaximalSeshadri.Geometry.affine_openRestriction_localize line 81
  9. theorem OAI.MaximalSeshadri.Geometry.affine_basicOpen_denominators line 100
  10. def OAI.MaximalSeshadri.Geometry.openTopSections line 109
  11. theorem OAI.MaximalSeshadri.Geometry.LineBundle.affine_openSections_finite line 127
  12. theorem OAI.MaximalSeshadri.Geometry.affine_sections_denominators line 134