OAI/GroupTheory/FiniteType/StandardShapiro.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.StandardShapiro.restrictedResolution line 13
  2. def OAI.StandardShapiro.inclusion line 16
  3. lemma OAI.StandardShapiro.inclusion_π line 19
  4. def OAI.StandardShapiro.comparisonEquiv line 34
  5. def OAI.StandardShapiro.indEquiv line 42
  6. lemma OAI.StandardShapiro.indEquiv_hom_f_mk_tmul line 49
  7. def OAI.FunctionalTree.parentMap line 66
  8. def OAI.FunctionalTree.boundary line 69
  9. def OAI.FunctionalTree.augmentation line 72
  10. lemma OAI.FunctionalTree.parentMap_single line 75
  11. lemma OAI.FunctionalTree.augmentation_single line 79
  12. lemma OAI.FunctionalTree.augmentation_parentMap line 83
  13. lemma OAI.FunctionalTree.augmentation_boundary line 91
  14. def OAI.FunctionalTree.path line 95
  15. lemma OAI.FunctionalTree.boundary_path line 98
  16. lemma OAI.FunctionalTree.single_sub_single_mem_range line 111
  17. lemma OAI.FunctionalTree.range_boundary_eq_ker_augmentation line 119
  18. lemma OAI.FunctionalTree.boundary_injective line 141
  19. lemma OAI.FunctionalTree.augmentation_surjective line 159
  20. def OAI.FunctionalTree.diagonalAction line 170
  21. lemma OAI.FunctionalTree.diagonalAction_single line 173
  22. def OAI.FunctionalTree.diagonalRep line 177
  23. lemma OAI.FunctionalTree.diagonalRep_single line 189
  24. def OAI.FunctionalTree.parentHom line 195
  25. def OAI.FunctionalTree.boundaryHom line 202
  26. lemma OAI.FunctionalTree.boundaryHom_apply line 205
  27. def OAI.FunctionalTree.augmentationHom line 208
  28. lemma OAI.FunctionalTree.augmentationHom_apply line 215
  29. def OAI.FunctionalTree.equivariantComplex line 218
  30. lemma OAI.FunctionalTree.equivariantComplex_shortExact line 223