OAI/Algebra/AuslanderReiten/Homology/VectorCochainKunnethCycles.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ArExplicit.VectorCochain.gradedCycles line 12
2. def OAI.ArExplicit.VectorCochain.cyclesInclusion line 14
3. def OAI.ArExplicit.VectorCochain.cyclesQuotient line 18
4. theorem OAI.ArExplicit.VectorCochain.cyclesMap_cyclesInclusion line 22
5. theorem OAI.ArExplicit.VectorCochain.homologyMap_cyclesInclusion line 27
6. theorem OAI.ArExplicit.VectorCochain.cyclesInclusion_comp_splitting_inv line 33
7. def OAI.ArExplicit.VectorCochain.cyclesInclusionHomotopy line 47
8. def OAI.ArExplicit.VectorCochain.tensorCyclesInclusionHomotopy line 59
9. theorem OAI.ArExplicit.VectorCochain.tensorRepresentatives_kunneth line 69
10. theorem OAI.ArExplicit.VectorCochain.tensorCycles_kunneth line 77