OAI/GroupTheory/SimpleAmenable/Simplicial/StageTripleHomology.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ColimitTransfer.transportDiagram line 16
  2. def OAI.ColimitTransfer.transportIso line 21
  3. def OAI.ColimitTransfer.transportCocone line 23
  4. def OAI.ColimitTransfer.transportIsColimit line 28
  5. instance OAI.IntervalBar.Diagram.map₂Monoidal line 41
  6. abbrev OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.tripleDegree line 50
  7. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.tripleEvalIso line 52
  8. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.tripleHomologyStage line 55
  9. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.tripleHomologyCocone line 59
  10. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.tripleHomologyIsColimit line 66
  11. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.tripleEvalIso_hom line 71
  12. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.tripleEval_naturality line 73
  13. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.tripleHomologyStage_map line 83
  14. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.tripleHomologyCocone_ι line 92
  15. lemma OAI.IntervalBar.Diagram.map₂_η_app line 111
  16. lemma OAI.IntervalBar.Diagram.map₂_μ_app line 117
  17. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.map₃_inclusion_comp_obj line 127
  18. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.map₃_inclusion_comp line 170
  19. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.map₃_inclusion_forget_obj line 184
  20. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.map₃_inclusion_forget line 226
  21. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.map₃_inclusion_id_obj line 240
  22. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.map₃_inclusion_id line 276