OAI/GroupTheory/Congruence/ProStability.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

Positive exactness, coefficient change, Bockstein groups, integral pro-stability support, and F2 reductions.

  1. theorem OAI.CoboundaryExpanders.Construction.U_constantCoeff line 25
  2. theorem OAI.CoboundaryExpanders.Construction.cycleGenerated_eq_U line 35
  3. theorem OAI.CoboundaryExpanders.Construction.infinite_locals_generate line 50
  4. def OAI.CoboundaryExpanders.TypedCosetFaces.singletonFace line 83
  5. def OAI.CoboundaryExpanders.TypedCosetFaces.pairFace line 86
  6. lemma OAI.CoboundaryExpanders.TypedCosetFaces.boundary_pair line 91
  7. abbrev OAI.CoboundaryExpanders.TypedCosetFaces.Components line 101
  8. def OAI.CoboundaryExpanders.TypedCosetFaces.component line 103
  9. lemma OAI.CoboundaryExpanders.TypedCosetFaces.component_same_chamber line 106
  10. lemma OAI.CoboundaryExpanders.TypedCosetFaces.component_mul_local line 121
  11. lemma OAI.CoboundaryExpanders.TypedCosetFaces.component_mul_closure line 133
  12. lemma OAI.CoboundaryExpanders.TypedCosetFaces.component_constant line 152
  13. lemma OAI.CoboundaryExpanders.TypedCosetFaces.singletonFace_surjective line 157
  14. theorem OAI.CoboundaryExpanders.TypedCosetFaces.augmentation_exact_of_generation line 163
  15. theorem OAI.CoboundaryExpanders.Construction.infinite_augmentation_exact line 193
  16. theorem OAI.CoboundaryExpanders.Construction.oppositionAcyclic_iff_positive line 198
  17. theorem OAI.CoboundaryExpanders.reduction_to_positive_open_inputs line 209
  18. structure OAI.CoboundaryExpanders.ProCoefficientChange.Tower line 227
  19. structure OAI.CoboundaryExpanders.ProCoefficientChange.Map line 236
  20. def OAI.CoboundaryExpanders.ProCoefficientChange.Map.ProSurjective line 243
  21. def OAI.CoboundaryExpanders.ProCoefficientChange.Map.ProInjective line 246
  22. lemma OAI.CoboundaryExpanders.ProCoefficientChange.Map.natural_apply line 249
  23. lemma OAI.CoboundaryExpanders.ProCoefficientChange.Tower.trans_apply line 254
  24. structure OAI.CoboundaryExpanders.ProCoefficientChange.Bockstein line 258
  25. theorem OAI.CoboundaryExpanders.ProCoefficientChange.proSurjective_of_bockstein line 264
  26. abbrev OAI.CoboundaryExpanders.BocksteinGroups.ZRep line 315
  27. abbrev OAI.CoboundaryExpanders.BocksteinGroups.FRep line 316
  28. def OAI.CoboundaryExpanders.BocksteinGroups.twice line 318
  29. def OAI.CoboundaryExpanders.BocksteinGroups.red line 320
  30. def OAI.CoboundaryExpanders.BocksteinGroups.sequence line 323
  31. lemma OAI.CoboundaryExpanders.BocksteinGroups.sequence_exact line 331
  32. abbrev OAI.CoboundaryExpanders.BocksteinGroups.HZ line 348
  33. abbrev OAI.CoboundaryExpanders.BocksteinGroups.HF line 349
  34. def OAI.CoboundaryExpanders.BocksteinGroups.reduce line 351
  35. def OAI.CoboundaryExpanders.BocksteinGroups.delta line 352
  36. lemma OAI.CoboundaryExpanders.BocksteinGroups.exact_reduce_delta line 354
  37. lemma OAI.CoboundaryExpanders.BocksteinGroups.exact_delta_twice line 358
  38. def OAI.CoboundaryExpanders.BocksteinGroups.coeff line 388
  39. def OAI.CoboundaryExpanders.BocksteinGroups.chainMap line 391
  40. def OAI.CoboundaryExpanders.BocksteinGroups.homMap line 396
  41. lemma OAI.CoboundaryExpanders.BocksteinGroups.homMap_id line 400
  42. lemma OAI.CoboundaryExpanders.BocksteinGroups.homMap_comp line 402
  43. lemma OAI.CoboundaryExpanders.BocksteinGroups.chain_coeff_natural line 410
  44. lemma OAI.CoboundaryExpanders.BocksteinGroups.hom_coeff_natural line 419
  45. def OAI.CoboundaryExpanders.BocksteinGroups.sequenceMap line 426
  46. lemma OAI.CoboundaryExpanders.BocksteinGroups.delta_natural line 441
  47. lemma OAI.CoboundaryExpanders.BocksteinGroups.reduce_natural line 447
  48. structure OAI.CoboundaryExpanders.GroupProStability.Groups line 458
  49. structure OAI.CoboundaryExpanders.GroupProStability.Hom line 466
  50. def OAI.CoboundaryExpanders.GroupProStability.tower line 472
  51. def OAI.CoboundaryExpanders.GroupProStability.map line 483
  52. def OAI.CoboundaryExpanders.GroupProStability.redMap line 490
  53. def OAI.CoboundaryExpanders.GroupProStability.deltaMap line 494
  54. def OAI.CoboundaryExpanders.GroupProStability.bockstein line 498
  55. theorem OAI.CoboundaryExpanders.GroupProStability.modTwo_proSurjective line 505
  56. def OAI.CoboundaryExpanders.IntegralProStability.groups line 523
  57. def OAI.CoboundaryExpanders.IntegralProStability.stabilization line 530
  58. def OAI.CoboundaryExpanders.IntegralProStability.ProIso line 534
  59. def OAI.CoboundaryExpanders.IntegralProStability.IntegralStability line 538
  60. theorem OAI.CoboundaryExpanders.IntegralProStability.modTwo_proSurjective line 541
  61. abbrev OAI.CoboundaryExpanders.HomologyScalars.SC line 552
  62. abbrev OAI.CoboundaryExpanders.HomologyScalars.ZC line 553
  63. abbrev OAI.CoboundaryExpanders.HomologyScalars.FC line 554
  64. abbrev OAI.CoboundaryExpanders.HomologyScalars.RC line 555
  65. def OAI.CoboundaryExpanders.HomologyScalars.degreeAddEquiv line 557
  66. def OAI.CoboundaryExpanders.HomologyScalars.degreeIso line 564
  67. lemma OAI.CoboundaryExpanders.HomologyScalars.single_compare line 567
  68. lemma OAI.CoboundaryExpanders.HomologyScalars.differential line 585
  69. def OAI.CoboundaryExpanders.HomologyScalars.chainIso line 598
  70. def OAI.CoboundaryExpanders.HomologyScalars.homologyIso line 605
  71. def OAI.CoboundaryExpanders.HomologyScalars.coeffZ line 613
  72. def OAI.CoboundaryExpanders.HomologyScalars.coeffF line 614
  73. def OAI.CoboundaryExpanders.HomologyScalars.mapZ line 615
  74. def OAI.CoboundaryExpanders.HomologyScalars.mapF line 616
  75. lemma OAI.CoboundaryExpanders.HomologyScalars.chain_natural line 618
  76. lemma OAI.CoboundaryExpanders.HomologyScalars.homology_natural line 639
  77. lemma OAI.CoboundaryExpanders.IntegralProStability.natural_apply line 663
  78. lemma OAI.CoboundaryExpanders.IntegralProStability.moduleIso_right_inv line 670
  79. lemma OAI.CoboundaryExpanders.IntegralProStability.natural_lift line 674
  80. theorem OAI.CoboundaryExpanders.IntegralProStability.proZero_of_integral line 690
  81. theorem OAI.CoboundaryExpanders.IntegralProStability.proZero_of_stability line 709
  82. theorem OAI.CoboundaryExpanders.reduction_to_opposition_integral_stability_and_OVB line 719
  83. lemma OAI.CoboundaryExpanders.BocksteinGroups.homMap_zero_eq line 744
  84. lemma OAI.CoboundaryExpanders.BocksteinGroups.homMap_zero_bijective line 753
  85. theorem OAI.CoboundaryExpanders.IntegralProStability.proIso_zero line 764
  86. theorem OAI.CoboundaryExpanders.IntegralProStability.integralStability_iff_positive line 781
  87. theorem OAI.CoboundaryExpanders.reduction_to_positive_literature_inputs line 796