OAI/Combinatorics/Coboundary/Links.lean

GitHub source file

95 declarations, 0 contain sorry, 0 declared as axioms

Coset-link identifications, product and cut models, and all proper-link cone bounds.

  1. def OAI.CoboundaryExpanders.Construction.localReducedHom line 23
  2. lemma OAI.CoboundaryExpanders.Construction.localReducedHom_surjective line 30
  3. lemma OAI.CoboundaryExpanders.Construction.localQuotient_cross_injective line 36
  4. lemma OAI.CoboundaryExpanders.Construction.localReducedHom_injective line 44
  5. def OAI.CoboundaryExpanders.Construction.localReducedEquiv line 50
  6. lemma OAI.CoboundaryExpanders.Construction.localReducedHom_mem_iff line 55
  7. def OAI.CoboundaryExpanders.Construction.reducedFlagEquiv line 67
  8. lemma OAI.CoboundaryExpanders.Construction.reducedFlagEquiv_stabilizer line 72
  9. def OAI.CoboundaryExpanders.Construction.quotientLinkGroups line 92
  10. lemma OAI.CoboundaryExpanders.Construction.quotientLinkGroups_correspond line 96
  11. def OAI.CoboundaryExpanders.Construction.quotientLinkVertexModel line 117
  12. lemma OAI.CoboundaryExpanders.Construction.quotientLinkVertexModel_injective line 125
  13. theorem OAI.CoboundaryExpanders.Construction.quotientLinkFace_iff line 130
  14. theorem OAI.CoboundaryExpanders.Construction.quotientLinkFace_surjective line 138
  15. def OAI.CoboundaryExpanders.Construction.actualLinkEmbedding line 154
  16. lemma OAI.CoboundaryExpanders.Construction.actualLinkEmbedding_injective line 158
  17. theorem OAI.CoboundaryExpanders.Construction.actualLinkFace_iff line 162
  18. lemma OAI.CoboundaryExpanders.Construction.actualLinkFace_surjective line 171
  19. def OAI.CoboundaryExpanders.Construction.sphericalLinkModel line 185
  20. def OAI.CoboundaryExpanders.Construction.actualVertexLinkModel line 193
  21. theorem OAI.CoboundaryExpanders.Construction.uniform_actual_vertex_cones line 201
  22. def OAI.CoboundaryExpanders.InfiniteChains.Complex.faceLink line 219
  23. def OAI.CoboundaryExpanders.InfiniteChains.Cone.FaceModel.linkModel line 236
  24. lemma OAI.CoboundaryExpanders.InfiniteChains.complex_eq line 259
  25. lemma OAI.CoboundaryExpanders.InfiniteChains.faceLink_empty line 262
  26. lemma OAI.CoboundaryExpanders.InfiniteChains.faceLink_iterated line 267
  27. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.mem_link_left line 280
  28. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.mem_link_right line 283
  29. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.disjoint_split line 287
  30. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.link_eq line 299
  31. def OAI.CoboundaryExpanders.InfiniteChains.Join.emptyLeftModel line 311
  32. def OAI.CoboundaryExpanders.TypedCosetFaces.productGroups line 337
  33. def OAI.CoboundaryExpanders.TypedCosetFaces.productVertex line 341
  34. lemma OAI.CoboundaryExpanders.TypedCosetFaces.productVertex_left line 356
  35. lemma OAI.CoboundaryExpanders.TypedCosetFaces.productVertex_right line 359
  36. def OAI.CoboundaryExpanders.TypedCosetFaces.embedLeft line 362
  37. def OAI.CoboundaryExpanders.TypedCosetFaces.embedRight line 370
  38. def OAI.CoboundaryExpanders.TypedCosetFaces.productVertexEquiv line 378
  39. lemma OAI.CoboundaryExpanders.TypedCosetFaces.productFace_image line 408
  40. lemma OAI.CoboundaryExpanders.TypedCosetFaces.productFace_image_general line 414
  41. theorem OAI.CoboundaryExpanders.TypedCosetFaces.productFace_iff line 424
  42. def OAI.CoboundaryExpanders.InfiniteChains.Cone.FaceModel.trans line 442
  43. def OAI.CoboundaryExpanders.TypedCosetFaces.isoModel line 459
  44. def OAI.CoboundaryExpanders.TypedCosetFaces.productModel line 472
  45. instance OAI.CoboundaryExpanders.MatrixOpposition.cutDecidableEq line 507
  46. instance OAI.CoboundaryExpanders.MatrixOpposition.cutFinite line 508
  47. instance OAI.CoboundaryExpanders.MatrixOpposition.cutFintype line 510
  48. def OAI.CoboundaryExpanders.MatrixOpposition.cutTypeEquiv line 512
  49. lemma OAI.CoboundaryExpanders.MatrixOpposition.cutGroups_correspond line 518
  50. def OAI.CoboundaryExpanders.MatrixOpposition.cutSphericalModel line 531
  51. lemma OAI.CoboundaryExpanders.TypedCosetFaces.standard_face_mem line 547
  52. lemma OAI.CoboundaryExpanders.TypedCosetFaces.linkComplex_eq line 548
  53. def OAI.CoboundaryExpanders.TypedCosetFaces.singleLinkModel line 556
  54. def OAI.CoboundaryExpanders.MatrixOpposition.middleCut line 568
  55. def OAI.CoboundaryExpanders.MatrixOpposition.cutLinkTypes line 569
  56. lemma OAI.CoboundaryExpanders.MatrixOpposition.cutLinkGroups_correspond line 576
  57. def OAI.CoboundaryExpanders.MatrixOpposition.cutProductLinkModel line 593
  58. instance OAI.CoboundaryExpanders.TypedCosetFaces.vertexAction line 605
  59. lemma OAI.CoboundaryExpanders.TypedCosetFaces.smul_vertex line 611
  60. lemma OAI.CoboundaryExpanders.TypedCosetFaces.smul_face line 614
  61. lemma OAI.CoboundaryExpanders.TypedCosetFaces.IsFace.smul line 618
  62. lemma OAI.CoboundaryExpanders.TypedCosetFaces.IsFace.type_card line 623
  63. lemma OAI.CoboundaryExpanders.TypedCosetFaces.coset_pure line 628
  64. lemma OAI.CoboundaryExpanders.TypedCosetFaces.chamber_transitive line 637
  65. lemma OAI.CoboundaryExpanders.TypedCosetFaces.stabilizer_fixes line 648
  66. lemma OAI.CoboundaryExpanders.TypedCosetFaces.remaining_card line 654
  67. lemma OAI.CoboundaryExpanders.TypedCosetFaces.linkFace_smul line 659
  68. lemma OAI.CoboundaryExpanders.TypedCosetFaces.link_chamber_transitive line 669
  69. def OAI.CoboundaryExpanders.InfiniteChains.Cone.BoundedCone.weaken line 701
  70. def OAI.CoboundaryExpanders.InfiniteChains.RankBound line 708
  71. def OAI.CoboundaryExpanders.InfiniteChains.AllLinkCones line 710
  72. lemma OAI.CoboundaryExpanders.InfiniteChains.RankBound.link line 714
  73. lemma OAI.CoboundaryExpanders.InfiniteChains.RankBound.terminal line 721
  74. lemma OAI.CoboundaryExpanders.InfiniteChains.AllLinkCones.weaken line 729
  75. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.FaceModel.pushAllLinks line 734
  76. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.FaceModel.pullAllLinks line 741
  77. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.FaceModel.rankBound line 750
  78. def OAI.CoboundaryExpanders.InfiniteChains.Join.emptyRightModel line 759
  79. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.rankBound line 778
  80. theorem OAI.CoboundaryExpanders.InfiniteChains.Join.allLinkCones line 786
  81. lemma OAI.CoboundaryExpanders.InfiniteChains.singleton_mem_of_mem_face line 823
  82. lemma OAI.CoboundaryExpanders.InfiniteChains.faceLink_congr line 826
  83. lemma OAI.CoboundaryExpanders.InfiniteChains.AllLinkCones.vertexCriterion line 829
  84. def OAI.CoboundaryExpanders.TypedCosetFaces.actionModel line 859
  85. lemma OAI.CoboundaryExpanders.TypedCosetFaces.rankBound line 878
  86. lemma OAI.CoboundaryExpanders.TypedCosetFaces.standard_singleton_face line 883
  87. lemma OAI.CoboundaryExpanders.TypedCosetFaces.standard_link_eq line 885
  88. lemma OAI.CoboundaryExpanders.MatrixOpposition.card_cut line 896
  89. lemma OAI.CoboundaryExpanders.MatrixOpposition.cut_rankBound line 898
  90. lemma OAI.CoboundaryExpanders.MatrixOpposition.cut_middle_link_cones line 901
  91. theorem OAI.CoboundaryExpanders.MatrixOpposition.uniform_cut_allLinkCones line 911
  92. def OAI.CoboundaryExpanders.InfiniteChains.ProperLinkCones line 975
  93. lemma OAI.CoboundaryExpanders.InfiniteChains.ProperLinkCones.vertexCriterion line 979
  94. lemma OAI.CoboundaryExpanders.TypedCosetFaces.allVertexLinks_of_standard line 1004
  95. theorem OAI.CoboundaryExpanders.Construction.uniform_actual_proper_link_cones line 1025