OAI/NumberTheory/PiExponent/Cohomology/ProjectiveLineLaurent.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.ProjectiveLine.zeroPolynomialMap line 13
  2. def OAI.PiExponent.ProjectiveLine.infinityPolynomialMap line 16
  3. theorem OAI.PiExponent.ProjectiveLine.zeroPolynomialMap_C line 19
  4. theorem OAI.PiExponent.ProjectiveLine.zeroPolynomialMap_X line 23
  5. theorem OAI.PiExponent.ProjectiveLine.infinityPolynomialMap_C line 27
  6. theorem OAI.PiExponent.ProjectiveLine.infinityPolynomialMap_X line 31
  7. theorem OAI.PiExponent.ProjectiveLine.infinityPolynomialMap_eq_invert_comp line 35
  8. def OAI.PiExponent.ProjectiveLine.laurentInversion line 43
  9. instance OAI.PiExponent.ProjectiveLine.laurentInversion_isIso line 48
  10. def OAI.PiExponent.ProjectiveLine.zeroChartOverlap line 54
  11. def OAI.PiExponent.ProjectiveLine.infinityChartOverlap line 58
  12. theorem OAI.PiExponent.ProjectiveLine.infinityChartOverlap_eq line 62
  13. instance OAI.PiExponent.ProjectiveLine.zeroChartOverlap_isOpenImmersion line 67
  14. instance OAI.PiExponent.ProjectiveLine.infinityChartOverlap_isOpenImmersion line 70
  15. theorem OAI.PiExponent.ProjectiveLine.zeroChartOverlap_opensRange line 74
  16. theorem OAI.PiExponent.ProjectiveLine.infinityChartOverlap_opensRange line 79