OAI/NumberTheory/PiExponent/Cohomology/PencilCohomologySections.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.PiExponentSeshadri.Geometry.LineBundle.quasicoherent line 16
  2. theorem OAI.PiExponentSeshadri.Geometry.LineBundle.affine_sections_finite line 21
  3. def OAI.PiExponentSeshadri.Geometry.LineBundle.restrict line 26
  4. def OAI.PiExponentSeshadri.Geometry.OpenSections line 46
  5. instance OAI.PiExponentSeshadri.Geometry.(instance at line 47) line 47
  6. instance OAI.PiExponentSeshadri.Geometry.(instance at line 49) line 49
  7. abbrev OAI.PiExponentSeshadri.Geometry.schemeFreeOpen line 52

    Also declared: OAI/NumberTheory/PiExponent/Cohomology/PencilCohomologyCech.lean:52 (same declaration text).

  8. def OAI.PiExponentSeshadri.Geometry.freeOpenHomAddCommGroup line 55
  9. def OAI.PiExponentSeshadri.Geometry.freeOpenLinearEquiv line 64
  10. def OAI.PiExponentSeshadri.Geometry.openRestriction line 70
  11. lemma OAI.PiExponentSeshadri.Geometry.freeOpenLinearEquiv_naturality line 82
  12. theorem OAI.PiExponentSeshadri.Geometry.quasicoherent_pushforward_iso line 94
  13. abbrev OAI.PiExponentSeshadri.Geometry.affineToSpecModule line 106
  14. instance OAI.PiExponentSeshadri.Geometry.affineToSpecModule_quasicoherent line 109
  15. theorem OAI.PiExponentSeshadri.Geometry.affine_sections_localize line 113
  16. def OAI.PiExponentSeshadri.Geometry.affineSpecSections line 120
  17. def OAI.PiExponentSeshadri.Geometry.openSectionsCongr line 146
  18. lemma OAI.PiExponentSeshadri.Geometry.openSectionsCongr_restriction line 151
  19. theorem OAI.PiExponentSeshadri.Geometry.affine_openRestriction_localize line 157
  20. theorem OAI.PiExponentSeshadri.Geometry.affine_basicOpen_denominators line 176
  21. def OAI.PiExponentSeshadri.Geometry.openTopSections line 185
  22. theorem OAI.PiExponentSeshadri.Geometry.LineBundle.affine_openSections_finite line 203
  23. theorem OAI.PiExponentSeshadri.Geometry.affine_sections_denominators line 210
  24. lemma OAI.PiExponentSeshadri.Geometry.restrictScalar_appIso line 223
  25. def OAI.PiExponentSeshadri.Geometry.restrictedOpenSections line 235
  26. lemma OAI.PiExponentSeshadri.Geometry.restrictedOpenSections_naturality line 253
  27. def OAI.PiExponentSeshadri.Geometry.moduleIsoSections line 263
  28. def OAI.PiExponentSeshadri.Geometry.openImmersionTop line 276
  29. theorem OAI.PiExponentSeshadri.Geometry.openImmersionTop_localize line 283
  30. theorem OAI.PiExponentSeshadri.Geometry.openImmersionTop_denominators line 303