OAI/NumberTheory/PiExponent/Approximation/ClosedAnnihilatedDescent.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponentSeshadri.ClosedAnnihilatedDescent.specPushforwardSectionsIso line 10
2. def OAI.PiExponentSeshadri.ClosedAnnihilatedDescent.specPushforwardTildeIso line 17
3. def OAI.PiExponentSeshadri.ClosedAnnihilatedDescent.quotientModule line 26
4. def OAI.PiExponentSeshadri.ClosedAnnihilatedDescent.quotientModuleRestrictIso line 33
5. def OAI.PiExponentSeshadri.ClosedAnnihilatedDescent.affineDescent line 38
6. instance OAI.PiExponentSeshadri.ClosedAnnihilatedDescent.affineDescent_isQuasicoherent line 43
7. def OAI.PiExponentSeshadri.ClosedAnnihilatedDescent.affineDescentPushforwardIso line 49
8. instance OAI.PiExponentSeshadri.ClosedAnnihilatedDescent.quotientModule_finite line 58
9. lemma OAI.PiExponentSeshadri.ClosedAnnihilatedDescent.affineDescent_finitePresentation line 68
10. theorem OAI.PiExponentSeshadri.ClosedAnnihilatedDescent.exists_affine_coherent_descent line 74