OAI/NumberTheory/PiExponent/Approximation/ClosedImmersionSerreTransfer.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PiExponent.ClosedImmersionSerreTransfer.schemeUnit line 13
2. def OAI.PiExponent.ClosedImmersionSerreTransfer.structureMap line 18
3. lemma OAI.PiExponent.ClosedImmersionSerreTransfer.globalHom_push line 22
4. lemma OAI.PiExponent.ClosedImmersionSerreTransfer.globalHom_push_bijective line 30
5. instance OAI.PiExponent.ClosedImmersionSerreTransfer.pushforward_flasque line 45
6. def OAI.PiExponent.ClosedImmersionSerreTransfer.cohomologyMap line 57
7. theorem OAI.PiExponent.ClosedImmersionSerreTransfer.cohomologyMap_bijective line 64
8. def OAI.PiExponent.ClosedImmersionSerreTransfer.cohomologyEquiv line 76
9. theorem OAI.PiExponent.ClosedImmersionSerreTransfer.ext_zero_iff line 82
10. def OAI.PiExponent.ClosedImmersionSerreTransfer.closedCohomologyEquiv line 95