OAI/CategoryTheory/ThickClosure/UnrollDerived.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HahnWilson.Unroll.PD line 19
2. abbrev OAI.HahnWilson.Unroll.q line 20
3. lemma OAI.HahnWilson.Unroll.inverts_quasiIso line 23
4. def OAI.HahnWilson.Unroll.derivedFunctor line 31
5. def OAI.HahnWilson.Unroll.derivedFactors line 34
6. def OAI.HahnWilson.Unroll.derivedHomologyIso line 37
7. theorem OAI.HahnWilson.Unroll.derived_homology_iso line 60
8. instance OAI.HahnWilson.Unroll.(instance at line 66) line 66
9. lemma OAI.HahnWilson.Unroll.down_rel line 79
10. lemma OAI.HahnWilson.Unroll.up_rel line 83
11. def OAI.HahnWilson.Unroll.coneXIso line 85
12. lemma OAI.HahnWilson.Unroll.obj_d line 91
13. lemma OAI.HahnWilson.Unroll.map_f line 95
14. lemma OAI.HahnWilson.Unroll.coneXIso_comm line 98
15. def OAI.HahnWilson.Unroll.coneIso line 139
16. lemma OAI.HahnWilson.Unroll.coneIso_inr line 147
17. theorem OAI.HahnWilson.Unroll.cone_iso line 160