OAI/GroupTheory/FiniteType/RepresentationKilling.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RepresentationKilling.stableKernel line 13
  2. theorem OAI.RepresentationKilling.eq_zero line 31
  3. lemma OAI.PresentationGeometry.CellCoverExtension.critical_homology_zero line 59
  4. theorem OAI.PresentationGeometry.CellCoverExtension.coveringCore_connectivity line 88
  5. def OAI.CWCellular.topCycleMap line 118
  6. lemma OAI.CWCellular.topCycleMap_bijective line 125
  7. def OAI.CWCellular.topCycleIso line 133
  8. lemma OAI.CWCellular.exact_of_homology_zero line 138
  9. lemma OAI.CWCellular.complex_exactAt line 153
  10. lemma OAI.CWCellular.contractible_exactAt line 162
  11. lemma OAI.CWCellular.q_zero_isIso line 174
  12. def OAI.CWCellular.zeroIso line 184
  13. def OAI.CWCellular.augmentation line 188
  14. lemma OAI.CWCellular.q_augmentation line 191
  15. lemma OAI.CWCellular.incl_toComplex line 196
  16. lemma OAI.CWCellular.d_augmentation line 201
  17. lemma OAI.CWCellular.augmentation_exact line 207
  18. lemma OAI.CWCellular.augmentation_epi line 231
  19. def OAI.CWCellular.contractibleZeroIso line 242
  20. def OAI.CWCellular.integralAugmentation line 247
  21. structure OAI.CWCellular.SkeletalMap line 258
  22. def OAI.CWCellular.SkeletalMap.onSkel line 264
  23. def OAI.CWCellular.SkeletalMap.absoluteMap line 267
  24. lemma OAI.CWCellular.SkeletalMap.lower_maps line 270
  25. def OAI.CWCellular.SkeletalMap.relativeMap line 273
  26. def OAI.CWCellular.SkeletalMap.sequenceMap line 276
  27. def OAI.CWCellular.SkeletalMap.cellMap line 291
  28. lemma OAI.CWCellular.SkeletalMap.q_natural line 294
  29. lemma OAI.CWCellular.SkeletalMap.delta_natural line 300
  30. lemma OAI.CWCellular.SkeletalMap.d_natural line 305
  31. def OAI.CWCellular.SkeletalMap.chainMap line 311