OAI/GroupTheory/Congruence/Stabilization.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

Block stabilization, homology actions, quotient vanishing, and congruence cokernels.

  1. def OAI.CoboundaryExpanders.Blocks.gammaStabilization line 24
  2. def OAI.CoboundaryExpanders.Blocks.gammaReindex line 32
  3. theorem OAI.CoboundaryExpanders.Blocks.reindexSL_E line 48
  4. theorem OAI.CoboundaryExpanders.Blocks.stabilize_commutes_tail line 57
  5. theorem OAI.CoboundaryExpanders.Blocks.exists_pair_permutation line 66
  6. theorem OAI.CoboundaryExpanders.Blocks.elementary_centralizes_complement line 83
  7. def OAI.CoboundaryExpanders.Actions.coeff line 103
  8. def OAI.CoboundaryExpanders.Actions.induced line 106
  9. theorem OAI.CoboundaryExpanders.Actions.induced_id line 110
  10. theorem OAI.CoboundaryExpanders.Actions.induced_congr line 113
  11. theorem OAI.CoboundaryExpanders.Actions.induced_comp line 116
  12. theorem OAI.CoboundaryExpanders.Actions.induced_equiv_surjective line 122
  13. def OAI.CoboundaryExpanders.Actions.conjugation line 133
  14. theorem OAI.CoboundaryExpanders.Actions.conjugation_one line 137
  15. theorem OAI.CoboundaryExpanders.Actions.conjugation_mul line 143
  16. def OAI.CoboundaryExpanders.Actions.fixingSubgroup line 151
  17. theorem OAI.CoboundaryExpanders.Actions.centralizer_fixes_image line 166
  18. theorem OAI.CoboundaryExpanders.Actions.centralizer_fixes_of_surjective line 176
  19. instance OAI.CoboundaryExpanders.Blocks.gammaNormal line 192
  20. theorem OAI.CoboundaryExpanders.Blocks.elementary_fixes_complement_image line 195
  21. theorem OAI.CoboundaryExpanders.Blocks.trivial_action_of_stabilization line 207
  22. def OAI.CoboundaryExpanders.Blocks.StabilizationObligation line 220
  23. abbrev OAI.CoboundaryExpanders.QuotientVanishing.K line 231
  24. def OAI.CoboundaryExpanders.QuotientVanishing.gammaInU line 233
  25. theorem OAI.CoboundaryExpanders.QuotientVanishing.gammaInU_conj line 240
  26. theorem OAI.CoboundaryExpanders.QuotientVanishing.conjugation_in_U line 249
  27. theorem OAI.CoboundaryExpanders.QuotientVanishing.gamma_isZero_of_U_and_action line 264
  28. theorem OAI.CoboundaryExpanders.QuotientVanishing.gamma_isZero_of_U_and_stabilization line 290
  29. theorem OAI.CoboundaryExpanders.Construction.congruence_homology_transition_surjective line 305
  30. theorem OAI.CoboundaryExpanders.Blocks.gammaStabilization_coe line 331
  31. theorem OAI.CoboundaryExpanders.Blocks.gammaStabilization_natural line 334
  32. theorem OAI.CoboundaryExpanders.Blocks.stabilizeSL_left_block line 348
  33. theorem OAI.CoboundaryExpanders.Blocks.stabilizeSL_entry line 356
  34. theorem OAI.CoboundaryExpanders.Blocks.stabilizeSL_two line 376
  35. theorem OAI.CoboundaryExpanders.Blocks.gammaStabilization_two line 395
  36. abbrev OAI.CoboundaryExpanders.Cokernel.Coker line 411
  37. def OAI.CoboundaryExpanders.Cokernel.transition line 413
  38. theorem OAI.CoboundaryExpanders.Cokernel.transition_mk line 421
  39. theorem OAI.CoboundaryExpanders.Cokernel.transition_surjective line 425
  40. theorem OAI.CoboundaryExpanders.Cokernel.surjective_iff_coker_subsingleton line 433
  41. theorem OAI.CoboundaryExpanders.Cokernel.surjective_of_zero_coker_transition line 437
  42. abbrev OAI.CoboundaryExpanders.CongruenceCokernels.H line 456
  43. def OAI.CoboundaryExpanders.CongruenceCokernels.stabilization line 458
  44. def OAI.CoboundaryExpanders.CongruenceCokernels.transition line 461
  45. theorem OAI.CoboundaryExpanders.CongruenceCokernels.group_natural line 464
  46. theorem OAI.CoboundaryExpanders.CongruenceCokernels.natural line 470
  47. abbrev OAI.CoboundaryExpanders.CongruenceCokernels.C line 477
  48. def OAI.CoboundaryExpanders.CongruenceCokernels.cokerTransition line 479
  49. def OAI.CoboundaryExpanders.CongruenceCokernels.ProZero line 483
  50. theorem OAI.CoboundaryExpanders.CongruenceCokernels.transition_surjective line 486
  51. theorem OAI.CoboundaryExpanders.CongruenceCokernels.cokerTransition_surjective line 491
  52. theorem OAI.CoboundaryExpanders.CongruenceCokernels.stabilization_surjective_of_proZero line 497
  53. theorem OAI.CoboundaryExpanders.CongruenceCokernels.two_step_surjective_of_proZero line 508
  54. theorem OAI.CoboundaryExpanders.CongruenceCokernels.gamma_isZero_of_U_and_proZero line 517