OAI/Algebra/AuslanderReiten/Homology/VectorCochainSplitting.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.ArExplicit.VectorCochain.vectorSpaceInjective line 17
  2. abbrev OAI.ArExplicit.VectorCochain.zeroDifferential line 26
  3. def OAI.ArExplicit.VectorCochain.zeroHomologyIso line 32
  4. theorem OAI.ArExplicit.VectorCochain.zeroHomologyIso_π line 37
  5. abbrev OAI.ArExplicit.VectorCochain.gradedHomology line 47
  6. def OAI.ArExplicit.VectorCochain.cycleSection line 50
  7. theorem OAI.ArExplicit.VectorCochain.cycleSection_π line 53
  8. def OAI.ArExplicit.VectorCochain.representatives line 57
  9. theorem OAI.ArExplicit.VectorCochain.cyclesMap_representatives line 61
  10. theorem OAI.ArExplicit.VectorCochain.homologyMap_representatives line 67
  11. instance OAI.ArExplicit.VectorCochain.representatives_quasiIso line 73
  12. def OAI.ArExplicit.VectorCochain.splitting line 79
  13. theorem OAI.ArExplicit.VectorCochain.splitting_hom line 83