OAI/GroupTheory/SimpleAmenable/Simplicial/RestrictedMonoidalTranspose.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RestrictedNerve.transposeε line 17
  2. def OAI.RestrictedNerve.transposeμ line 35
  3. lemma OAI.RestrictedNerve.transposeμ_natural_left line 57
  4. lemma OAI.RestrictedNerve.transposeμ_natural_right line 73
  5. instance OAI.RestrictedNerve.transposeMonoidal line 89
  6. instance OAI.RestrictedNerve.transposeBraided line 137
  7. instance OAI.RestrictedNerve.inclusionEssSurj line 156
  8. abbrev OAI.RestrictedNerve.posDiagramInclusion line 158
  9. instance OAI.RestrictedNerve.posDiagramInclusionMonoidal line 160
  10. instance OAI.RestrictedNerve.posDiagramInclusionBraided line 162
  11. instance OAI.RestrictedNerve.posDiagramInclusionEssSurj line 164
  12. instance OAI.RestrictedNerve.posDiagramInclusionEquivalence line 168
  13. def OAI.RestrictedNerve.posDiagramTripleHomologyIso line 172
  14. lemma OAI.RestrictedNerve.reindex_η line 188
  15. lemma OAI.RestrictedNerve.reindex_μ line 191
  16. lemma OAI.RestrictedNerve.map_strings_reindex_id line 193
  17. lemma OAI.RestrictedNerve.map_strings_reindex_comp line 213
  18. def OAI.RestrictedNerve.diagramHorizontal line 237
  19. lemma OAI.RestrictedNerve.eqToHom_transposed_app line 242
  20. lemma OAI.RestrictedNerve.transposed_comp_app line 247
  21. lemma OAI.RestrictedNerve.eqToHom_vertex_app line 253
  22. lemma OAI.RestrictedNerve.stringVertex_reindex line 261
  23. lemma OAI.RestrictedNerve.transpose_reindex line 274

    Distinct definitions of this name: OAI/GroupTheory/SimpleAmenable/Simplicial/MonoidalCongruence.lean:62 (different declaration text). Qualify references as OAI.RestrictedNerve.transpose_reindex@path.

  24. def OAI.RestrictedNerve.diagramTranspose line 295
  25. def OAI.RestrictedNerve.diagramResolutionHomologyIso line 301