OAI/GroupTheory/SimpleAmenable/Homology/BoundedHomologyEdge.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BoundedHomologyEdge.Hmap line 16
  2. lemma OAI.BoundedHomologyEdge.Hmap_comp line 20
  3. lemma OAI.BoundedHomologyEdge.epi_Hmap_zero line 24
  4. lemma OAI.BoundedHomologyEdge.exact₂ line 27
  5. lemma OAI.BoundedHomologyEdge.exact₁ line 32
  6. lemma OAI.BoundedHomologyEdge.exact₃ line 37
  7. lemma OAI.BoundedHomologyEdge.epi_Hmap_succ_of_mono line 42
  8. lemma OAI.BoundedHomologyEdge.epi_Hmap_succ_of_isZero line 46
  9. lemma OAI.BoundedHomologyEdge.mono_Hmap_of_zero line 50
  10. lemma OAI.BoundedHomologyEdge.isZero_H0_quotient line 54
  11. lemma OAI.BoundedHomologyEdge.isIso_right_of_epi_left line 60
  12. lemma OAI.BoundedHomologyEdge.isIso_H0_i₂ line 74
  13. lemma OAI.BoundedHomologyEdge.isZero_H0_kernel line 81
  14. lemma OAI.BoundedHomologyEdge.H1_isIso line 88
  15. lemma OAI.BoundedHomologyEdge.H2_epi_of_isZero line 98
  16. lemma OAI.BoundedHomologyEdge.H2_epi_of_epi line 105
  17. lemma OAI.BoundedHomologyEdge.isZero_H0_third_kernel line 129
  18. lemma OAI.BoundedHomologyEdge.H2_isIso line 138
  19. lemma OAI.BoundedHomologyEdge.exact_of_comp_mono line 155
  20. lemma OAI.BoundedHomologyEdge.kernel_shortExact line 164
  21. def OAI.BoundedHomologyEdge.lift₂ line 172
  22. lemma OAI.BoundedHomologyEdge.lift₂_ι line 174
  23. lemma OAI.BoundedHomologyEdge.comp_lift₂_zero line 177
  24. def OAI.BoundedHomologyEdge.lift₃ line 181
  25. lemma OAI.BoundedHomologyEdge.lift₃_ι line 184
  26. lemma OAI.BoundedHomologyEdge.comp_lift₃_zero line 188
  27. def OAI.BoundedHomologyEdge.lift₄ line 192
  28. lemma OAI.BoundedHomologyEdge.lift₄_ι line 195
  29. lemma OAI.BoundedHomologyEdge.comp_lift₄_zero line 199
  30. lemma OAI.BoundedHomologyEdge.epi_lift₂ line 203
  31. lemma OAI.BoundedHomologyEdge.epi_lift₃ line 206
  32. lemma OAI.BoundedHomologyEdge.epi_lift₄ line 214
  33. lemma OAI.BoundedHomologyEdge.chain_H2_epi line 223
  34. lemma OAI.BoundedHomologyEdge.chain_H1_isIso line 234
  35. lemma OAI.BoundedHomologyEdge.chain_H2_isIso line 248