OAI/AlgebraicGeometry/Seshadri/Cohomology/AffineDenominators.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaximalSeshadri.AffineDenominators.basicOpen line 20
2. lemma OAI.MaximalSeshadri.AffineDenominators.basicOpen_mul line 22
3. lemma OAI.MaximalSeshadri.AffineDenominators.basicOpen_mul_le_left line 26
4. lemma OAI.MaximalSeshadri.AffineDenominators.basicOpen_mul_le_right line 30
5. lemma OAI.MaximalSeshadri.AffineDenominators.moduleIsSheaf line 34
6. structure OAI.MaximalSeshadri.AffineDenominators.Aux line 50
7. lemma OAI.MaximalSeshadri.AffineDenominators.Aux.of_le line 57
8. lemma OAI.MaximalSeshadri.AffineDenominators.Aux.of_eq_iSup_basicOpen line 73
9. lemma OAI.MaximalSeshadri.AffineDenominators.isLocalizing_iff_aux line 192
10. theorem OAI.MaximalSeshadri.AffineDenominators.aux_of_isCompact line 210
11. def OAI.MaximalSeshadri.AffineDenominators.res line 219
12. lemma OAI.MaximalSeshadri.AffineDenominators.res_comp line 222
13. lemma OAI.MaximalSeshadri.AffineDenominators.eq_zero_of_cover line 226
14. lemma OAI.MaximalSeshadri.AffineDenominators.power_in_ideal_of_generator_powers line 236
15. lemma OAI.MaximalSeshadri.AffineDenominators.kernel_is_torsion line 245
16. lemma OAI.MaximalSeshadri.AffineDenominators.torsion_free line 259
17. lemma OAI.MaximalSeshadri.AffineDenominators.torsion_in_kernel line 272
18. lemma OAI.MaximalSeshadri.AffineDenominators.cokernel_is_torsion line 281