OAI/GroupTheory/SimpleAmenable/Configurations/SymmetricComponents.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SimpleAmenable.SymmetricConfiguration.generator line 15
  2. lemma OAI.SimpleAmenable.SymmetricConfiguration.component_pow line 16
  3. lemma OAI.SimpleAmenable.SymmetricConfiguration.generator_surjective line 22
  4. lemma OAI.SimpleAmenable.SymmetricConfiguration.generator_cofinal line 25
  5. def OAI.SimpleAmenable.SymmetricConfiguration.standardNerveInclusion line 29
  6. def OAI.SimpleAmenable.SymmetricConfiguration.standardFiberInclusion line 34
  7. instance OAI.SimpleAmenable.SymmetricConfiguration.standardFiberInclusion_faithful line 36
  8. instance OAI.SimpleAmenable.SymmetricConfiguration.standardFiberInclusion_full line 38
  9. instance OAI.SimpleAmenable.SymmetricConfiguration.standardFiberInclusion_essSurj line 40
  10. instance OAI.SimpleAmenable.SymmetricConfiguration.standardFiberInclusion_isEquivalence line 42
  11. def OAI.SimpleAmenable.SymmetricConfiguration.standardHomologyIso line 44
  12. lemma OAI.SimpleAmenable.SymmetricConfiguration.tensor_stabilize line 49
  13. def OAI.SimpleAmenable.SymmetricConfiguration.standardTensorIso line 64
  14. def OAI.SimpleAmenable.SymmetricConfiguration.standardCastIso line 71
  15. def OAI.SimpleAmenable.SymmetricConfiguration.standardSuccessorIso line 75
  16. def OAI.SimpleAmenable.SymmetricConfiguration.representativeGeneratorIso line 91
  17. def OAI.SimpleAmenable.SymmetricConfiguration.representativeSuccessorIso line 93
  18. def OAI.SimpleAmenable.SymmetricConfiguration.fiberSuccessorIso line 98
  19. lemma OAI.SimpleAmenable.SymmetricConfiguration.component_successor_isIso line 106
  20. lemma OAI.SimpleAmenable.SymmetricConfiguration.component_sequence_succ line 124
  21. lemma OAI.SimpleAmenable.SymmetricConfiguration.componentStable_finite line 133
  22. lemma OAI.SimpleAmenable.SymmetricConfiguration.componentStableH1_finite line 145
  23. lemma OAI.SimpleAmenable.SymmetricConfiguration.componentStableH2_finite line 147
  24. lemma OAI.SimpleAmenable.SymmetricConfiguration.component_fg line 149
  25. lemma OAI.SimpleAmenable.SymmetricConfiguration.component_homology_finite line 154
  26. lemma OAI.SimpleAmenable.SymmetricConfiguration.triple_homology_finite line 160