OAI/GroupTheory/SimpleAmenable/Homology/ConcreteHomology.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ConcreteHomology.c line 14
  2. abbrev OAI.ConcreteHomology.CC line 15
  3. def OAI.ConcreteHomology.S line 17
  4. abbrev OAI.ConcreteHomology.Cycles line 18
  5. abbrev OAI.ConcreteHomology.boundary line 19
  6. abbrev OAI.ConcreteHomology.H line 20
  7. def OAI.ConcreteHomology.π line 21
  8. lemma OAI.ConcreteHomology.π_eq_zero line 23
  9. lemma OAI.ConcreteHomology.π_surjective line 26
  10. def OAI.ConcreteHomology.sFunctor line 29
  11. instance OAI.ConcreteHomology.(instance at line 35) line 35
  12. def OAI.ConcreteHomology.sIso line 39
  13. def OAI.ConcreteHomology.functor line 43
  14. instance OAI.ConcreteHomology.(instance at line 46) line 46
  15. lemma OAI.ConcreteHomology.prev line 57
  16. lemma OAI.ConcreteHomology.next line 58
  17. def OAI.ConcreteHomology.naturalIso line 63
  18. def OAI.ConcreteHomology.iso line 67
  19. def OAI.ConcreteHomology.cyclesMap line 70
  20. lemma OAI.ConcreteHomology.cyclesMap_val line 74
  21. lemma OAI.ConcreteHomology.map_π line 80
  22. abbrev OAI.ConeCoordinates.C line 98
  23. abbrev OAI.ConeCoordinates.left line 99
  24. abbrev OAI.ConeCoordinates.right line 100
  25. abbrev OAI.ConeCoordinates.fst line 101
  26. abbrev OAI.ConeCoordinates.snd line 102
  27. lemma OAI.ConeCoordinates.zero_next line 103
  28. lemma OAI.ConeCoordinates.fst_left line 104
  29. lemma OAI.ConeCoordinates.snd_right line 106
  30. lemma OAI.ConeCoordinates.fst_right line 108
  31. lemma OAI.ConeCoordinates.snd_left line 110
  32. lemma OAI.ConeCoordinates.ext line 112
  33. lemma OAI.ConeCoordinates.ext_zero line 130
  34. lemma OAI.ConeCoordinates.decomp line 132
  35. lemma OAI.ConeCoordinates.decomp_zero line 137
  36. lemma OAI.ConeCoordinates.d_snd line 139
  37. lemma OAI.ConeCoordinates.d_fst line 143
  38. lemma OAI.ConeCoordinates.d_right line 147
  39. lemma OAI.ConeCoordinates.d_left line 151
  40. lemma OAI.ConeCoordinates.d_left_zero line 159
  41. lemma OAI.ConeCoordinates.d_left_cycle line 162