OAI/AlgebraicGeometry/Seshadri/Cohomology/SheafExactness.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MaximalSeshadri.TildeFlasque.top_surjective line 18
  2. theorem OAI.MaximalSeshadri.TildeFlasque.flasque_of_injective_global line 38
  3. instance OAI.MaximalSeshadri.TildeFlasque.tilde_injective_isFlasque line 50
  4. instance OAI.MaximalSeshadri.TildeExact.map_mono line 67
  5. instance OAI.MaximalSeshadri.TildeExact.preservesMonomorphisms line 77
  6. instance OAI.MaximalSeshadri.TildeExact.preservesHomology line 80
  7. instance OAI.MaximalSeshadri.TildeExact.preservesFiniteLimits line 83
  8. instance OAI.MaximalSeshadri.ModuleGrothendieck.presheafAB5 line 95
  9. instance OAI.MaximalSeshadri.ModuleGrothendieck.presheafHasSeparator line 99
  10. instance OAI.MaximalSeshadri.ModuleGrothendieck.presheafGrothendieck line 103
  11. instance OAI.MaximalSeshadri.ModuleGrothendieck.sheafAB5 line 108
  12. lemma OAI.MaximalSeshadri.ModuleGrothendieck.freeSheafSeparating line 112
  13. instance OAI.MaximalSeshadri.ModuleGrothendieck.sheafHasSeparator line 126
  14. instance OAI.MaximalSeshadri.ModuleGrothendieck.sheafGrothendieck line 131
  15. theorem OAI.MaximalSeshadri.ModuleGrothendieck.enoughInjectives line 133
  16. abbrev OAI.MaximalSeshadri.ModuleFlasque.freeOpen line 145
  17. abbrev OAI.MaximalSeshadri.ModuleFlasque.freeOpenMap line 149
  18. lemma OAI.MaximalSeshadri.ModuleFlasque.freeMap_mono line 153
  19. instance OAI.MaximalSeshadri.ModuleFlasque.freeOpenMap_mono line 161
  20. def OAI.MaximalSeshadri.ModuleFlasque.freeOpenEquiv line 166
  21. lemma OAI.MaximalSeshadri.ModuleFlasque.freeYoneda_naturality line 171
  22. lemma OAI.MaximalSeshadri.ModuleFlasque.freeOpenEquiv_naturality line 182
  23. theorem OAI.MaximalSeshadri.ModuleFlasque.restriction_surjective line 194
  24. instance OAI.MaximalSeshadri.ModuleFlasque.injective_isFlasque line 203
  25. instance OAI.MaximalSeshadri.ModuleSheafExact.toSheafPreservesColimit line 219
  26. instance OAI.MaximalSeshadri.ModuleSheafExact.toSheafPreservesColimits line 235
  27. theorem OAI.MaximalSeshadri.ModuleSheafExact.shortExact_map line 239