OAI/NumberTheory/PiExponent/Cohomology/CartierEulerPair.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponent.NumericalAmpleness.regular_tensorSection_restriction_shortExact line 13
  2. def OAI.PiExponent.NumericalAmpleness.tensorSectionComplex line 30
  3. theorem OAI.PiExponent.NumericalAmpleness.tensorSectionComplex_shortExact line 36
  4. def OAI.PiExponent.NumericalAmpleness.CartierEulerPair.source line 43
  5. def OAI.PiExponent.NumericalAmpleness.CartierEulerPair.middle line 45
  6. def OAI.PiExponent.NumericalAmpleness.CartierEulerPair.middleIso line 48
  7. def OAI.PiExponent.NumericalAmpleness.CartierEulerPair.leftComplex line 54
  8. def OAI.PiExponent.NumericalAmpleness.CartierEulerPair.rightComplex line 58
  9. lemma OAI.PiExponent.NumericalAmpleness.CartierEulerPair.iso_middle_comm line 68
  10. def OAI.PiExponent.NumericalAmpleness.CartierEulerPair.rightComplexIso line 72
  11. theorem OAI.PiExponent.NumericalAmpleness.CartierEulerPair.left_shortExact line 82
  12. theorem OAI.PiExponent.NumericalAmpleness.CartierEulerPair.right_shortExact line 87
  13. abbrev OAI.PiExponent.NumericalAmpleness.CartierEulerPair.FiniteThrough line 93
  14. theorem OAI.PiExponent.NumericalAmpleness.CartierEulerPair.finiteThrough_closedPushforward line 97
  15. theorem OAI.PiExponent.NumericalAmpleness.CartierEulerPair.euler_difference line 109