OAI/NumberTheory/PiExponent/Cohomology/PencilCohomologyCharts.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponentSeshadri.Geometry.BaseSections.Sections line 13
  2. instance OAI.PiExponentSeshadri.Geometry.BaseSections.(instance at line 14) line 14
  3. instance OAI.PiExponentSeshadri.Geometry.BaseSections.globalModule line 16
  4. instance OAI.PiExponentSeshadri.Geometry.BaseSections.baseModule line 18
  5. def OAI.PiExponentSeshadri.Geometry.BaseSections.res line 21
  6. def OAI.PiExponentSeshadri.Geometry.BaseSections.congr line 27
  7. lemma OAI.PiExponentSeshadri.Geometry.BaseSections.congr_res line 32
  8. lemma OAI.PiExponentSeshadri.Geometry.BaseSections.congr_naturality line 37
  9. def OAI.PiExponentSeshadri.Geometry.BaseSections.restrictEquiv line 44
  10. lemma OAI.PiExponentSeshadri.Geometry.BaseSections.restrictEquiv_res line 55
  11. lemma OAI.PiExponentSeshadri.Geometry.BaseSections.chart_image_top line 61
  12. lemma OAI.PiExponentSeshadri.Geometry.BaseSections.chart_image_preimage line 64
  13. def OAI.PiExponentSeshadri.Geometry.BaseSections.chartTop line 67
  14. def OAI.PiExponentSeshadri.Geometry.BaseSections.chartOverlap line 71
  15. lemma OAI.PiExponentSeshadri.Geometry.BaseSections.chartRestriction line 77
  16. def OAI.PiExponentSeshadri.Geometry.BaseSections.polynomialModule line 94
  17. theorem OAI.PiExponentSeshadri.Geometry.BaseSections.polynomialTower line 98
  18. def OAI.PiExponentSeshadri.Geometry.BaseSections.polynomialRes line 108
  19. theorem OAI.PiExponentSeshadri.Geometry.BaseSections.polynomial_localization line 119
  20. theorem OAI.PiExponentSeshadri.Geometry.BaseSections.polynomial_finite line 143
  21. def OAI.PiExponentSeshadri.Geometry.chartModuleEquiv line 162
  22. def OAI.PiExponentSeshadri.Geometry.chartModuleMap line 174
  23. theorem OAI.PiExponentSeshadri.Geometry.chartModuleMap_localize line 182
  24. def OAI.PiExponentSeshadri.Geometry.BaseSections.chartMap line 197
  25. lemma OAI.PiExponentSeshadri.Geometry.BaseSections.chartMap_smul line 211
  26. lemma OAI.PiExponentSeshadri.Geometry.BaseSections.eval_transport line 227
  27. def OAI.PiExponentSeshadri.Geometry.BaseSections.chartPolynomialMap line 239
  28. theorem OAI.PiExponentSeshadri.Geometry.BaseSections.chartPolynomialMap_localize line 255