OAI/CategoryTheory/ThickClosure/PeriodicSplitting.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HahnWilson.PeriodicSplitting.homologyDiagonal line 16
  2. abbrev OAI.HahnWilson.PeriodicSplitting.resolutionTerm line 24
  3. def OAI.HahnWilson.PeriodicSplitting.resolutionD line 26
  4. lemma OAI.HahnWilson.PeriodicSplitting.resolutionD_sq line 30
  5. abbrev OAI.HahnWilson.PeriodicSplitting.resolutionComplex line 36
  6. lemma OAI.HahnWilson.PeriodicSplitting.resolutionComplex_d line 39
  7. lemma OAI.HahnWilson.PeriodicSplitting.resolutionComplex_d_prev line 43
  8. def OAI.HahnWilson.PeriodicSplitting.resolutionMap line 65
  9. lemma OAI.HahnWilson.PeriodicSplitting.resolutionMap_inl line 72
  10. def OAI.HahnWilson.PeriodicSplitting.resolutionLeftHomologyData line 85
  11. lemma OAI.HahnWilson.PeriodicSplitting.resolutionLeftHomologyData_i line 119
  12. lemma OAI.HahnWilson.PeriodicSplitting.resolutionLeftHomologyData_π line 121
  13. def OAI.HahnWilson.PeriodicSplitting.leftHomologyMapOfSquares line 126
  14. def OAI.HahnWilson.PeriodicSplitting.chosenCycleLift line 149
  15. lemma OAI.HahnWilson.PeriodicSplitting.chosenCycleLift_π line 153
  16. def OAI.HahnWilson.PeriodicSplitting.chosenBoundaryLift line 157
  17. lemma OAI.HahnWilson.PeriodicSplitting.chosenBoundaryLift_f' line 165
  18. def OAI.HahnWilson.PeriodicSplitting.resolutionCycleMap line 172
  19. def OAI.HahnWilson.PeriodicSplitting.resolutionBoundaryMap line 175
  20. lemma OAI.HahnWilson.PeriodicSplitting.resolutionCycleMap_d line 179
  21. lemma OAI.HahnWilson.PeriodicSplitting.resolutionBoundaryMap_d line 191
  22. def OAI.HahnWilson.PeriodicSplitting.comparisonMap line 214
  23. lemma OAI.HahnWilson.PeriodicSplitting.comparisonMap_quasiIso line 231
  24. def OAI.HahnWilson.PeriodicSplitting.cyclicHomologyData line 256
  25. abbrev OAI.HahnWilson.PeriodicSplitting.diagonalComplex line 262
  26. lemma OAI.HahnWilson.PeriodicSplitting.diagonalComplex_d line 265
  27. def OAI.HahnWilson.PeriodicSplitting.diagonalMap line 274
  28. lemma OAI.HahnWilson.PeriodicSplitting.diagonalMap_quasiIso line 283
  29. theorem OAI.HahnWilson.PeriodicSplitting.exists_categorical_resolution line 305
  30. theorem OAI.HahnWilson.PeriodicSplitting.periodic_homology_splitting line 320