OAI/GroupTheory/Congruence/OddHomology.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

Permutation orbit parameters, locally finite odd groups, quotient coinvariants, and bar augmentations.

  1. structure OAI.CoboundaryExpanders.FinsuppPermutation.OrbitParam line 17
  2. def OAI.CoboundaryExpanders.FinsuppPermutation.OrbitParam.toCoin line 25
  3. lemma OAI.CoboundaryExpanders.FinsuppPermutation.OrbitParam.toCoin_mk line 33
  4. def OAI.CoboundaryExpanders.FinsuppPermutation.OrbitParam.chosen line 36
  5. lemma OAI.CoboundaryExpanders.FinsuppPermutation.OrbitParam.chosen_spec line 37
  6. def OAI.CoboundaryExpanders.FinsuppPermutation.OrbitParam.fromCoin line 39
  7. lemma OAI.CoboundaryExpanders.FinsuppPermutation.OrbitParam.fromCoin_single line 42
  8. lemma OAI.CoboundaryExpanders.FinsuppPermutation.OrbitParam.mk_eq line 47
  9. lemma OAI.CoboundaryExpanders.FinsuppPermutation.OrbitParam.from_to line 54
  10. lemma OAI.CoboundaryExpanders.FinsuppPermutation.OrbitParam.to_from line 63
  11. def OAI.CoboundaryExpanders.FinsuppPermutation.OrbitParam.coinEquiv line 70
  12. lemma OAI.CoboundaryExpanders.FinsuppPermutation.OrbitParam.coinEquiv_mk line 72
  13. def OAI.CoboundaryExpanders.FinsuppPermutation.OrbitParam.H0Equiv line 76
  14. lemma OAI.CoboundaryExpanders.FinsuppPermutation.OrbitParam.H0_naturality line 79
  15. structure OAI.CoboundaryExpanders.InfiniteChains.Complex.Reduction line 110
  16. def OAI.CoboundaryExpanders.InfiniteChains.Complex.Reduction.face line 118
  17. def OAI.CoboundaryExpanders.InfiniteChains.Complex.Reduction.chains line 122
  18. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.Reduction.chains_single line 126
  19. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.Reduction.image_erase line 130
  20. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.Reduction.raw_boundary line 140
  21. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.Reduction.embed_chains line 152
  22. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.Reduction.boundary line 163
  23. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.Reduction.sum_chains line 181
  24. lemma OAI.CoboundaryExpanders.LocallyFiniteOdd.coinvariant_relation_support line 195
  25. lemma OAI.CoboundaryExpanders.LocallyFiniteOdd.norm_zero_of_relation line 216
  26. lemma OAI.CoboundaryExpanders.LocallyFiniteOdd.coinvariant_norm_subgroup line 225
  27. theorem OAI.CoboundaryExpanders.LocallyFiniteOdd.coinvariants_map_injective line 239
  28. theorem OAI.CoboundaryExpanders.LocallyFiniteOdd.coinvariants_preserves_monomorphisms line 279
  29. theorem OAI.CoboundaryExpanders.LocallyFiniteOdd.coinvariants_preserves_homology line 286
  30. abbrev OAI.CoboundaryExpanders.QuotientCoinvariants.L line 306
  31. abbrev OAI.CoboundaryExpanders.QuotientCoinvariants.R line 307
  32. def OAI.CoboundaryExpanders.QuotientCoinvariants.homTo line 309
  33. def OAI.CoboundaryExpanders.QuotientCoinvariants.homFrom line 317
  34. def OAI.CoboundaryExpanders.QuotientCoinvariants.homEquiv line 335
  35. def OAI.CoboundaryExpanders.QuotientCoinvariants.adjunction line 348
  36. instance OAI.CoboundaryExpanders.QuotientCoinvariants.(instance at line 362) line 362
  37. instance OAI.CoboundaryExpanders.QuotientCoinvariants.(instance at line 370) line 370
  38. instance OAI.CoboundaryExpanders.QuotientCoinvariants.(instance at line 372) line 372
  39. theorem OAI.CoboundaryExpanders.QuotientCoinvariants.preservesMonomorphisms line 383
  40. theorem OAI.CoboundaryExpanders.QuotientCoinvariants.preservesHomology line 389
  41. def OAI.CoboundaryExpanders.QuotientCoinvariants.descendedResolution line 393
  42. def OAI.CoboundaryExpanders.QuotientCoinvariants.inflatedTrivialIso line 402
  43. def OAI.CoboundaryExpanders.QuotientCoinvariants.totalAdjunction line 406
  44. def OAI.CoboundaryExpanders.QuotientCoinvariants.totalCoinvariantsIso line 411
  45. lemma OAI.CoboundaryExpanders.QuotientCoinvariants.totalCoinvariantsIso_double_mk line 415
  46. def OAI.CoboundaryExpanders.QuotientCoinvariants.trivialIso line 423
  47. def OAI.CoboundaryExpanders.QuotientCoinvariants.quotientResolution line 450
  48. def OAI.CoboundaryExpanders.QuotientCoinvariants.homologyIso line 457
  49. def OAI.CoboundaryExpanders.QuotientCoinvariants.quotientBarF line 487
  50. theorem OAI.CoboundaryExpanders.QuotientCoinvariants.quotientBarF_single line 494
  51. def OAI.CoboundaryExpanders.QuotientCoinvariants.quotientBar line 507
  52. lemma OAI.CoboundaryExpanders.QuotientBarAugmentation.diagonal_inv_single line 546
  53. theorem OAI.CoboundaryExpanders.QuotientBarAugmentation.bar_augmentation_single line 567
  54. theorem OAI.CoboundaryExpanders.QuotientCoinvariants.quotientBar_augmentation line 582
  55. def OAI.CoboundaryExpanders.QuotientCoinvariants.quotientBarHomotopy line 600
  56. def OAI.CoboundaryExpanders.QuotientCoinvariants.quotientBarEquiv line 609
  57. abbrev OAI.CoboundaryExpanders.QuotientCoinvariantModel.complex line 636
  58. def OAI.CoboundaryExpanders.QuotientCoinvariantModel.chainsIso line 639
  59. theorem OAI.CoboundaryExpanders.QuotientCoinvariantModel.chainsIso_hom_single line 646
  60. lemma OAI.CoboundaryExpanders.QuotientCoinvariants.totalCoinvariantsIso_inv_mk line 663
  61. def OAI.CoboundaryExpanders.QuotientCoinvariants.coinvariantQuotient line 670
  62. def OAI.CoboundaryExpanders.QuotientCoinvariants.trivialQuotient line 676
  63. theorem OAI.CoboundaryExpanders.QuotientCoinvariants.quotient_chain_factorization line 679
  64. def OAI.CoboundaryExpanders.QuotientCoinvariants.coinvariantQuotientEquiv line 702
  65. theorem OAI.CoboundaryExpanders.QuotientCoinvariants.quotient_map_isIso line 710
  66. def OAI.CoboundaryExpanders.QuotientCoinvariants.trivialMap line 752
  67. theorem OAI.CoboundaryExpanders.QuotientCoinvariants.surjection_map_isIso line 755
  68. theorem OAI.CoboundaryExpanders.QuotientCoinvariants.localOdd_equiv line 783
  69. def OAI.CoboundaryExpanders.QuotientCoinvariants.semidirectKernelEquiv line 802
  70. theorem OAI.CoboundaryExpanders.QuotientCoinvariants.semidirect_projection_isIso line 815
  71. theorem OAI.CoboundaryExpanders.QuotientCoinvariants.semidirect_section_isIso line 823
  72. theorem OAI.CoboundaryExpanders.LocallyFiniteOdd.vector_group_local_odd line 850
  73. theorem OAI.CoboundaryExpanders.QuotientCoinvariants.vector_semidirect_maps_isIso line 888
  74. theorem OAI.CoboundaryExpanders.QuotientCoinvariants.localOdd_of_injective line 903