OAI/GroupTheory/SimpleAmenable/Homology/StageCoefficients.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SimpleAmenable.PolygonObject.LabelledStage.Coefficients line 15
2. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.label line 19
3. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.label_injective line 20
4. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.label_mem_support line 21
5. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.label_range line 23
6. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.realize line 25
7. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.realize_at_label line 29
8. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.realize_outside line 37
9. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.coefficientEvaluate line 42
10. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.coefficientEvaluate_realize line 46
11. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.realize_injective line 51
12. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.Admissible line 57
13. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.realize_admissible line 59
14. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.realize_coefficientEvaluate line 69
15. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.admissible_mono line 79
16. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.coefficientRefinement line 82
17. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.realize_refinement line 85
18. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.exists_coefficient_stage line 89
19. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.coefficientDiagram line 107
20. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.coefficientCocone line 119
21. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.coefficientIsColimit line 125