OAI/CategoryTheory/ThickClosure/PeriodicHom.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HahnWilson.PeriodicHom.homotopyQuotient line 16
2. lemma OAI.HahnWilson.PeriodicHom.diagonal_map_cycle line 22
3. def OAI.HahnWilson.PeriodicHom.cycleClass line 26
4. lemma OAI.HahnWilson.PeriodicHom.source_cycle_naturality line 30
5. lemma OAI.HahnWilson.PeriodicHom.cycleClass_eq line 38
6. lemma OAI.HahnWilson.PeriodicHom.null_homotopy_of_cycleClass_zero line 45
7. theorem OAI.HahnWilson.PeriodicHom.homotopy_zero_iff line 75
8. lemma OAI.HahnWilson.PeriodicHom.cycleClass_comp line 87
9. lemma OAI.HahnWilson.PeriodicHom.cycleClass_sub line 92
10. lemma OAI.HahnWilson.PeriodicHom.quotient_eq_of_cycleClass_eq line 96
11. def OAI.HahnWilson.PeriodicHom.mapOfClasses line 105
12. lemma OAI.HahnWilson.PeriodicHom.cycleClass_mapOfClasses line 112
13. theorem OAI.HahnWilson.PeriodicHom.free_hom_quasiIso_bijective line 124