OAI/GroupTheory/Congruence/Resolution.lean

GitHub source file

101 declarations, 0 contain sorry, 0 declared as axioms

Partial resolutions, orbit projectivity, and homology of finite congruence coset complexes.

  1. abbrev OAI.CoboundaryExpanders.PartialResolution.X line 27
  2. def OAI.CoboundaryExpanders.PartialResolution.lowIso line 29
  3. def OAI.CoboundaryExpanders.PartialResolution.highIso line 32
  4. def OAI.CoboundaryExpanders.PartialResolution.augment line 35
  5. theorem OAI.CoboundaryExpanders.PartialResolution.augment_condition line 38
  6. instance OAI.CoboundaryExpanders.PartialResolution.(instance at line 43) line 43
  7. def OAI.CoboundaryExpanders.PartialResolution.d line 45
  8. theorem OAI.CoboundaryExpanders.PartialResolution.lowIso_inv_hom line 59
  9. theorem OAI.CoboundaryExpanders.PartialResolution.highIso_inv_hom line 63
  10. theorem OAI.CoboundaryExpanders.PartialResolution.d_comp_d line 67
  11. def OAI.CoboundaryExpanders.PartialResolution.complex line 84
  12. theorem OAI.CoboundaryExpanders.PartialResolution.complex_d line 86
  13. def OAI.CoboundaryExpanders.PartialResolution.short line 90
  14. def OAI.CoboundaryExpanders.PartialResolution.kernelShort line 93
  15. theorem OAI.CoboundaryExpanders.PartialResolution.kernelShort_exact line 97
  16. def OAI.CoboundaryExpanders.PartialResolution.augmentShort line 108
  17. theorem OAI.CoboundaryExpanders.PartialResolution.augmentShort_exact line 112
  18. def OAI.CoboundaryExpanders.PartialResolution.lowShortIso line 138
  19. def OAI.CoboundaryExpanders.PartialResolution.kernelShortIso line 145
  20. def OAI.CoboundaryExpanders.PartialResolution.augmentShortIso line 152
  21. lemma OAI.CoboundaryExpanders.PartialResolution.d_high line 160
  22. def OAI.CoboundaryExpanders.PartialResolution.tailShortIso line 165
  23. theorem OAI.CoboundaryExpanders.PartialResolution.complex_exactAt_succ line 180
  24. theorem OAI.CoboundaryExpanders.PartialResolution.complex_projective line 198
  25. def OAI.CoboundaryExpanders.PartialResolution.π line 206
  26. def OAI.CoboundaryExpanders.PartialResolution.augmentationShortIso line 213
  27. def OAI.CoboundaryExpanders.PartialResolution.resolution line 230
  28. lemma OAI.CoboundaryExpanders.PartialResolution.complex_d_low line 250
  29. lemma OAI.CoboundaryExpanders.PartialResolution.low_comm line 261
  30. def OAI.CoboundaryExpanders.PartialResolution.mappedLowShortIso line 271
  31. def OAI.CoboundaryExpanders.PartialResolution.mappedHomologyIso line 286
  32. def OAI.CoboundaryExpanders.PartialResolution.derivedIso line 295
  33. def OAI.CoboundaryExpanders.CoinvariantHomology.trivialTensorIso line 310
  34. def OAI.CoboundaryExpanders.CoinvariantHomology.coinvariantChainsIso line 317
  35. def OAI.CoboundaryExpanders.CoinvariantHomology.homologyIso line 321
  36. theorem OAI.CoboundaryExpanders.TypedCosetFaces.groupHomology_isZero_of_acyclic line 343
  37. abbrev OAI.CoboundaryExpanders.Construction.infiniteCosetComplex line 375
  38. lemma OAI.CoboundaryExpanders.Construction.uLocalGroup_odd line 378
  39. def OAI.CoboundaryExpanders.Construction.OppositionAcyclic line 387
  40. theorem OAI.CoboundaryExpanders.Construction.u_homology_isZero_of_opposition line 392
  41. theorem OAI.CoboundaryExpanders.Construction.gamma_isZero_of_opposition_and_proZero line 404
  42. def OAI.CoboundaryExpanders.KernelCosetOrbits.cosetMap line 420
  43. lemma OAI.CoboundaryExpanders.KernelCosetOrbits.cosetMap_mk line 426
  44. lemma OAI.CoboundaryExpanders.KernelCosetOrbits.cosetMap_smul line 429
  45. lemma OAI.CoboundaryExpanders.KernelCosetOrbits.cosetMap_eq_iff line 435
  46. def OAI.CoboundaryExpanders.KernelCosetOrbits.orbitMap line 458
  47. lemma OAI.CoboundaryExpanders.KernelCosetOrbits.orbitMap_bijective line 461
  48. def OAI.CoboundaryExpanders.KernelCosetOrbits.orbitEquiv line 472
  49. lemma OAI.CoboundaryExpanders.KernelCosetOrbits.orbitEquiv_mk line 476
  50. theorem OAI.CoboundaryExpanders.KernelCosetOrbits.stabilizer_eq_bot line 479
  51. def OAI.CoboundaryExpanders.KernelCosetOrbits.project line 497
  52. lemma OAI.CoboundaryExpanders.KernelCosetOrbits.cosetMap_project line 501
  53. abbrev OAI.CoboundaryExpanders.TypedCosetFaces.imageGroups line 515
  54. def OAI.CoboundaryExpanders.TypedCosetFaces.vertexMap line 517
  55. lemma OAI.CoboundaryExpanders.TypedCosetFaces.vertexMap_vertex line 521
  56. lemma OAI.CoboundaryExpanders.TypedCosetFaces.image_face line 525
  57. lemma OAI.CoboundaryExpanders.TypedCosetFaces.vertexMap_injOn line 530
  58. def OAI.CoboundaryExpanders.TypedCosetFaces.quotientFaceMap line 540
  59. lemma OAI.CoboundaryExpanders.TypedCosetFaces.quotientFaceMap_graded line 548
  60. lemma OAI.CoboundaryExpanders.TypedCosetFaces.quotientFaceMap_surjective line 554
  61. instance OAI.CoboundaryExpanders.TypedCosetFaces.kernelInvariant line 562
  62. lemma OAI.CoboundaryExpanders.TypedCosetFaces.kernel_smul_graded line 568
  63. lemma OAI.CoboundaryExpanders.TypedCosetFaces.quotientFaceMap_invariant line 574
  64. lemma OAI.CoboundaryExpanders.TypedCosetFaces.quotientFaceMap_eq_iff line 581
  65. abbrev OAI.CoboundaryExpanders.TypedCosetFaces.KernelCoinvariantChains line 624
  66. def OAI.CoboundaryExpanders.TypedCosetFaces.quotientChainMap line 626
  67. lemma OAI.CoboundaryExpanders.TypedCosetFaces.quotientChainMap_single line 629
  68. lemma OAI.CoboundaryExpanders.TypedCosetFaces.quotientChainMap_invariant line 633
  69. def OAI.CoboundaryExpanders.TypedCosetFaces.toQuotient line 642
  70. lemma OAI.CoboundaryExpanders.TypedCosetFaces.toQuotient_single line 645
  71. def OAI.CoboundaryExpanders.TypedCosetFaces.liftFace line 650
  72. lemma OAI.CoboundaryExpanders.TypedCosetFaces.quotient_liftFace line 653
  73. def OAI.CoboundaryExpanders.TypedCosetFaces.fromQuotient line 657
  74. lemma OAI.CoboundaryExpanders.TypedCosetFaces.fromQuotient_single line 661
  75. lemma OAI.CoboundaryExpanders.TypedCosetFaces.fromQuotient_toQuotient line 667
  76. lemma OAI.CoboundaryExpanders.TypedCosetFaces.toQuotient_fromQuotient line 684
  77. def OAI.CoboundaryExpanders.TypedCosetFaces.quotientChainsEquiv line 692
  78. lemma OAI.CoboundaryExpanders.TypedCosetFaces.image_erase_vertex line 697
  79. lemma OAI.CoboundaryExpanders.TypedCosetFaces.quotientChainMap_boundary line 705
  80. def OAI.CoboundaryExpanders.TypedCosetFaces.kernelCoinvariantBoundary line 732
  81. lemma OAI.CoboundaryExpanders.TypedCosetFaces.toQuotient_boundary line 736
  82. abbrev OAI.CoboundaryExpanders.TypedCosetFaces.kernelCoinvariantComplex line 742
  83. def OAI.CoboundaryExpanders.TypedCosetFaces.kernelCoinvariantQuotientIso line 746
  84. theorem OAI.CoboundaryExpanders.TypedCosetFaces.kernel_face_stabilizer line 770
  85. abbrev OAI.CoboundaryExpanders.PermutationProjectivity.Orbit line 797
  86. def OAI.CoboundaryExpanders.PermutationProjectivity.orbitStabilizer line 798
  87. def OAI.CoboundaryExpanders.PermutationProjectivity.orbitBasis line 801
  88. lemma OAI.CoboundaryExpanders.PermutationProjectivity.orbitBasis_apply line 804
  89. lemma OAI.CoboundaryExpanders.PermutationProjectivity.orbitBasis_smul line 807
  90. def OAI.CoboundaryExpanders.PermutationProjectivity.chainsIso line 812
  91. theorem OAI.CoboundaryExpanders.PermutationProjectivity.projective_of_odd line 830
  92. theorem OAI.CoboundaryExpanders.PermutationProjectivity.projective_of_free line 839
  93. lemma OAI.CoboundaryExpanders.TypedCosetFaces.kernel_projective_chains line 858
  94. def OAI.CoboundaryExpanders.TypedCosetFaces.kernelHomologyQuotientIso line 862
  95. abbrev OAI.CoboundaryExpanders.Construction.quotientProjection line 896
  96. lemma OAI.CoboundaryExpanders.Construction.quotientProjection_cross_injective line 899
  97. lemma OAI.CoboundaryExpanders.Construction.quotientProjection_intersections line 908
  98. abbrev OAI.CoboundaryExpanders.Construction.quotientTypedComplex line 933
  99. def OAI.CoboundaryExpanders.Construction.gammaQuotientKernelEquiv line 936
  100. def OAI.CoboundaryExpanders.Construction.matrixKernelHomologyIso line 941
  101. theorem OAI.CoboundaryExpanders.Construction.quotientTyped_homology_isZero line 956