OAI/GroupTheory/FiniteType/SingularSigma.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SingularSigma.Space line 14
  2. def OAI.SingularSigma.incl line 16
  3. def OAI.SingularSigma.snd line 17
  4. def OAI.SingularSigma.index line 18
  5. lemma OAI.SingularSigma.index_eq line 19
  6. lemma OAI.SingularSigma.incl_snd line 24
  7. lemma OAI.SingularSigma.index_incl line 30
  8. lemma OAI.SingularSigma.snd_incl line 31
  9. def OAI.SingularSigma.subset line 34
  10. def OAI.SingularSigma.inclPair line 36
  11. def OAI.SingularSigma.merge line 39
  12. lemma OAI.SingularSigma.merge_single line 52
  13. def OAI.SingularSigma.splitAbsolute line 56
  14. lemma OAI.SingularSigma.splitAbsolute_gen line 61
  15. lemma OAI.SingularSigma.splitAbsolute_kill line 68
  16. def OAI.SingularSigma.split line 81
  17. lemma OAI.SingularSigma.split_projection line 86
  18. lemma OAI.SingularSigma.merge_splitAbsolute line 89
  19. lemma OAI.SingularSigma.splitAbsolute_incl line 99
  20. lemma OAI.SingularSigma.merge_split line 110
  21. lemma OAI.SingularSigma.split_merge line 119
  22. instance OAI.SingularSigma.merge_isIso line 128
  23. def OAI.SingularSigma.homologyIso line 132
  24. def OAI.RelativeChains.setIso line 143
  25. lemma OAI.RelativeChains.map_setIso line 148
  26. def OAI.FinsuppHomology.objIso line 156
  27. lemma OAI.FinsuppHomology.obj_isZero line 158
  28. lemma OAI.DiskHomology.boundary_zero line 165
  29. def OAI.DiskHomology.zeroHomologyIso line 175
  30. lemma OAI.DiskHomology.zeroHomology_isZero line 182
  31. def OAI.DiskHomology.cellIso line 190
  32. lemma OAI.DiskHomology.cell_isZero line 194
  33. abbrev OAI.CWSkeletalHomology.complex line 206
  34. lemma OAI.CWSkeletalHomology.boundary_eq line 209
  35. def OAI.CWSkeletalHomology.diskSumIso line 215
  36. def OAI.CWSkeletalHomology.characteristicMap line 222
  37. def OAI.CWSkeletalHomology.characteristicIso line 227
  38. lemma OAI.CWSkeletalHomology.characteristicIso_hom line 232
  39. def OAI.CWSkeletalHomology.basisIso line 235
  40. lemma OAI.CWSkeletalHomology.homology_isZero line 239