OAI/NumberTheory/PiExponent/Cohomology/ReesSheafCechBase.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PiExponent.ReesSheafCechBase.chartMap line 28
  2. abbrev OAI.PiExponent.ReesSheafCechBase.schemeFreeOpen line 36
  3. abbrev OAI.PiExponent.ReesSheafCechBase.exceptionalPower line 39
  4. def OAI.PiExponent.ReesSheafCechBase.opens line 41
  5. theorem OAI.PiExponent.ReesSheafCechBase.tuple_mem line 44
  6. theorem OAI.PiExponent.ReesSheafCechBase.tuple_nonempty line 48
  7. def OAI.PiExponent.ReesSheafCechBase.freeOpenSectionsEquiv line 51
  8. def OAI.PiExponent.ReesSheafCechBase.freeOpenHomCongr line 55
  9. theorem OAI.PiExponent.ReesSheafCechBase.freeOpenHomCongr_restrict line 69
  10. theorem OAI.PiExponent.ReesSheafCechBase.tupleOpen_eq line 79
  11. def OAI.PiExponent.ReesSheafCechBase.genericChartHomEquiv line 93
  12. theorem OAI.PiExponent.ReesSheafCechBase.chartFrameTyped_nonempty line 110
  13. def OAI.PiExponent.ReesSheafCechBase.chartFrameTyped line 119
  14. def OAI.PiExponent.ReesSheafCechBase.chartHomEquiv line 123
  15. theorem OAI.PiExponent.ReesSheafCechBase.chartHomEquiv_pieceEquiv line 130
  16. def OAI.PiExponent.ReesSheafCechBase.tupleHomEquiv line 144
  17. def OAI.PiExponent.ReesSheafCechBase.cochainEquiv line 159
  18. theorem OAI.PiExponent.ReesSheafCechBase.tuple_isAffine line 173
  19. theorem OAI.PiExponent.ReesSheafCechBase.iSup_opens line 180