OAI/AlgebraicGeometry/Seshadri/Divisors/BaseSections.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaximalSeshadri.Geometry.BaseSections.Sections line 17
2. instance OAI.MaximalSeshadri.Geometry.BaseSections.(instance at line 18) line 18
3. instance OAI.MaximalSeshadri.Geometry.BaseSections.globalModule line 20
4. instance OAI.MaximalSeshadri.Geometry.BaseSections.baseModule line 22
5. def OAI.MaximalSeshadri.Geometry.BaseSections.res line 25
6. def OAI.MaximalSeshadri.Geometry.BaseSections.congr line 31
7. lemma OAI.MaximalSeshadri.Geometry.BaseSections.congr_res line 36
8. lemma OAI.MaximalSeshadri.Geometry.BaseSections.congr_naturality line 41
9. def OAI.MaximalSeshadri.Geometry.BaseSections.restrictEquiv line 48
10. lemma OAI.MaximalSeshadri.Geometry.BaseSections.restrictEquiv_res line 59
11. lemma OAI.MaximalSeshadri.Geometry.BaseSections.chart_image_top line 65
12. lemma OAI.MaximalSeshadri.Geometry.BaseSections.chart_image_preimage line 68
13. def OAI.MaximalSeshadri.Geometry.BaseSections.chartTop line 71
14. def OAI.MaximalSeshadri.Geometry.BaseSections.chartOverlap line 75
15. lemma OAI.MaximalSeshadri.Geometry.BaseSections.chartRestriction line 81