OAI/Algebra/AuslanderReiten/Duality/RightDualHomology.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.RightDualHomology.cycleMap line 16
2. def OAI.ArExplicit.RightDualHomology.boundaries line 19
3. abbrev OAI.ArExplicit.RightDualHomology.Homology line 21
4. def OAI.ArExplicit.RightDualHomology.cyclesToDualHomology line 23
5. theorem OAI.ArExplicit.RightDualHomology.cyclesToDualHomology_mk line 43
6. theorem OAI.ArExplicit.RightDualHomology.cyclesToDualHomology_surjective line 49
7. def OAI.ArExplicit.RightDualHomology.dualCycleMap line 72
8. def OAI.ArExplicit.RightDualHomology.dualBoundaries line 81
9. abbrev OAI.ArExplicit.RightDualHomology.DualHomology line 84
10. theorem OAI.ArExplicit.RightDualHomology.cyclesToDualHomology_kernel line 86
11. def OAI.ArExplicit.RightDualHomology.dualHomologyEquiv line 107