OAI/NumberTheory/PiExponent/Cohomology/CurveEuler.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponentSeshadri.Geometry.restrictScalar line 16
  2. lemma OAI.PiExponentSeshadri.Geometry.restrictScalar_naturality line 19
  3. def OAI.PiExponentSeshadri.Geometry.sheafHomSMul line 25
  4. instance OAI.PiExponentSeshadri.Geometry.sheafHomModule line 49
  5. instance OAI.PiExponentSeshadri.Geometry.sheafLinear line 79
  6. instance OAI.PiExponentSeshadri.Geometry.schemeHasExt line 97
  7. def OAI.PiExponentSeshadri.Geometry.baseScalars line 99
  8. abbrev OAI.PiExponentSeshadri.Geometry.complexSectionModule line 102
  9. abbrev OAI.PiExponentSeshadri.Geometry.cohomology line 106
  10. def OAI.PiExponentSeshadri.Geometry.cohomologyDimension line 109
  11. def OAI.PiExponentSeshadri.Geometry.eulerCharacteristic line 115
  12. def OAI.PiExponentSeshadri.Geometry.globalHomLinearEquiv line 124
  13. def OAI.PiExponentSeshadri.Geometry.cohomologyZeroSections line 136
  14. lemma OAI.PiExponentSeshadri.Geometry.cohomologyDimension_zero line 147
  15. theorem OAI.PiExponentSeshadri.Geometry.affine_eulerCharacteristic line 155