OAI/NumberTheory/PiExponent/Approximation/ClosedPushforwardLinear.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PiExponent.ClosedImmersionSerreTransfer.baseScalars_comp_actual line 16
2. lemma OAI.PiExponent.ClosedImmersionSerreTransfer.scalar_naturality line 22
3. theorem OAI.PiExponent.ClosedImmersionSerreTransfer.complexLinearPushforward line 29
4. lemma OAI.PiExponent.ClosedImmersionSerreTransfer.cohomologyMap_comp line 45
5. def OAI.PiExponent.ClosedImmersionSerreTransfer.typedCohomologyMap line 52
6. lemma OAI.PiExponent.ClosedImmersionSerreTransfer.typedCohomologyMap_comp line 56
7. lemma OAI.PiExponent.ClosedImmersionSerreTransfer.typedCohomologyMap_bijective line 63
8. def OAI.PiExponent.ClosedImmersionSerreTransfer.cohomologyLinearMap line 67
9. lemma OAI.PiExponent.ClosedImmersionSerreTransfer.cohomologyLinearMap_eq line 88
10. def OAI.PiExponent.ClosedImmersionSerreTransfer.cohomologyLinearEquiv line 91
11. theorem OAI.PiExponent.ClosedImmersionSerreTransfer.finiteDimensional_of_pushforward line 98
12. lemma OAI.PiExponent.ClosedImmersionSerreTransfer.cohomologyDimension_pushforward line 110
13. theorem OAI.PiExponent.ClosedImmersionSerreTransfer.euler_pushforward line 118