OAI/GroupTheory/SimpleAmenable/Simplicial/ResolutionAugmentation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RestrictedNerve.verticalDiagonalFunctor line 13
2. def OAI.RestrictedNerve.verticalAugmentation line 23
3. lemma OAI.RestrictedNerve.constantMap_verticalAugmentation line 31
4. def OAI.RestrictedNerve.resolutionAugmentation line 41
5. lemma OAI.RestrictedNerve.resolutionAugmentation_homology line 44
6. instance OAI.RestrictedNerve.resolutionAugmentation_isIso line 59
7. lemma OAI.RestrictedNerve.verticalAugmentation_natural line 66
8. lemma OAI.RestrictedNerve.resolutionAugmentation_natural line 75
9. def OAI.RestrictedNerve.tripleResolutionAugmentation line 92
10. lemma OAI.RestrictedNerve.tripleResolutionAugmentation_homology line 97
11. instance OAI.RestrictedNerve.tripleResolutionAugmentation_isIso line 107
12. lemma OAI.RestrictedNerve.tripleResolutionAugmentation_outer_natural line 111
13. lemma OAI.RestrictedNerve.tripleResolutionAugmentation_middle_natural line 129