OAI/GroupTheory/SimpleAmenable/CentralCovers/PerfectCalculus.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.perfect_hom_to_commGroup line 16
  2. theorem OAI.SimpleAmenable.perfect_lift_unique line 23
  3. theorem OAI.SimpleAmenable.perfect_commutator_central_trivial line 50
  4. theorem OAI.SimpleAmenable.perfect_center_quotient line 61
  5. theorem OAI.SimpleAmenable.central_extension_decomposition line 65
  6. theorem OAI.SimpleAmenable.central_extension_commutator_perfect line 76
  7. theorem OAI.SimpleAmenable.central_extension_commutator_surjective line 96
  8. theorem OAI.SimpleAmenable.commutator_eq_of_central_kernel line 112
  9. theorem OAI.SimpleAmenable.finite_of_perfect_central_cover line 121
  10. def OAI.SimpleAmenable.freeEvaluation line 151
  11. theorem OAI.SimpleAmenable.freeEvaluation_of line 153
  12. theorem OAI.SimpleAmenable.freeEvaluation_surjective line 156
  13. def OAI.SimpleAmenable.centralizingRelations line 159
  14. instance OAI.SimpleAmenable.(instance at line 162) line 162
  15. abbrev OAI.SimpleAmenable.CentralizedFree line 166
  16. def OAI.SimpleAmenable.centralFreeMap line 168
  17. theorem OAI.SimpleAmenable.centralFreeMap_mk line 173
  18. theorem OAI.SimpleAmenable.centralFreeMap_surjective line 177
  19. theorem OAI.SimpleAmenable.centralFreeMap_central line 181
  20. abbrev OAI.SimpleAmenable.UniversalExtension line 196
  21. def OAI.SimpleAmenable.universalProjection line 198
  22. instance OAI.SimpleAmenable.(instance at line 201) line 201
  23. theorem OAI.SimpleAmenable.universalProjection_surjective line 205
  24. theorem OAI.SimpleAmenable.universalProjection_central line 209
  25. theorem OAI.SimpleAmenable.universal_lift_exists line 219
  26. theorem OAI.SimpleAmenable.universal_lift_exists_unique line 251
  27. def OAI.SimpleAmenable.universalLift line 259
  28. theorem OAI.SimpleAmenable.universalLift_spec line 264
  29. def OAI.SimpleAmenable.universalMap line 271
  30. theorem OAI.SimpleAmenable.universalMap_spec line 275
  31. theorem OAI.SimpleAmenable.universalMap_id line 279
  32. theorem OAI.SimpleAmenable.universalMap_comp line 284
  33. def OAI.SimpleAmenable.universalEquiv line 290
  34. instance OAI.SimpleAmenable.universalExtension_finite line 295