OAI/NumberTheory/PiExponent/Cohomology/ProjectiveCoordinateAcyclicity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PiExponent.GeometrySupport.ProjectiveCoordinateAcyclicity.schemeUnit line 21
2. theorem OAI.PiExponent.GeometrySupport.ProjectiveCoordinateAcyclicity.coordinateTupleCoefficient_restrict line 25
3. def OAI.PiExponent.GeometrySupport.ProjectiveCoordinateAcyclicity.coordinateLaurentCechPresentation line 44
4. def OAI.PiExponent.GeometrySupport.ProjectiveCoordinateAcyclicity.coordinateLineBundle line 54
5. theorem OAI.PiExponent.GeometrySupport.ProjectiveCoordinateAcyclicity.coordinatePower_isQuasicoherent line 66
6. theorem OAI.PiExponent.GeometrySupport.ProjectiveCoordinateAcyclicity.coordinatePower_ext_succ_eq_zero line 72
7. theorem OAI.PiExponent.GeometrySupport.ProjectiveCoordinateAcyclicity.coordinatePower_ext_eq_zero line 81
8. theorem OAI.PiExponent.GeometrySupport.ProjectiveCoordinateAcyclicity.coordinateBundle_serre line 87