OAI/Geometry/Coboundary/Flags.lean

GitHub source file

134 declarations, 0 contain sorry, 0 declared as axioms

Complete flags, spherical opposition, unitriangular groups, and the flag-coset model.

  1. structure OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag line 16
  2. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.space_zero line 27
  3. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.space_last line 31
  4. def OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.Opposed line 36
  5. def OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.Good line 39
  6. def OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.complex line 42
  7. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.mem_faces line 50
  8. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.rank_le line 54
  9. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.opposed_iff_disjoint line 57
  10. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.opposed_disjoint_below line 65
  11. def OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.forbidden line 70
  12. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.forbidden_rank line 73
  13. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.forbidden_ne_top line 84
  14. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.extension_rank line 91
  15. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.opposed_extension line 97
  16. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.good_extension line 125
  17. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.opposed_line line 132
  18. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.good_line line 138
  19. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.opposed_sup_above line 145
  20. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.lower_rank line 152
  21. def OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.lower line 166
  22. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.disjoint_map_subtype_iff line 179
  23. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.opposed_lower_iff line 190
  24. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.good_lower_map line 207
  25. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.face_has_greatest line 215
  26. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.sup_mem_face line 226
  27. def OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.safeComplex line 232
  28. def OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.carrierApex line 239
  29. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.carrierApex_mono line 243
  30. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.carrierApex_good line 249
  31. def OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.carrier line 258
  32. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.self_mem_carrier line 263
  33. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.carrier_mono line 268
  34. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.carrier_cone line 272
  35. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.map_comap_lower line 295
  36. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.rank_comap_lower line 300
  37. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.good_lower_comap line 304
  38. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.lower_face_map line 315
  39. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.lower_face_comap line 339
  40. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.comap_injOn_lower line 353
  41. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.hyperplane_link_lower line 359
  42. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.insert_greatest_face line 373
  43. theorem OAI.CoboundaryExpanders.SphericalOpposition.exists_vector_avoiding line 394
  44. theorem OAI.CoboundaryExpanders.SphericalOpposition.exists_vector_avoiding_finset line 423
  45. theorem OAI.CoboundaryExpanders.SphericalOpposition.exists_common_good_line line 432
  46. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.safe_filling line 456
  47. def OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.TopBad line 485
  48. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.no_top_filling line 488
  49. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.hyperplane_link_filling line 532
  50. def OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.eliminationBound line 591
  51. def OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.fillingBound line 593
  52. def OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.fieldBound line 595
  53. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.small_filling line 597
  54. theorem OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.exists_uniform_cones line 635
  55. theorem OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.uniform_spherical_exactness line 676
  56. def OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.Opposite line 694
  57. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.opposite_symm line 698
  58. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.opposite_line_rank line 707
  59. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.opposite_line_vector line 719
  60. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.step_span line 737
  61. theorem OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.exists_adapted_basis line 748
  62. def OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.prefixIndex line 774
  63. def OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.suffixIndex line 775
  64. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.prefixIndex_injective line 777
  65. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.suffixIndex_injective line 782
  66. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.adapted_prefix line 789
  67. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.adapted_suffix line 799
  68. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.basis_equiv_span_range line 811
  69. theorem OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.exists_flag_stabilizing_equiv line 817
  70. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.opposed_bot line 848
  71. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.opposed_top line 855
  72. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.extend_opposed line 861
  73. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.interval_opposed line 876
  74. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.rank_injective_on_face line 891
  75. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.face_order_of_rank_le line 900
  76. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.face_has_least line 909
  77. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.face_lower_bound_at line 915
  78. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.face_upper_bound_at line 931
  79. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.insert_rank line 954
  80. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.exists_extend_ranks line 989
  81. def OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.FullFace line 1007
  82. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.exists_full_face line 1010
  83. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.fullFace_card line 1016
  84. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.fullFace_of_card line 1032
  85. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.exists_flag_stages line 1045
  86. theorem OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.exists_flag_from_face line 1056
  87. def OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.flagStabilizer line 1092
  88. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.mem_flagStabilizer line 1096
  89. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.flagStabilizer_good line 1101
  90. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.flagStabilizer_invariant line 1112
  91. theorem OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.chamber_transitive line 1125
  92. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.prefix_span_image line 1158
  93. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.mem_flag_iff_repr line 1168
  94. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.adapted_basis_not_mem_previous line 1183
  95. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.adapted_diagonal_ne_zero line 1194
  96. theorem OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.exists_normalized_adapted_basis line 1211
  97. def OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.Unitriangular line 1227
  98. theorem OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.exists_unitriangular_equiv line 1230
  99. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.suffix_span_image line 1275
  100. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.mem_opposite_flag_iff_repr line 1291
  101. theorem OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.unitriangular_stabilizer_trivial line 1304
  102. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.flagStabilizer_mem line 1326
  103. def OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.unipotentFlagStabilizer line 1332
  104. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.unitriangular_difference line 1353
  105. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.unitriangular_grading line 1361
  106. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.unipotent_unitriangular line 1376
  107. theorem OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.unipotent_transitive line 1384
  108. theorem OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.unipotent_stabilizer_trivial line 1393
  109. def OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.properIndex line 1409
  110. def OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.baseSpace line 1410
  111. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.baseSpace_rank line 1413
  112. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.baseSpace_injective line 1416
  113. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.opposed_of_opposite line 1423
  114. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.baseSpace_good line 1430
  115. def OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.baseSimplex line 1434
  116. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.baseSimplex_full line 1439
  117. def OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.vertexStabilizers line 1458
  118. def OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.cosetVertexMap line 1462
  119. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.cosetVertexMap_vertex line 1467
  120. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.cosetVertexMap_rank line 1472
  121. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.cosetVertexMap_injective line 1480
  122. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.unipotent_good line 1489
  123. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.cosetVertexMap_good line 1493
  124. theorem OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.cosetFace_opposed line 1499
  125. theorem OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.opposedFace_coset line 1519
  126. theorem OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.cosetFace_iff line 1544
  127. def OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.basisFlag line 1562
  128. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.basisFlag_adapted line 1576
  129. def OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.tailIndex line 1582
  130. def OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.oppositeBasisFlag line 1584
  131. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.oppositeBasisFlag_adapted line 1606
  132. theorem OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.basisFlags_opposite line 1615
  133. lemma OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.unitriangular_flag line 1631
  134. theorem OAI.CoboundaryExpanders.SphericalOpposition.CompleteFlag.mem_unipotent_iff_unitriangular line 1650