OAI/GroupTheory/Heisenberg/BarDetector.lean

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

Integral Heisenberg groups and evaluation of group homology and cohomology on bar cycles.

  1. structure OAI.BaumConnesCounterexample.Partial.Heisenberg line 10
  2. instance OAI.BaumConnesCounterexample.Partial.Heisenberg.(instance at line 18) line 18
  3. instance OAI.BaumConnesCounterexample.Partial.Heisenberg.(instance at line 20) line 20
  4. instance OAI.BaumConnesCounterexample.Partial.Heisenberg.(instance at line 21) line 21
  5. theorem OAI.BaumConnesCounterexample.Partial.Heisenberg.a_mul line 23
  6. theorem OAI.BaumConnesCounterexample.Partial.Heisenberg.b_mul line 24
  7. theorem OAI.BaumConnesCounterexample.Partial.Heisenberg.c_mul line 25
  8. theorem OAI.BaumConnesCounterexample.Partial.Heisenberg.a_one line 26
  9. theorem OAI.BaumConnesCounterexample.Partial.Heisenberg.b_one line 27
  10. theorem OAI.BaumConnesCounterexample.Partial.Heisenberg.c_one line 28
  11. theorem OAI.BaumConnesCounterexample.Partial.Heisenberg.a_inv line 29
  12. theorem OAI.BaumConnesCounterexample.Partial.Heisenberg.b_inv line 30
  13. theorem OAI.BaumConnesCounterexample.Partial.Heisenberg.c_inv line 31
  14. instance OAI.BaumConnesCounterexample.Partial.Heisenberg.(instance at line 33) line 33
  15. def OAI.BaumConnesCounterexample.Partial.Heisenberg.x line 39
  16. def OAI.BaumConnesCounterexample.Partial.Heisenberg.y line 40
  17. def OAI.BaumConnesCounterexample.Partial.Heisenberg.z line 41
  18. def OAI.BaumConnesCounterexample.Partial.Heisenberg.chooseTwo line 43
  19. lemma OAI.BaumConnesCounterexample.Partial.Heisenberg.two_mul_chooseTwo line 45
  20. lemma OAI.BaumConnesCounterexample.Partial.Heisenberg.chooseTwo_zero line 49
  21. lemma OAI.BaumConnesCounterexample.Partial.Heisenberg.chooseTwo_one line 50
  22. lemma OAI.BaumConnesCounterexample.Partial.Heisenberg.chooseTwo_add line 52
  23. lemma OAI.BaumConnesCounterexample.Partial.Heisenberg.a_pow line 59
  24. lemma OAI.BaumConnesCounterexample.Partial.Heisenberg.b_pow line 64
  25. lemma OAI.BaumConnesCounterexample.Partial.Heisenberg.c_pow line 69
  26. instance OAI.BaumConnesCounterexample.Partial.Heisenberg.(instance at line 78) line 78
  27. lemma OAI.BaumConnesCounterexample.Partial.Heisenberg.eq_one_of_pow_eq_one line 89
  28. instance OAI.BaumConnesCounterexample.Partial.Heisenberg.(instance at line 93) line 93
  29. instance OAI.BaumConnesCounterexample.Partial.Heisenberg.(instance at line 94) line 94
  30. instance OAI.BaumConnesCounterexample.Partial.Heisenberg.(instance at line 95) line 95
  31. def OAI.BaumConnesCounterexample.Partial.Heisenberg.xLine line 97
  32. def OAI.BaumConnesCounterexample.Partial.Heisenberg.yLine line 102
  33. def OAI.BaumConnesCounterexample.Partial.Heisenberg.zLine line 107
  34. lemma OAI.BaumConnesCounterexample.Partial.Heisenberg.x_zpow line 112
  35. lemma OAI.BaumConnesCounterexample.Partial.Heisenberg.y_zpow line 115
  36. lemma OAI.BaumConnesCounterexample.Partial.Heisenberg.z_zpow line 118
  37. lemma OAI.BaumConnesCounterexample.Partial.Heisenberg.normal_form line 121
  38. lemma OAI.BaumConnesCounterexample.Partial.Heisenberg.commutator_x_y line 125
  39. lemma OAI.BaumConnesCounterexample.Partial.Heisenberg.closure_xy line 128
  40. instance OAI.BaumConnesCounterexample.Partial.Heisenberg.(instance at line 140) line 140
  41. abbrev OAI.BaumConnesCounterexample.Partial.Heisenberg.TorusGroup line 143
  42. def OAI.BaumConnesCounterexample.Partial.Heisenberg.torusEmbedding line 145
  43. lemma OAI.BaumConnesCounterexample.Partial.Heisenberg.torusEmbedding_injective line 150
  44. lemma OAI.BaumConnesCounterexample.Partial.Heisenberg.torusEmbedding_eq_zpow line 156
  45. lemma OAI.BaumConnesCounterexample.Partial.Heisenberg.commute_z_x line 161
  46. def OAI.BaumConnesCounterexample.Partial.Heisenberg.omega line 165
  47. lemma OAI.BaumConnesCounterexample.Partial.Heisenberg.omega_one_left line 167
  48. lemma OAI.BaumConnesCounterexample.Partial.Heisenberg.omega_one_right line 168
  49. lemma OAI.BaumConnesCounterexample.Partial.Heisenberg.omega_cocycle line 170
  50. lemma OAI.BaumConnesCounterexample.Partial.Heisenberg.omega_pair_z_x line 175
  51. abbrev OAI.BaumConnesCounterexample.Partial.IntegralCohomology.coefficients line 185
  52. abbrev OAI.BaumConnesCounterexample.Partial.IntegralCohomology.DegreeTwo line 187
  53. def OAI.BaumConnesCounterexample.Partial.IntegralCohomology.pairOnCocycles line 189
  54. lemma OAI.BaumConnesCounterexample.Partial.IntegralCohomology.pairOnCocycles_vanishes line 199
  55. lemma OAI.BaumConnesCounterexample.Partial.IntegralCohomology.projection_surjective line 209
  56. def OAI.BaumConnesCounterexample.Partial.IntegralCohomology.pairEvaluation line 212
  57. lemma OAI.BaumConnesCounterexample.Partial.IntegralCohomology.pairEvaluation_projection line 217
  58. def OAI.BaumConnesCounterexample.Partial.IntegralCohomology.coefficientMap line 222
  59. def OAI.BaumConnesCounterexample.Partial.IntegralCohomology.pullback line 225
  60. lemma OAI.BaumConnesCounterexample.Partial.IntegralCohomology.pairEvaluation_pullback line 228
  61. def OAI.BaumConnesCounterexample.Partial.IntegralCohomology.barPair line 239
  62. lemma OAI.BaumConnesCounterexample.Partial.IntegralCohomology.barPair_mem_cycles line 242
  63. def OAI.BaumConnesCounterexample.Partial.IntegralCohomology.barPairCycle line 249
  64. def OAI.BaumConnesCounterexample.Partial.IntegralCohomology.cochainOnChains line 253
  65. lemma OAI.BaumConnesCounterexample.Partial.IntegralCohomology.cochainOnChains_single line 257
  66. lemma OAI.BaumConnesCounterexample.Partial.IntegralCohomology.cochainOnChains_barPair line 262
  67. lemma OAI.BaumConnesCounterexample.Partial.IntegralCohomology.cochainOnChains_boundary line 266
  68. def OAI.BaumConnesCounterexample.Partial.IntegralCohomology.cochainOnCycles line 283
  69. lemma OAI.BaumConnesCounterexample.Partial.IntegralCohomology.cochainOnCycles_vanishes line 287
  70. def OAI.BaumConnesCounterexample.Partial.IntegralCohomology.cochainOnHomology line 295
  71. lemma OAI.BaumConnesCounterexample.Partial.IntegralCohomology.cochainOnHomology_projection line 302
  72. def OAI.BaumConnesCounterexample.Partial.IntegralCohomology.barPairClass line 307
  73. lemma OAI.BaumConnesCounterexample.Partial.IntegralCohomology.cochainOnHomology_barPairClass line 311
  74. def OAI.BaumConnesCounterexample.Partial.IntegralCohomology.coefficientMapForward line 318
  75. def OAI.BaumConnesCounterexample.Partial.IntegralCohomology.pushforward line 321
  76. lemma OAI.BaumConnesCounterexample.Partial.IntegralCohomology.pushforward_barPairClass line 325
  77. def OAI.BaumConnesCounterexample.Partial.Heisenberg.omegaCocycle line 343
  78. def OAI.BaumConnesCounterexample.Partial.Heisenberg.detectorClass line 348
  79. lemma OAI.BaumConnesCounterexample.Partial.Heisenberg.detectorClass_evaluation line 351
  80. def OAI.BaumConnesCounterexample.Partial.Heisenberg.torusU line 356
  81. def OAI.BaumConnesCounterexample.Partial.Heisenberg.torusV line 357
  82. lemma OAI.BaumConnesCounterexample.Partial.Heisenberg.commute_torusU_torusV line 359
  83. lemma OAI.BaumConnesCounterexample.Partial.Heisenberg.torusEmbedding_u line 361
  84. lemma OAI.BaumConnesCounterexample.Partial.Heisenberg.torusEmbedding_v line 362
  85. def OAI.BaumConnesCounterexample.Partial.Heisenberg.torusBarEvaluation line 364
  86. lemma OAI.BaumConnesCounterexample.Partial.Heisenberg.detectorClass_restriction line 367
  87. lemma OAI.BaumConnesCounterexample.Partial.Heisenberg.detectorClass_multiple_eq_zero_iff line 372
  88. def OAI.BaumConnesCounterexample.Partial.Heisenberg.barTorusHomologyClass line 381
  89. lemma OAI.BaumConnesCounterexample.Partial.Heisenberg.barTorusHomologyClass_eq line 384
  90. lemma OAI.BaumConnesCounterexample.Partial.Heisenberg.barTorusHomologyClass_evaluation line 388
  91. lemma OAI.BaumConnesCounterexample.Partial.Heisenberg.barTorusHomologyClass_multiple_eq_zero_iff line 393
  92. theorem OAI.BaumConnesCounterexample.Partial.Heisenberg.explicitHeisenbergBarDetector line 402