OAI/GroupTheory/FiniteType/SingularAction.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SingularAction.actionMap line 15
  2. def OAI.SingularAction.rep line 16
  3. def OAI.SingularAction.val line 30
  4. def OAI.SingularAction.ofVal line 31
  5. lemma OAI.SingularAction.val_surjective line 33
  6. def OAI.SingularAction.fromUniv line 44
  7. lemma OAI.SingularAction.finite_of_univ line 53
  8. lemma OAI.SingularAction.univ_homology_zero line 58
  9. def OAI.CoveringCellGeometry.deckPullback line 84
  10. theorem OAI.CoveringCellGeometry.familyLift_deck line 87
  11. theorem OAI.CoveringCellGeometry.characteristicLift_deck line 105
  12. instance OAI.EquivariantCoverCells.cellAction line 145
  13. def OAI.EquivariantCoverCells.seed line 155
  14. def OAI.EquivariantCoverCells.cellEquiv line 159
  15. theorem OAI.EquivariantCoverCells.cellEquiv_smul line 175
  16. abbrev OAI.EquivariantCoverCells.cellularRepresentation line 180
  17. def OAI.EquivariantCoverCells.abelianEquiv line 183
  18. theorem OAI.EquivariantCoverCells.abelianEquiv_single line 192
  19. def OAI.EquivariantCoverCells.representationEquiv line 198
  20. def OAI.EquivariantCoverCells.freeIso line 211
  21. def OAI.EquivariantCoverCells.freeEquiv line 215
  22. def OAI.EquivariantCoverCells.basis line 224
  23. theorem OAI.EquivariantCoverCells.free line 231
  24. theorem OAI.EquivariantCoverCells.finite line 237
  25. def OAI.EquivariantCoverCells.actionHomeo line 244
  26. lemma OAI.EquivariantCoverCells.chart_smul line 253
  27. lemma OAI.EquivariantCoverCells.homology_finite line 278