OAI/GroupTheory/SimpleAmenable/Simplicial/CanonicalShapiro.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CanonicalShapiro.barLift line 11
  2. lemma OAI.CanonicalShapiro.barLift_single line 15
  3. lemma OAI.CanonicalShapiro.barLift_d line 20
  4. def OAI.CanonicalShapiro.barMap line 40
  5. lemma OAI.CanonicalShapiro.diagonal_inv_single line 49
  6. lemma OAI.CanonicalShapiro.bar_π_zero_single line 70
  7. lemma OAI.CanonicalShapiro.barMap_π line 77
  8. def OAI.CanonicalShapiro.barComparison line 95
  9. lemma OAI.CanonicalShapiro.barComparison_hom line 112
  10. def OAI.CanonicalShapiro.indUnit line 115
  11. lemma OAI.CanonicalShapiro.indUnit_apply line 118
  12. lemma OAI.CanonicalShapiro.coinvariantsTensor_map_mk line 122
  13. def OAI.CanonicalShapiro.tensorBarMap line 127
  14. lemma OAI.CanonicalShapiro.chainsIso_hom_single line 133
  15. lemma OAI.CanonicalShapiro.chainsIso_inv_mk_single line 141
  16. lemma OAI.CanonicalShapiro.tensorBarMap_f_mk line 151
  17. def OAI.CanonicalShapiro.resTensorIso line 161
  18. lemma OAI.CanonicalShapiro.resTensorIso_hom_f line 167
  19. lemma OAI.CanonicalShapiro.resIso_hom_f_mk line 171
  20. lemma OAI.CanonicalShapiro.chainsMap_factorization line 180
  21. def OAI.CanonicalShapiro.chainsEquivalence line 201
  22. lemma OAI.CanonicalShapiro.chainsEquivalence_hom line 210
  23. lemma OAI.CanonicalShapiro.isIso_map_indUnit line 215