OAI/GroupTheory/Congruence/Parabolic.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

Actual parabolic stabilizers, F2 homological stability maps, and matrix duality.

  1. abbrev OAI.CoboundaryExpanders.ActualParabolic.Idx line 26
  2. def OAI.CoboundaryExpanders.ActualParabolic.rowFixed line 28
  3. def OAI.CoboundaryExpanders.ActualParabolic.group line 44
  4. theorem OAI.CoboundaryExpanders.ActualParabolic.block_form line 47
  5. def OAI.CoboundaryExpanders.ActualParabolic.projectValue line 58
  6. def OAI.CoboundaryExpanders.ActualParabolic.projectSL line 64
  7. def OAI.CoboundaryExpanders.ActualParabolic.project line 78
  8. def OAI.CoboundaryExpanders.ActualParabolic.sectionValue line 89
  9. theorem OAI.CoboundaryExpanders.ActualParabolic.project_surjective line 109
  10. theorem OAI.CoboundaryExpanders.ActualParabolic.kernel_form line 113
  11. def OAI.CoboundaryExpanders.ActualParabolic.kernelColumn line 122
  12. theorem OAI.CoboundaryExpanders.ActualParabolic.kernelColumn_injective line 135
  13. theorem OAI.CoboundaryExpanders.ActualParabolic.project_homology_isIso line 146
  14. def OAI.CoboundaryExpanders.ActualParabolic.sectionHom line 160
  15. theorem OAI.CoboundaryExpanders.ActualParabolic.project_comp_section line 173
  16. theorem OAI.CoboundaryExpanders.ActualParabolic.section_homology_isIso line 177
  17. def OAI.CoboundaryExpanders.ActualParabolic.idxEquiv line 208
  18. def OAI.CoboundaryExpanders.ActualParabolic.inclusion line 211
  19. theorem OAI.CoboundaryExpanders.ActualParabolic.inclusion_comp_section line 219
  20. theorem OAI.CoboundaryExpanders.ActualParabolic.stabilization_homology_factor line 241
  21. theorem OAI.CoboundaryExpanders.ActualParabolic.stabilization_surjective_iff_parabolic line 249
  22. theorem OAI.CoboundaryExpanders.ActualParabolic.stabilization_injective_iff_parabolic line 267
  23. abbrev OAI.CoboundaryExpanders.F2Stability.hom line 298
  24. lemma OAI.CoboundaryExpanders.F2Stability.hom_comp line 301
  25. lemma OAI.CoboundaryExpanders.F2Stability.hom_id line 306
  26. lemma OAI.CoboundaryExpanders.F2Stability.endomorphism_hom_eq_id line 309
  27. def OAI.CoboundaryExpanders.F2Stability.meetConj line 315
  28. def OAI.CoboundaryExpanders.ActualParabolic.shear line 328
  29. lemma OAI.CoboundaryExpanders.ActualParabolic.shear_mem line 333
  30. lemma OAI.CoboundaryExpanders.ActualParabolic.shear_inv line 337
  31. def OAI.CoboundaryExpanders.ActualParabolic.shearConj line 345
  32. lemma OAI.CoboundaryExpanders.ActualParabolic.project_comp_shearConj line 350
  33. theorem OAI.CoboundaryExpanders.ActualParabolic.shearConj_homology_eq_id line 362
  34. def OAI.CoboundaryExpanders.ActualParabolic.shearFin line 373
  35. lemma OAI.CoboundaryExpanders.ActualParabolic.inclusion_comp_shearConj line 377
  36. theorem OAI.CoboundaryExpanders.ActualParabolic.shearFin_fixes_stable_image line 390
  37. lemma OAI.CoboundaryExpanders.MatrixDual.transpose_mul line 406
  38. lemma OAI.CoboundaryExpanders.MatrixDual.transpose_one line 411
  39. lemma OAI.CoboundaryExpanders.MatrixDual.transpose_transpose line 415
  40. lemma OAI.CoboundaryExpanders.MatrixDual.transpose_inv line 418
  41. def OAI.CoboundaryExpanders.MatrixDual.dual line 422
  42. lemma OAI.CoboundaryExpanders.MatrixDual.dual_apply line 429
  43. lemma OAI.CoboundaryExpanders.MatrixDual.dual_dual line 431
  44. lemma OAI.CoboundaryExpanders.MatrixDual.map_transpose line 433
  45. lemma OAI.CoboundaryExpanders.MatrixDual.map_dual line 436
  46. lemma OAI.CoboundaryExpanders.MatrixDual.reindex_dual line 440
  47. lemma OAI.CoboundaryExpanders.MatrixDual.block_dual line 445
  48. lemma OAI.CoboundaryExpanders.MatrixDual.stabilize_dual line 456
  49. lemma OAI.CoboundaryExpanders.MatrixDual.dual_mem_gamma line 465
  50. def OAI.CoboundaryExpanders.MatrixDual.gammaDual line 469
  51. lemma OAI.CoboundaryExpanders.MatrixDual.gammaDual_stabilization line 476
  52. lemma OAI.CoboundaryExpanders.F2Stability.hom_equiv_isIso line 488
  53. lemma OAI.CoboundaryExpanders.MatrixDual.gammaDual_conj line 510
  54. theorem OAI.CoboundaryExpanders.MatrixDual.dual_fixes_stable_image line 519
  55. theorem OAI.CoboundaryExpanders.ActualParabolic.lowerShear_fixes_stable_image line 543
  56. def OAI.CoboundaryExpanders.Actions.fixingImage line 563
  57. lemma OAI.CoboundaryExpanders.ActualParabolic.idxEquiv_inl line 586
  58. lemma OAI.CoboundaryExpanders.ActualParabolic.idxEquiv_inr line 587
  59. lemma OAI.CoboundaryExpanders.ActualParabolic.upperRoot_shear line 589
  60. lemma OAI.CoboundaryExpanders.ActualParabolic.dual_root line 607
  61. abbrev OAI.CoboundaryExpanders.ActualParabolic.stableFixed line 614
  62. lemma OAI.CoboundaryExpanders.ActualParabolic.upper_root_mem line 617
  63. lemma OAI.CoboundaryExpanders.ActualParabolic.lower_root_mem line 624
  64. theorem OAI.CoboundaryExpanders.ActualParabolic.polynomial_fixes_stable_image line 630