OAI/NumberTheory/PiExponent/Cohomology/NakaiCohomology.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.NumericalAmpleness.cohomologyMap line 11
  2. theorem OAI.PiExponent.NumericalAmpleness.globalSections_surjective_of_h1_stationary line 22
  3. theorem OAI.PiExponent.NumericalAmpleness.eventually_constant_of_antitone_nat line 54
  4. theorem OAI.PiExponent.NumericalAmpleness.eventual_globalSections_surjective line 63
  5. theorem OAI.PiExponent.NumericalAmpleness.cohomologyMap_bijective_of_quotient_vanishing line 98
  6. theorem OAI.PiExponent.NumericalAmpleness.cohomologyDimension_eq_of_quotient_vanishing line 114
  7. theorem OAI.PiExponent.NumericalAmpleness.eventual_cohomologyDimension_constant_of_two_sequences line 124