OAI/AlgebraicGeometry/Seshadri/Cohomology/SurfaceCech.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MaximalSeshadri.ExtCokernel.higherQuotientEquiv line 17
  2. lemma OAI.MaximalSeshadri.ModuleMayerVietoris.freeOpenMap_comp line 47
  3. def OAI.MaximalSeshadri.ModuleMayerVietoris.shortComplexMap line 51
  4. def OAI.MaximalSeshadri.Geometry.openBoundary line 93
  5. lemma OAI.MaximalSeshadri.Geometry.openBoundary_left line 99
  6. lemma OAI.MaximalSeshadri.Geometry.openBoundary_right line 122
  7. lemma OAI.MaximalSeshadri.Geometry.openBoundary_natural line 146
  8. def OAI.MaximalSeshadri.Geometry.tripleOpen line 168
  9. def OAI.MaximalSeshadri.Geometry.overlapIso line 170
  10. def OAI.MaximalSeshadri.Geometry.tripleSectionBoundary line 176
  11. lemma OAI.MaximalSeshadri.Geometry.openBoundary_surjective line 186
  12. theorem OAI.MaximalSeshadri.Geometry.tripleSectionBoundary_surjective line 203
  13. def OAI.MaximalSeshadri.Geometry.openSectionExt line 225
  14. lemma OAI.MaximalSeshadri.Geometry.openSectionExt_restrict line 233
  15. lemma OAI.MaximalSeshadri.Geometry.tripleSectionBoundary_apply line 246
  16. lemma OAI.MaximalSeshadri.Geometry.tripleSectionBoundary_left line 253
  17. lemma OAI.MaximalSeshadri.Geometry.tripleSectionBoundary_right line 268
  18. lemma OAI.MaximalSeshadri.Geometry.tripleSectionBoundary_top line 283
  19. def OAI.MaximalSeshadri.Geometry.tripleChartImage line 307
  20. lemma OAI.MaximalSeshadri.Geometry.tripleChartImage_le_ker line 314
  21. def OAI.MaximalSeshadri.Geometry.tripleCokernelBoundary line 324
  22. theorem OAI.MaximalSeshadri.Geometry.tripleCokernelBoundary_surjective line 330
  23. def OAI.MaximalSeshadri.Geometry.tripleCohomologyTwo line 340
  24. theorem OAI.MaximalSeshadri.Geometry.tripleCohomologyTwo_surjective line 350