OAI/GroupTheory/Congruence/Coinvariants.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

Simplicial group actions, permutation modules, coset sums, and chain coinvariants.

  1. def OAI.CoboundaryExpanders.InfiniteChains.rawMap line 23
  2. lemma OAI.CoboundaryExpanders.InfiniteChains.rawMap_single line 27
  3. lemma OAI.CoboundaryExpanders.InfiniteChains.rawMap_boundary line 31
  4. def OAI.CoboundaryExpanders.InfiniteChains.Complex.mapFace line 45
  5. def OAI.CoboundaryExpanders.InfiniteChains.Complex.map line 48
  6. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.map_single line 52
  7. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.embed_map line 57
  8. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.map_boundary line 67
  9. def OAI.CoboundaryExpanders.FinsuppPermutation.ρ line 88
  10. lemma OAI.CoboundaryExpanders.FinsuppPermutation.ρ_single line 103
  11. abbrev OAI.CoboundaryExpanders.FinsuppPermutation.rep line 107
  12. def OAI.CoboundaryExpanders.FinsuppPermutation.coeffIso line 109
  13. def OAI.CoboundaryExpanders.InfiniteChains.Complex.Invariant line 125
  14. instance OAI.CoboundaryExpanders.InfiniteChains.Complex.faceMulAction line 130
  15. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.smul_face_val line 147
  16. abbrev OAI.CoboundaryExpanders.InfiniteChains.Complex.chainsRep line 150
  17. def OAI.CoboundaryExpanders.InfiniteChains.Complex.boundaryRep line 152
  18. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.boundaryRep_squared line 157
  19. def OAI.CoboundaryExpanders.InfiniteChains.Complex.repComplex line 163
  20. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.repComplex_d line 168
  21. def OAI.CoboundaryExpanders.InfiniteChains.Complex.augmentationRep line 172
  22. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.augmentationRep_boundary line 181
  23. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.repComplex_exactAt line 187
  24. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.augmentationRep_exact line 198
  25. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.augmentationRep_epi line 205
  26. instance OAI.CoboundaryExpanders.TypedCosetFaces.vertexMulAction line 217
  27. lemma OAI.CoboundaryExpanders.TypedCosetFaces.map_face line 223
  28. lemma OAI.CoboundaryExpanders.TypedCosetFaces.types_card line 228
  29. instance OAI.CoboundaryExpanders.TypedCosetFaces.complexInvariant line 233
  30. abbrev OAI.CoboundaryExpanders.TypedCosetFaces.Types line 238
  31. abbrev OAI.CoboundaryExpanders.TypedCosetFaces.Basis line 239
  32. instance OAI.CoboundaryExpanders.TypedCosetFaces.basisMulAction line 241
  33. def OAI.CoboundaryExpanders.TypedCosetFaces.gradedFace line 246
  34. lemma OAI.CoboundaryExpanders.TypedCosetFaces.gradedFace_bijective line 253
  35. def OAI.CoboundaryExpanders.TypedCosetFaces.gradedEquiv line 271
  36. lemma OAI.CoboundaryExpanders.TypedCosetFaces.gradedFace_mk line 274
  37. lemma OAI.CoboundaryExpanders.TypedCosetFaces.gradedFace_smul line 277
  38. abbrev OAI.CoboundaryExpanders.CosetModules.permutation line 303
  39. def OAI.CoboundaryExpanders.CosetModules.orbitVector line 305
  40. theorem OAI.CoboundaryExpanders.CosetModules.orbitVector_mk line 315
  41. theorem OAI.CoboundaryExpanders.CosetModules.orbitVector_smul line 319
  42. def OAI.CoboundaryExpanders.CosetModules.extend line 326
  43. theorem OAI.CoboundaryExpanders.CosetModules.extend_single line 340
  44. def OAI.CoboundaryExpanders.CosetModules.base line 347
  45. theorem OAI.CoboundaryExpanders.CosetModules.projective_permutation line 361
  46. theorem OAI.CoboundaryExpanders.CosetModules.projective_permutation_of_invertible_order line 397
  47. theorem OAI.CoboundaryExpanders.CosetModules.projective_permutation_of_odd_order line 411
  48. abbrev OAI.CoboundaryExpanders.CosetSums.Basis line 425
  49. instance OAI.CoboundaryExpanders.CosetSums.(instance at line 426) line 426
  50. abbrev OAI.CoboundaryExpanders.CosetSums.permutation line 430
  51. def OAI.CoboundaryExpanders.CosetSums.inclusion line 432
  52. theorem OAI.CoboundaryExpanders.CosetSums.inclusion_single line 449
  53. def OAI.CoboundaryExpanders.CosetSums.descend line 455
  54. theorem OAI.CoboundaryExpanders.CosetSums.descend_single line 477
  55. theorem OAI.CoboundaryExpanders.CosetSums.projective line 484
  56. theorem OAI.CoboundaryExpanders.CosetSums.projective_of_odd_order line 503
  57. def OAI.CoboundaryExpanders.TypedCosetFaces.chainsIso line 516
  58. lemma OAI.CoboundaryExpanders.TypedCosetFaces.stabilizer_le line 535
  59. lemma OAI.CoboundaryExpanders.TypedCosetFaces.stabilizer_finite line 539
  60. lemma OAI.CoboundaryExpanders.TypedCosetFaces.stabilizer_odd line 546
  61. theorem OAI.CoboundaryExpanders.TypedCosetFaces.projective_chains line 551
  62. abbrev OAI.CoboundaryExpanders.TypedCosetFaces.Simplex line 566
  63. def OAI.CoboundaryExpanders.TypedCosetFaces.typeFace line 568
  64. def OAI.CoboundaryExpanders.TypedCosetFaces.baseFace line 571
  65. lemma OAI.CoboundaryExpanders.TypedCosetFaces.typeFace_baseFace line 574
  66. lemma OAI.CoboundaryExpanders.TypedCosetFaces.typeFace_smul line 577
  67. lemma OAI.CoboundaryExpanders.TypedCosetFaces.face_orbit_base line 584
  68. def OAI.CoboundaryExpanders.TypedCosetFaces.typeMap line 591
  69. lemma OAI.CoboundaryExpanders.TypedCosetFaces.typeMap_single line 594
  70. lemma OAI.CoboundaryExpanders.TypedCosetFaces.typeMap_invariant line 598
  71. abbrev OAI.CoboundaryExpanders.TypedCosetFaces.CoinvariantChains line 606
  72. def OAI.CoboundaryExpanders.TypedCosetFaces.toTypes line 608
  73. lemma OAI.CoboundaryExpanders.TypedCosetFaces.toTypes_single line 611
  74. def OAI.CoboundaryExpanders.TypedCosetFaces.fromTypes line 615
  75. lemma OAI.CoboundaryExpanders.TypedCosetFaces.fromTypes_single line 619
  76. lemma OAI.CoboundaryExpanders.TypedCosetFaces.fromTypes_toTypes line 624
  77. lemma OAI.CoboundaryExpanders.TypedCosetFaces.toTypes_fromTypes line 640
  78. def OAI.CoboundaryExpanders.TypedCosetFaces.typesEquiv line 647
  79. lemma OAI.CoboundaryExpanders.TypedCosetFaces.types_erase_vertex line 651
  80. lemma OAI.CoboundaryExpanders.TypedCosetFaces.typeMap_boundary line 656
  81. def OAI.CoboundaryExpanders.TypedCosetFaces.coinvariantBoundary line 680
  82. lemma OAI.CoboundaryExpanders.TypedCosetFaces.toTypes_boundary line 683
  83. abbrev OAI.CoboundaryExpanders.TypedCosetFaces.coinvariantComplex line 689
  84. def OAI.CoboundaryExpanders.TypedCosetFaces.coinvariantSimplexIso line 692
  85. theorem OAI.CoboundaryExpanders.TypedCosetFaces.coinvariant_homology_isZero line 707