OAI/NumberTheory/PiExponent/Approximation/ClosedPushforwardCoherent.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PiExponentSeshadri.ClosedPushforward.sections_empty line 14
2. lemma OAI.PiExponentSeshadri.ClosedPushforward.map_epi line 19
3. instance OAI.PiExponentSeshadri.ClosedPushforward.preservesEpis line 61
4. instance OAI.PiExponentSeshadri.ClosedPushforward.preservesHomology line 65
5. instance OAI.PiExponentSeshadri.ClosedPushforward.preservesFiniteColimits line 69
6. theorem OAI.PiExponentSeshadri.ClosedPushforward.presentation_transport line 76
7. instance OAI.PiExponentSeshadri.ClosedPushforward.pushforward_isFinitePresentation line 83