OAI/AlgebraicGeometry/Seshadri/Intersection/EulerExact.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MaximalSeshadri.Cohomology.alternatingTrunc line 15
  2. lemma OAI.MaximalSeshadri.Cohomology.alternatingTrunc_succ line 18
  3. lemma OAI.MaximalSeshadri.Cohomology.alternating_rank_identity line 22
  4. lemma OAI.MaximalSeshadri.Cohomology.finrank_middle_of_exact line 36
  5. def OAI.MaximalSeshadri.Cohomology.extEuler line 49
  6. def OAI.MaximalSeshadri.Cohomology.cohomologyMap₁ line 54
  7. def OAI.MaximalSeshadri.Cohomology.cohomologyMap₂ line 57
  8. def OAI.MaximalSeshadri.Cohomology.cohomologyBoundary line 60
  9. lemma OAI.MaximalSeshadri.Cohomology.cohomology_exact₂ line 64
  10. lemma OAI.MaximalSeshadri.Cohomology.cohomology_exact₃ line 74
  11. lemma OAI.MaximalSeshadri.Cohomology.cohomology_exact₁ line 84
  12. theorem OAI.MaximalSeshadri.Cohomology.extEuler_add_of_boundary_zero line 94
  13. theorem OAI.MaximalSeshadri.Cohomology.extEuler_add line 150
  14. def OAI.MaximalSeshadri.Geometry.sheafComplexLinear line 169
  15. def OAI.MaximalSeshadri.Geometry.complexExtModule line 179
  16. lemma OAI.MaximalSeshadri.Geometry.complexExtModule_eq line 183
  17. lemma OAI.MaximalSeshadri.Geometry.eulerCharacteristic_eq_extEuler line 192
  18. theorem OAI.MaximalSeshadri.Geometry.eulerCharacteristic_add line 203