OAI/CategoryTheory/ThickClosure/PeriodicDerived.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HahnWilson.PeriodicDerived.PeriodicComplex line 17
2. def OAI.HahnWilson.PeriodicDerived.GradedFiniteFree line 19
3. inductive OAI.HahnWilson.PeriodicDerived.FiniteCell line 22
4. abbrev OAI.HahnWilson.PeriodicDerived._root_.OAI.HahnWilson.PeriodicDerived line 30
5. abbrev OAI.HahnWilson.PeriodicDerived.Q line 33
6. abbrev OAI.HahnWilson.PeriodicDerived.homology line 36
7. def OAI.HahnWilson.PeriodicDerived.IsPerfect line 39
8. lemma OAI.HahnWilson.PeriodicDerived.finiteCell_terms line 50
9. lemma OAI.HahnWilson.PeriodicDerived.down_prev line 72
10. lemma OAI.HahnWilson.PeriodicDerived.cofiber_XIso_hom_snd line 75
11. def OAI.HahnWilson.PeriodicDerived.diagonalFamilyMap line 85
12. def OAI.HahnWilson.PeriodicDerived.resolutionConeIso line 92
13. lemma OAI.HahnWilson.PeriodicDerived.resolution_finiteCell line 129
14. lemma OAI.HahnWilson.PeriodicDerived.finite_homology_of_finite_terms line 143
15. theorem OAI.HahnWilson.PeriodicDerived.perfect_homology_finite line 156
16. lemma OAI.HahnWilson.PeriodicDerived.perfect_of_iso line 171
17. lemma OAI.HahnWilson.PeriodicDerived.diagonal_perfect line 177
18. lemma OAI.HahnWilson.PeriodicDerived.derived_homology_splitting line 195
19. theorem OAI.HahnWilson.PeriodicDerived.perfect_splitting line 207