OAI/GroupTheory/SimpleAmenable/Homology/IntegralTransgressionFinite.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.IntegralTransgression.onCycles_kills_homology_kernel line 20
  2. theorem OAI.SimpleAmenable.IntegralTransgression.cycles_to_h2_surjective line 29
  3. def OAI.SimpleAmenable.IntegralTransgression.transgression line 34
  4. theorem OAI.SimpleAmenable.IntegralTransgression.transgression_cycle line 41
  5. theorem OAI.SimpleAmenable.IntegralTransgression.transgression_surjective line 45
  6. theorem OAI.SimpleAmenable.IntegralTransgression.kernel_fg line 53
  7. theorem OAI.SimpleAmenable.universalKernel_fg_of_integral_h2 line 66
  8. theorem OAI.SimpleAmenable.finitelyPresented_of_central_cover_h2 line 72
  9. abbrev OAI.SimpleAmenable.IntegralHomology.coefficients line 86
  10. def OAI.SimpleAmenable.IntegralHomology.coefficientMap line 90
  11. def OAI.SimpleAmenable.IntegralHomology.mapH2 line 93
  12. def OAI.SimpleAmenable.IntegralHomology.mapC2 line 96
  13. theorem OAI.SimpleAmenable.IntegralHomology.mapC2_single line 99
  14. def OAI.SimpleAmenable.IntegralHomology.prism1 line 103
  15. def OAI.SimpleAmenable.IntegralHomology.prism2 line 106
  16. theorem OAI.SimpleAmenable.IntegralHomology.prism1_single line 111
  17. theorem OAI.SimpleAmenable.IntegralHomology.prism2_single line 115
  18. lemma OAI.SimpleAmenable.IntegralHomology.boundary2_single line 120
  19. lemma OAI.SimpleAmenable.IntegralHomology.boundary3_single line 125
  20. theorem OAI.SimpleAmenable.IntegralHomology.prism_identity line 131