OAI/Algebra/AuslanderReiten/Duality/LinearHomologyDuality.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.LinearHomology.cycleMap line 15
2. def OAI.ArExplicit.LinearHomology.boundaries line 18
3. abbrev OAI.ArExplicit.LinearHomology.Homology line 21
4. theorem OAI.ArExplicit.LinearHomology.dual_comp line 24
5. def OAI.ArExplicit.LinearHomology.dualCyclesToDualHomology line 30
6. theorem OAI.ArExplicit.LinearHomology.dualCyclesToDualHomology_mk line 47
7. theorem OAI.ArExplicit.LinearHomology.dualCyclesToDualHomology_surjective line 51
8. theorem OAI.ArExplicit.LinearHomology.dualCyclesToDualHomology_kernel line 70
9. def OAI.ArExplicit.LinearHomology.dualHomologyEquiv line 91
10. theorem OAI.ArExplicit.LinearHomology.dualHomologyEquiv_symm_mk line 99