OAI/GroupTheory/Congruence/FrameHomology.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

Shapiro comparison, frame resolution homology, augmentation ranges, and triviality of conjugation.

  1. def OAI.CoboundaryExpanders.ActualShapiro.barF line 19
  2. lemma OAI.CoboundaryExpanders.ActualShapiro.barF_single line 25
  3. def OAI.CoboundaryExpanders.ActualShapiro.barMap line 37
  4. abbrev OAI.CoboundaryExpanders.ActualShapiro.restrictedResolution line 60
  5. lemma OAI.CoboundaryExpanders.ActualShapiro.bar_augmentation line 64
  6. def OAI.CoboundaryExpanders.ActualShapiro.barHomotopy line 82
  7. def OAI.CoboundaryExpanders.ActualShapiro.barEquiv line 89
  8. def OAI.CoboundaryExpanders.ActualShapiro.indBase line 99
  9. lemma OAI.CoboundaryExpanders.ActualShapiro.indBase_apply line 103
  10. def OAI.CoboundaryExpanders.ActualShapiro.inducedChainMap line 105
  11. lemma OAI.CoboundaryExpanders.ActualShapiro.chain_factorization line 110
  12. def OAI.CoboundaryExpanders.ActualShapiro.inducedChainEquiv line 132
  13. theorem OAI.CoboundaryExpanders.ActualShapiro.indBase_isIso line 138
  14. lemma OAI.CoboundaryExpanders.CosetModules.hom_ext_base line 166
  15. def OAI.CoboundaryExpanders.CosetModules.indToCoset line 187
  16. lemma OAI.CoboundaryExpanders.CosetModules.indBase_comp_toCoset line 191
  17. lemma OAI.CoboundaryExpanders.CosetModules.indBase_fixed line 196
  18. def OAI.CoboundaryExpanders.CosetModules.cosetToInd line 203
  19. lemma OAI.CoboundaryExpanders.CosetModules.base_comp_toInd line 207
  20. def OAI.CoboundaryExpanders.CosetModules.indCosetIso line 221
  21. theorem OAI.CoboundaryExpanders.CosetModules.base_isIso line 235
  22. def OAI.CoboundaryExpanders.CosetSums.projection line 260
  23. lemma OAI.CoboundaryExpanders.CosetSums.projection_coeff line 275
  24. lemma OAI.CoboundaryExpanders.CosetSums.inclusion_coeff line 278
  25. lemma OAI.CoboundaryExpanders.CosetSums.sum_inclusion_projection line 293
  26. lemma OAI.CoboundaryExpanders.CosetSums.chainsMap_eval line 321
  27. theorem OAI.CoboundaryExpanders.CosetSums.homology_generated line 328
  28. theorem OAI.CoboundaryExpanders.CosetSums.homology_isZero line 372
  29. theorem OAI.CoboundaryExpanders.CosetSums.map_range_le line 392
  30. theorem OAI.CoboundaryExpanders.PermutationProjectivity.homology_isZero line 424
  31. lemma OAI.CoboundaryExpanders.RowFrames.normalization_fixed line 442
  32. lemma OAI.CoboundaryExpanders.CongruenceFrames.face_fixed_iff line 459
  33. def OAI.CoboundaryExpanders.CongruenceFrames.completion line 472
  34. lemma OAI.CoboundaryExpanders.CongruenceFrames.completion_row line 479
  35. def OAI.CoboundaryExpanders.CongruenceFrames.normalize line 491
  36. lemma OAI.CoboundaryExpanders.CongruenceFrames.normalize_fixed_iff line 497
  37. def OAI.CoboundaryExpanders.CongruenceFrames.stabilizerEquiv line 533
  38. lemma OAI.CoboundaryExpanders.CongruenceFrames.stabilizer_homology_isZero line 555
  39. lemma OAI.CoboundaryExpanders.CongruenceFrames.chains_homology_isZero line 563
  40. def OAI.CoboundaryExpanders.MultiParabolic.sectionHom line 578
  41. lemma OAI.CoboundaryExpanders.MultiParabolic.project_section line 590
  42. lemma OAI.CoboundaryExpanders.MultiParabolic.section_homology_isIso line 593
  43. def OAI.CoboundaryExpanders.MultiParabolic.inclusion line 601
  44. lemma OAI.CoboundaryExpanders.MultiParabolic.inclusion_section line 608
  45. lemma OAI.CoboundaryExpanders.MultiParabolic.inclusion_hom_range line 613
  46. def OAI.CoboundaryExpanders.CongruenceFrames.vertexCompletion line 633
  47. lemma OAI.CoboundaryExpanders.CongruenceFrames.vertex_normalization_map line 637
  48. theorem OAI.CoboundaryExpanders.CongruenceFrames.vertex_image_stable line 660
  49. def OAI.CoboundaryExpanders.InfiniteChains.Complex.augmentedData line 686
  50. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.augmentation_exact_of_exactIn line 696
  51. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.augmentedData_exact line 705
  52. lemma OAI.CoboundaryExpanders.Unimodular.singleton_mem line 718
  53. lemma OAI.CoboundaryExpanders.CongruenceFrames.source_vertex line 731
  54. lemma OAI.CoboundaryExpanders.CongruenceFrames.H0_boundary line 736
  55. lemma OAI.CoboundaryExpanders.CongruenceFrames.H0_exact line 744
  56. theorem OAI.CoboundaryExpanders.CongruenceFrames.augmentation_homology_epi line 761
  57. lemma OAI.CoboundaryExpanders.PermutationProjectivity.chainsIso_single line 784
  58. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.orbitBase_augmentation line 795
  59. theorem OAI.CoboundaryExpanders.InfiniteChains.Complex.augmentation_range_le line 808
  60. theorem OAI.CoboundaryExpanders.CongruenceFrames.stabilization_surjective line 837
  61. theorem OAI.CoboundaryExpanders.CongruenceFrames.conjugation_trivial line 850