OAI/AlgebraicGeometry/Seshadri/Cohomology/Injectives.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaximalSeshadri.AdicInjective.adicTorsion line 16
2. lemma OAI.MaximalSeshadri.AdicInjective.torsion_mono line 19
3. lemma OAI.MaximalSeshadri.AdicInjective.mem_adicTorsion line 22
4. lemma OAI.MaximalSeshadri.AdicInjective.fg_uniform_exponent line 27
5. lemma OAI.MaximalSeshadri.AdicInjective.exists_power_inf_le line 37
6. theorem OAI.MaximalSeshadri.AdicInjective.adicTorsion_injective line 46
7. lemma OAI.MaximalSeshadri.InjectiveRange.injective_of_retract line 107
8. lemma OAI.MaximalSeshadri.InjectiveRange.range_injective line 119
9. lemma OAI.MaximalSeshadri.InjectiveRange.surjective_of_torsion_cokernel line 139