OAI/GroupTheory/Congruence/CongruenceFrames.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

Row-parabolic groups, row-frame actions, finite images, and congruence stabilizers.

  1. abbrev OAI.CoboundaryExpanders.RowParabolic.Idx line 19
  2. def OAI.CoboundaryExpanders.RowParabolic.fixed line 21
  3. lemma OAI.CoboundaryExpanders.RowParabolic.block_form line 37
  4. def OAI.CoboundaryExpanders.RowParabolic.project line 46
  5. def OAI.CoboundaryExpanders.RowParabolic.ofBlocks line 62
  6. lemma OAI.CoboundaryExpanders.RowParabolic.project_ofBlocks line 67
  7. def OAI.CoboundaryExpanders.RowParabolic.sectionHom line 70
  8. def OAI.CoboundaryExpanders.RowParabolic.map line 80
  9. lemma OAI.CoboundaryExpanders.RowParabolic.map_surjective line 89
  10. lemma OAI.CoboundaryExpanders.Unimodular.normalize_rows line 112
  11. theorem OAI.CoboundaryExpanders.Unimodular.row_completion line 127
  12. lemma OAI.CoboundaryExpanders.Unimodular.frame_linearEquiv line 179
  13. lemma OAI.CoboundaryExpanders.Unimodular.frame_map line 187
  14. lemma OAI.CoboundaryExpanders.Unimodular.frame_injective line 199
  15. lemma OAI.CoboundaryExpanders.RowFrames.smul_eq line 225
  16. def OAI.CoboundaryExpanders.RowFrames.linearAction line 228
  17. lemma OAI.CoboundaryExpanders.RowFrames.frame_smul line 236
  18. lemma OAI.CoboundaryExpanders.RowFrames.standard_fixed_iff line 241
  19. lemma OAI.CoboundaryExpanders.Construction.residue_isUnit line 264
  20. theorem OAI.CoboundaryExpanders.Construction.trunc_SL_surjective line 271
  21. theorem OAI.CoboundaryExpanders.Unimodular.row_completion_of_residue_frame line 286
  22. theorem OAI.CoboundaryExpanders.Unimodular.row_completion_residue line 307
  23. lemma OAI.CoboundaryExpanders.Construction.residue_surjective line 318
  24. theorem OAI.CoboundaryExpanders.Construction.trunc_SL_surjective_any line 323
  25. theorem OAI.CoboundaryExpanders.Construction.trunc_frame_lift line 328
  26. abbrev OAI.CoboundaryExpanders.RowFrames.standard line 349
  27. lemma OAI.CoboundaryExpanders.RowFrames.standard_frame line 350
  28. lemma OAI.CoboundaryExpanders.RowFrames.inverse_smul_standard line 355
  29. lemma OAI.CoboundaryExpanders.RowFrames.row_frame line 359
  30. theorem OAI.CoboundaryExpanders.RowFrames.same_reduction_orbit line 364
  31. abbrev OAI.CoboundaryExpanders.MultiParabolic.group line 411
  32. def OAI.CoboundaryExpanders.MultiParabolic.toFixed line 414
  33. def OAI.CoboundaryExpanders.MultiParabolic.project line 417
  34. def OAI.CoboundaryExpanders.MultiParabolic.sectionValue line 429
  35. lemma OAI.CoboundaryExpanders.MultiParabolic.project_surjective line 450
  36. lemma OAI.CoboundaryExpanders.MultiParabolic.kernel_form line 454
  37. def OAI.CoboundaryExpanders.MultiParabolic.kernelBlock line 465
  38. lemma OAI.CoboundaryExpanders.MultiParabolic.kernelBlock_injective line 478
  39. theorem OAI.CoboundaryExpanders.MultiParabolic.project_homology_isIso line 485
  40. lemma OAI.CoboundaryExpanders.MultiParabolic.homology_isZero line 493
  41. lemma OAI.CoboundaryExpanders.RowFrames.reindex_smul line 509
  42. lemma OAI.CoboundaryExpanders.RowFrames.frame_coordinates line 518
  43. def OAI.CoboundaryExpanders.RowFrames.kernelReindex line 522
  44. lemma OAI.CoboundaryExpanders.RowFrames.same_reduction_orbit_coordinates line 539
  45. def OAI.CoboundaryExpanders.RowFrames.splitCoordinates line 556
  46. def OAI.CoboundaryExpanders.FiniteImage.equiv line 568
  47. lemma OAI.CoboundaryExpanders.FiniteImage.equiv_val line 577
  48. lemma OAI.CoboundaryExpanders.FiniteImage.equiv_symm_val line 580
  49. def OAI.CoboundaryExpanders.FiniteImage.matching line 584
  50. lemma OAI.CoboundaryExpanders.FiniteImage.matching_val line 589
  51. lemma OAI.CoboundaryExpanders.FiniteImage.image_eq_of_matching line 597
  52. def OAI.CoboundaryExpanders.FiniteImage.enumeration line 611
  53. def OAI.CoboundaryExpanders.FiniteImage.familyEquiv line 614
  54. lemma OAI.CoboundaryExpanders.FiniteImage.familyEquiv_val line 622
  55. lemma OAI.CoboundaryExpanders.RowFrames.map_smul line 632
  56. lemma OAI.CoboundaryExpanders.RowFrames.kernel_smul line 639
  57. lemma OAI.CoboundaryExpanders.RowFrames.complex_invariant line 651
  58. abbrev OAI.CoboundaryExpanders.CongruenceFrames.source line 664
  59. abbrev OAI.CoboundaryExpanders.CongruenceFrames.reduce line 665
  60. abbrev OAI.CoboundaryExpanders.CongruenceFrames.residueVector line 667
  61. abbrev OAI.CoboundaryExpanders.CongruenceFrames.target line 669
  62. instance OAI.CoboundaryExpanders.CongruenceFrames.invariant line 672
  63. lemma OAI.CoboundaryExpanders.CongruenceFrames.reduce_injOn line 675
  64. def OAI.CoboundaryExpanders.CongruenceFrames.reduction line 684
  65. lemma OAI.CoboundaryExpanders.CongruenceFrames.reduce_smul line 694
  66. lemma OAI.CoboundaryExpanders.CongruenceFrames.face_invariant line 698
  67. lemma OAI.CoboundaryExpanders.CongruenceFrames.target_exact line 707
  68. lemma OAI.CoboundaryExpanders.CongruenceFrames.source_exact line 713
  69. lemma OAI.CoboundaryExpanders.CongruenceFrames.ordered_lift line 727
  70. lemma OAI.CoboundaryExpanders.CongruenceFrames.face_surjective line 748
  71. lemma OAI.CoboundaryExpanders.CongruenceFrames.face_fiber line 776
  72. def OAI.CoboundaryExpanders.CongruenceFrames.orbitParam line 803