OAI/GroupTheory/SimpleAmenable/Configurations/SymmetricFaces.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.SymmetricConfiguration.facePermutation line 14
  2. lemma OAI.SimpleAmenable.SymmetricConfiguration.facePermutation_apply line 16
  3. def OAI.SimpleAmenable.SymmetricConfiguration.permHom line 18
  4. lemma OAI.SimpleAmenable.SymmetricConfiguration.permHom_apply line 20
  5. lemma OAI.SimpleAmenable.SymmetricConfiguration.permHom_fixed line 22
  6. lemma OAI.SimpleAmenable.SymmetricConfiguration.permHom_centralizes line 24
  7. lemma OAI.SimpleAmenable.SymmetricConfiguration.permHom_face line 29
  8. lemma OAI.SimpleAmenable.SymmetricConfiguration.homology_face_eq line 34
  9. lemma OAI.SimpleAmenable.SymmetricConfiguration.boundary_two line 41
  10. lemma OAI.SimpleAmenable.SymmetricConfiguration.boundary_three line 45
  11. lemma OAI.SimpleAmenable.SymmetricConfiguration.homology_boundary_two_zero line 51
  12. lemma OAI.SimpleAmenable.SymmetricConfiguration.homology_boundary_three line 55
  13. lemma OAI.SimpleAmenable.SymmetricConfiguration.boundary_square line 61
  14. lemma OAI.SimpleAmenable.SymmetricConfiguration.boundary_exact line 71
  15. lemma OAI.SimpleAmenable.SymmetricConfiguration.boundary_zero_eq_face line 86
  16. lemma OAI.SimpleAmenable.SymmetricConfiguration.boundary_zero_epi line 90
  17. lemma OAI.SimpleAmenable.SymmetricConfiguration.face_H0_isIso line 100
  18. lemma OAI.SimpleAmenable.SymmetricConfiguration.boundary_two_H0_isIso line 106
  19. lemma OAI.SimpleAmenable.SymmetricConfiguration.boundary_zero_H1_isIso line 110
  20. instance OAI.SimpleAmenable.SymmetricConfiguration.empty_subsingleton line 124
  21. def OAI.SimpleAmenable.SymmetricConfiguration.empty line 127
  22. def OAI.SimpleAmenable.SymmetricConfiguration.emptyIso line 129
  23. lemma OAI.SimpleAmenable.SymmetricConfiguration.emptyIso_single line 140
  24. lemma OAI.SimpleAmenable.SymmetricConfiguration.augmentation_pointMap line 144
  25. lemma OAI.SimpleAmenable.SymmetricConfiguration.stabilizer_H1_isIso line 160