OAI/NumberTheory/PiExponent/Cohomology/PencilCohomologyCech.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponentSeshadri.ExtCokernel.quotientEquiv line 14
  2. abbrev OAI.PiExponentSeshadri.Geometry.schemeFreeOpen line 52

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

  3. abbrev OAI.PiExponentSeshadri.Geometry.schemeShortComplex line 55
  4. abbrev OAI.PiExponentSeshadri.Geometry.schemeFreeOpenEquiv line 58
  5. def OAI.PiExponentSeshadri.Geometry.twoChartImage line 62
  6. lemma OAI.PiExponentSeshadri.Geometry.twoChartImage_eq line 67
  7. def OAI.PiExponentSeshadri.Geometry.twoAffineUnionExtOne line 114
  8. def OAI.PiExponentSeshadri.Geometry.extSourceIso line 133
  9. def OAI.PiExponentSeshadri.Geometry.twoAffineCohomologyOne line 146
  10. theorem OAI.PiExponentSeshadri.Geometry.BaseSections.two_chart_cokernel_finite line 162
  11. def OAI.PiExponentSeshadri.Geometry.BaseSections.twoBaseImage line 212
  12. def OAI.PiExponentSeshadri.Geometry.BaseSections.twoBaseCohomologyOne line 222