OAI/NumberTheory/PiExponent/Geometry/LineBundleGluingSections.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponentSeshadri.LineBundleGluing.globalSection line 13
2. lemma OAI.PiExponentSeshadri.LineBundleGluing.sheafification_unit_counit_map line 18
3. lemma OAI.PiExponentSeshadri.LineBundleGluing.module_comp_val line 34
4. lemma OAI.PiExponentSeshadri.LineBundleGluing.openFrame_unit line 37
5. lemma OAI.PiExponentSeshadri.LineBundleGluing.openFrame_unit_apply line 60
6. lemma OAI.PiExponentSeshadri.LineBundleGluing.globalSection_app_one line 69
7. theorem OAI.PiExponentSeshadri.LineBundleGluing.globalSection_coefficient line 84