OAI/CategoryTheory/ThickClosure/ActionDerived.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HahnWilson.LaurentDg.actualEquivalence line 15
2. def OAI.HahnWilson.LaurentDg.ActionModule.forget line 21
3. def OAI.HahnWilson.LaurentDg.ActionModule.quasiIso line 27
4. def OAI.HahnWilson.LaurentDg.ActionModule.homology line 29
5. abbrev OAI.HahnWilson.LaurentDg.ActionModule.localization line 33
6. def OAI.HahnWilson.LaurentDg.actionForgetIso line 36
7. def OAI.HahnWilson.LaurentDg.inverseForgetIso line 40
8. lemma OAI.HahnWilson.LaurentDg.inverse_quasiIso_iff line 47
9. theorem OAI.HahnWilson.LaurentDg.ActionModule.localization_isLocalization line 62
10. def OAI.HahnWilson.LaurentDg.ActionModule.localizationHomologyIso line 86