OAI/NumberTheory/PiExponent/Cohomology/GradedPolynomialCech.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.GradedPolynomialCech.intersectionToPiece line 12
2. def OAI.PiExponent.GradedPolynomialCech.intersectionToLaurent line 19
3. theorem OAI.PiExponent.GradedPolynomialCech.intersectionToLaurent_apply line 24
4. def OAI.PiExponent.GradedPolynomialCech.cochainToLaurent line 29
5. theorem OAI.PiExponent.GradedPolynomialCech.cochainToLaurent_apply line 36
6. theorem OAI.PiExponent.GradedPolynomialCech.cochainToLaurent_injective line 41
7. theorem OAI.PiExponent.GradedPolynomialCech.cochainToLaurent_regular line 47
8. theorem OAI.PiExponent.GradedPolynomialCech.cochainToLaurent_surjective_regular line 55
9. theorem OAI.PiExponent.GradedPolynomialCech.cochainToLaurent_differential line 68
10. theorem OAI.PiExponent.GradedPolynomialCech.nonnegative_polynomial_cech_exact line 85
11. theorem OAI.PiExponent.GradedPolynomialCech.nonnegative_polynomial_augmentation_recovery line 99