OAI/CategoryTheory/ThickClosure/LaurentModules.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.HahnWilson.LaurentDg.Module line 14
  2. structure OAI.HahnWilson.LaurentDg.Module.Hom line 29
  3. instance OAI.HahnWilson.LaurentDg.Module.(instance at line 35) line 35
  4. lemma OAI.HahnWilson.LaurentDg.Module.id_f line 45
  5. lemma OAI.HahnWilson.LaurentDg.Module.comp_f line 46
  6. lemma OAI.HahnWilson.LaurentDg.Module.power_hom_refl line 48
  7. lemma OAI.HahnWilson.LaurentDg.Module.power_hom_trans line 50
  8. def OAI.HahnWilson.LaurentDg.rep line 58
  9. lemma OAI.HahnWilson.LaurentDg.rep_cast line 59
  10. lemma OAI.HahnWilson.LaurentDg.rep_next line 62
  11. def OAI.HahnWilson.LaurentDg.reduceD line 65
  12. lemma OAI.HahnWilson.LaurentDg.reduceD_sq line 69
  13. abbrev OAI.HahnWilson.LaurentDg.reduceObj line 76
  14. lemma OAI.HahnWilson.LaurentDg.reduceObj_d line 79
  15. lemma OAI.HahnWilson.LaurentDg.reduceObj_d_eq line 83
  16. def OAI.HahnWilson.LaurentDg.reduce line 89
  17. def OAI.HahnWilson.LaurentDg.inflateObj line 100
  18. def OAI.HahnWilson.LaurentDg.inflate line 112
  19. lemma OAI.HahnWilson.LaurentDg.Module.power_hom_eqToHom line 121
  20. def OAI.HahnWilson.LaurentDg.Module.isoMk line 125
  21. def OAI.HahnWilson.LaurentDg.counitApp line 143
  22. def OAI.HahnWilson.LaurentDg.counit line 154
  23. def OAI.HahnWilson.LaurentDg.unitApp line 161
  24. def OAI.HahnWilson.LaurentDg.unit line 176
  25. def OAI.HahnWilson.LaurentDg.equivalence line 183
  26. def OAI.HahnWilson.LaurentDg.forgetObj line 186
  27. def OAI.HahnWilson.LaurentDg.forget line 189
  28. abbrev OAI.HahnWilson.LaurentDg.unroll line 195
  29. def OAI.HahnWilson.LaurentDg.unrollScIso line 198
  30. def OAI.HahnWilson.LaurentDg.unrollHomologyIso line 210
  31. def OAI.HahnWilson.LaurentDg.homology line 221
  32. def OAI.HahnWilson.LaurentDg.homologyIso line 224
  33. def OAI.HahnWilson.LaurentDg.quasiIso line 231
  34. lemma OAI.HahnWilson.LaurentDg.quasiIso_iff line 234
  35. abbrev OAI.HahnWilson.LaurentDg.Derived line 250
  36. abbrev OAI.HahnWilson.LaurentDg.localization line 252
  37. theorem OAI.HahnWilson.LaurentDg.localization_isLocalization line 255
  38. lemma OAI.HahnWilson.LaurentDg.exponent_exists_unique line 280
  39. abbrev OAI.HahnWilson.LaurentDg.derivedHomology line 294
  40. def OAI.HahnWilson.LaurentDg.localizationHomologyIso line 297