OAI/NumberTheory/PiExponent/Cohomology/EulerExact.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponentSeshadri.Cohomology.alternatingTrunc line 13
  2. lemma OAI.PiExponentSeshadri.Cohomology.alternatingTrunc_succ line 16
  3. lemma OAI.PiExponentSeshadri.Cohomology.alternating_rank_identity line 20
  4. lemma OAI.PiExponentSeshadri.Cohomology.finrank_middle_of_exact line 34
  5. def OAI.PiExponentSeshadri.Cohomology.extEuler line 47
  6. def OAI.PiExponentSeshadri.Cohomology.cohomologyMap₁ line 52
  7. def OAI.PiExponentSeshadri.Cohomology.cohomologyMap₂ line 55
  8. def OAI.PiExponentSeshadri.Cohomology.cohomologyBoundary line 58
  9. lemma OAI.PiExponentSeshadri.Cohomology.cohomology_exact₂ line 62
  10. lemma OAI.PiExponentSeshadri.Cohomology.cohomology_exact₃ line 72
  11. lemma OAI.PiExponentSeshadri.Cohomology.cohomology_exact₁ line 82
  12. theorem OAI.PiExponentSeshadri.Cohomology.extEuler_add_of_boundary_zero line 92
  13. theorem OAI.PiExponentSeshadri.Cohomology.extEuler_add line 148
  14. def OAI.PiExponentSeshadri.Geometry.sheafComplexLinear line 165
  15. def OAI.PiExponentSeshadri.Geometry.complexExtModule line 175
  16. lemma OAI.PiExponentSeshadri.Geometry.complexExtModule_eq line 179
  17. lemma OAI.PiExponentSeshadri.Geometry.eulerCharacteristic_eq_extEuler line 188
  18. theorem OAI.PiExponentSeshadri.Geometry.eulerCharacteristic_add line 199