OAI/NumberTheory/PiExponent/Cohomology/FiniteSupportCohomology.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PiExponentSeshadri.FiniteSupport.discrete_restriction_surjective line 12
2. lemma OAI.PiExponentSeshadri.FiniteSupport.discrete_flasque line 53
3. lemma OAI.PiExponentSeshadri.FiniteSupport.proper_finite_discrete line 60
4. lemma OAI.PiExponentSeshadri.FiniteSupport.pushforward_flasque line 71
5. theorem OAI.PiExponentSeshadri.FiniteSupport.finite_pushforward_ext_zero line 80
6. def OAI.PiExponentSeshadri.FiniteSupport.pushforwardUnitSections line 87
7. theorem OAI.PiExponentSeshadri.FiniteSupport.finite_pushforward_euler line 102
8. theorem OAI.PiExponentSeshadri.FiniteSupport.finite_pushforward_finiteDimensional line 128