OAI/NumberTheory/PiExponent/Cohomology/CurveFinitePushforwardCohomology.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.CurveFinitePushforwardCohomology.sectionsEquiv line 12
2. lemma OAI.PiExponent.CurveFinitePushforwardCohomology.sectionsEquiv_image line 28
3. def OAI.PiExponent.CurveFinitePushforwardCohomology.cohomologyOneEquiv line 53
4. def OAI.PiExponent.CurveFinitePushforwardCohomology.zeroSections line 76
5. def OAI.PiExponent.CurveFinitePushforwardCohomology.cohomologyZeroEquiv line 96
6. def OAI.PiExponent.CurveFinitePushforwardCohomology.cohomologyLowEquiv line 107
7. theorem OAI.PiExponent.CurveFinitePushforwardCohomology.finiteDimensional_of_pushforward line 123
8. theorem OAI.PiExponent.CurveFinitePushforwardCohomology.finiteDimensional_pushforward line 139
9. lemma OAI.PiExponent.CurveFinitePushforwardCohomology.baseScalars_comp line 155
10. theorem OAI.PiExponent.CurveFinitePushforwardCohomology.cohomologyDimension_pushforward line 161
11. theorem OAI.PiExponent.CurveFinitePushforwardCohomology.euler_one_pushforward line 175