OAI/AlgebraicGeometry/Seshadri/Cohomology/TripleComplex.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MaximalSeshadri.ModuleMayerVietoris.tripleVertices line 17
2. abbrev OAI.MaximalSeshadri.ModuleMayerVietoris.triplePairs line 18
3. def OAI.MaximalSeshadri.ModuleMayerVietoris.tripleD line 19
4. def OAI.MaximalSeshadri.ModuleMayerVietoris.tripleG line 28
5. lemma OAI.MaximalSeshadri.ModuleMayerVietoris.tripleDG line 33
6. instance OAI.MaximalSeshadri.ModuleMayerVietoris.tripleG_epi line 40
7. def OAI.MaximalSeshadri.ModuleMayerVietoris.tripleG_isCokernel line 54
8. abbrev OAI.MaximalSeshadri.ModuleMayerVietoris.tripleRelations line 75
9. def OAI.MaximalSeshadri.ModuleMayerVietoris.tripleToRelations line 76
10. instance OAI.MaximalSeshadri.ModuleMayerVietoris.tripleToRelations_epi line 78
11. lemma OAI.MaximalSeshadri.ModuleMayerVietoris.tripleToRelations_cycle line 82
12. abbrev OAI.MaximalSeshadri.ModuleMayerVietoris.tripleKernelComplex line 94
13. lemma OAI.MaximalSeshadri.ModuleMayerVietoris.tripleKernelComplex_shortExact line 96