OAI/Algebra/Finitistic/Selected/SelectedTargetHomology.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LittleFinitistic.SelectedTargetHomology.C line 15
  2. abbrev OAI.LittleFinitistic.SelectedTargetHomology.I line 16
  3. abbrev OAI.LittleFinitistic.SelectedTargetHomology.cohomology line 17
  4. instance OAI.LittleFinitistic.SelectedTargetHomology.(instance at line 18) line 18
  5. instance OAI.LittleFinitistic.SelectedTargetHomology.(instance at line 19) line 19
  6. def OAI.LittleFinitistic.SelectedTargetHomology.stalkIso line 22
  7. def OAI.LittleFinitistic.SelectedTargetHomology.shiftedIso line 24
  8. def OAI.LittleFinitistic.SelectedTargetHomology.stalkHomologyIso line 30
  9. def OAI.LittleFinitistic.SelectedTargetHomology.shiftedHomologyIso line 33
  10. lemma OAI.LittleFinitistic.SelectedTargetHomology.single_zero line 37
  11. lemma OAI.LittleFinitistic.SelectedTargetHomology.stalk_zero line 43
  12. lemma OAI.LittleFinitistic.SelectedTargetHomology.shifted_zero line 47
  13. def OAI.LittleFinitistic.SelectedTargetHomology.targetH0 line 52
  14. def OAI.LittleFinitistic.SelectedTargetHomology.targetHm3 line 56
  15. lemma OAI.LittleFinitistic.SelectedTargetHomology.target_zero line 60
  16. lemma OAI.LittleFinitistic.SelectedTargetHomology.stalkHomologyIso_hom line 65
  17. lemma OAI.LittleFinitistic.SelectedTargetHomology.stalk_action line 71
  18. lemma OAI.LittleFinitistic.SelectedTargetHomology.shifted_action line 84
  19. lemma OAI.LittleFinitistic.SelectedTargetHomology.targetH0_hom line 122
  20. lemma OAI.LittleFinitistic.SelectedTargetHomology.targetHm3_hom line 126
  21. lemma OAI.LittleFinitistic.SelectedTargetHomology.targetH0_action line 131
  22. lemma OAI.LittleFinitistic.SelectedTargetHomology.targetHm3_action line 136