OAI/GroupTheory/SimpleAmenable/Homology/GroupoidComponentHomology.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GroupoidComponentHomology.inclusion line 13
2. lemma OAI.GroupoidComponentHomology.inclusion_obj line 15
3. lemma OAI.GroupoidComponentHomology.inclusion_map line 16
4. instance OAI.GroupoidComponentHomology.inclusion_faithful line 18
5. instance OAI.GroupoidComponentHomology.inclusion_full line 20
6. def OAI.GroupoidComponentHomology.fiberInclusion line 22
7. instance OAI.GroupoidComponentHomology.fiberInclusion_faithful line 24
8. instance OAI.GroupoidComponentHomology.fiberInclusion_full line 26
9. instance OAI.GroupoidComponentHomology.fiberInclusion_essSurj line 28
10. instance OAI.GroupoidComponentHomology.fiberInclusion_isEquivalence line 30
11. def OAI.GroupoidComponentHomology.fiberIsoHomology line 32
12. instance OAI.TranslationFiltered.regular_filtered line 46
13. abbrev OAI.TranslationFiltered.Q line 55
14. instance OAI.TranslationFiltered.completed_action line 56
15. lemma OAI.TranslationFiltered.common_target line 58
16. instance OAI.TranslationFiltered.completed_filtered line 66