OAI/GroupTheory/ArtinCAT0/Embeddings.lean

GitHub source file

131 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ArtinCAT0.AmalgamTools.reduced_append line 11
  2. lemma OAI.ArtinCAT0.AmalgamTools.reduced_singleton line 16
  3. lemma OAI.ArtinCAT0.AmalgamTools.reduced_inv line 20
  4. lemma OAI.ArtinCAT0.AmalgamTools.reduced_not_factor line 29
  5. lemma OAI.ArtinCAT0.AmalgamTools.conjugate_certificate line 56

    Source documentation

    A reduced word is either a single-factor element, or conjugating an element whose factor-conjugacy class avoids the base produces a reduced word still containing a letter from another factor.

    lemma conjugate_certificate {k i j : ι} (w : NeWord G i j) (hw : Reduced φ w.toWord) :
    (∃ b : G k, ofCoprodI (φ:=φ) w.prod=PushoutI.of k b ∧ i=k ∧ j=k) ∨
…
  6. lemma OAI.ArtinCAT0.AmalgamTools.normal_reduced line 103
  7. theorem OAI.ArtinCAT0.AmalgamTools.centralizer_in_factor line 112

    Source documentation

    Centralizers cannot escape the factor when the factor-conjugacy class of the element misses the amalgamating subgroup.

    theorem centralizer_in_factor (hφ : ∀ i, Function.Injective (φ i)) (k : ι) (q : G k)
    (hq : ∀ b : G k, b*q*b⁻¹∉(φ k).range)
    (g : PushoutI φ) (hg : Commute g (PushoutI.of k q)) : g∈(PushoutI.of k).range := by
…
  8. def OAI.ArtinCAT0.BinaryAmalgam.Family line 159
  9. instance OAI.ArtinCAT0.BinaryAmalgam.familyGroup line 162
  10. def OAI.ArtinCAT0.BinaryAmalgam.diagram line 165
  11. abbrev OAI.ArtinCAT0.BinaryAmalgam.GroupOf line 168
  12. def OAI.ArtinCAT0.BinaryAmalgam.left line 169
  13. def OAI.ArtinCAT0.BinaryAmalgam.right line 170
  14. lemma OAI.ArtinCAT0.BinaryAmalgam.agree line 171
  15. lemma OAI.ArtinCAT0.BinaryAmalgam.diagram_injective line 173
  16. lemma OAI.ArtinCAT0.BinaryAmalgam.left_injective line 177
  17. lemma OAI.ArtinCAT0.BinaryAmalgam.right_injective line 180
  18. def OAI.ArtinCAT0.BinaryAmalgam.targets line 184
  19. def OAI.ArtinCAT0.BinaryAmalgam.lift line 188
  20. lemma OAI.ArtinCAT0.BinaryAmalgam.lift_left line 191
  21. lemma OAI.ArtinCAT0.BinaryAmalgam.lift_right line 194
  22. lemma OAI.ArtinCAT0.BinaryAmalgam.centralizer_right line 198
  23. abbrev OAI.ArtinCAT0.FreeTwo.Cyclic line 207
  24. def OAI.ArtinCAT0.FreeTwo.maps line 208
  25. abbrev OAI.ArtinCAT0.FreeTwo.GroupOf line 209
  26. def OAI.ArtinCAT0.FreeTwo.gen line 210
  27. lemma OAI.ArtinCAT0.FreeTwo.maps_injective line 211
  28. lemma OAI.ArtinCAT0.FreeTwo.gen_ne_one line 212
  29. def OAI.ArtinCAT0.FreeTwo.lift line 218
  30. lemma OAI.ArtinCAT0.FreeTwo.lift_gen line 223
  31. lemma OAI.ArtinCAT0.FreeTwo.common_centralizer line 226
  32. lemma OAI.ArtinCAT0.blockLetter_injective line 246
  33. lemma OAI.ArtinCAT0.blockLetter_private line 251
  34. lemma OAI.ArtinCAT0.blockLetter_nonsentinel line 257
  35. lemma OAI.ArtinCAT0.adjacent_symm line 262
  36. lemma OAI.ArtinCAT0.distant_symm line 265
  37. lemma OAI.ArtinCAT0.sentinel_symm line 268
  38. lemma OAI.ArtinCAT0.adjacent_not_distant line 270
  39. lemma OAI.ArtinCAT0.sentinel_not_adjacent line 285
  40. lemma OAI.ArtinCAT0.explicitMatrix_symmetric line 291
  41. lemma OAI.ArtinCAT0.explicitMatrix_diagonal line 297
  42. lemma OAI.ArtinCAT0.explicitMatrix_values line 300
  43. lemma OAI.ArtinCAT0.matrix_block_adjacent line 306
  44. lemma OAI.ArtinCAT0.matrix_block_distant line 316
  45. lemma OAI.ArtinCAT0.matrix_sentinel line 327
  46. abbrev OAI.ArtinCAT0.MainGroup line 331
  47. abbrev OAI.ArtinCAT0.mainGen line 332
  48. lemma OAI.ArtinCAT0.artin_braid line 334
  49. lemma OAI.ArtinCAT0.artin_commute line 340
  50. def OAI.ArtinCAT0.mainLift line 348
  51. lemma OAI.ArtinCAT0.mainLift_gen line 367
  52. abbrev OAI.ArtinCAT0.Assembly.inc line 376
  53. abbrev OAI.ArtinCAT0.Assembly.A₁ line 377
  54. def OAI.ArtinCAT0.Assembly.t₁ line 378
  55. abbrev OAI.ArtinCAT0.Assembly.A₂ line 379
  56. def OAI.ArtinCAT0.Assembly.t₂ line 380
  57. abbrev OAI.ArtinCAT0.Assembly.A₃ line 381
  58. def OAI.ArtinCAT0.Assembly.t₃ line 382
  59. lemma OAI.ArtinCAT0.Assembly.inc_injective line 384
  60. lemma OAI.ArtinCAT0.Assembly.t₁_injective line 385
  61. lemma OAI.ArtinCAT0.Assembly.t₂_injective line 386
  62. lemma OAI.ArtinCAT0.Assembly.t₃_injective line 391
  63. def OAI.ArtinCAT0.Assembly.block₀ line 397
  64. def OAI.ArtinCAT0.Assembly.block₁ line 400
  65. def OAI.ArtinCAT0.Assembly.block₂ line 402
  66. def OAI.ArtinCAT0.Assembly.block line 404
  67. lemma OAI.ArtinCAT0.Assembly.block_agree line 405
  68. abbrev OAI.ArtinCAT0.Assembly.Product line 416
  69. def OAI.ArtinCAT0.Assembly.productT line 417
  70. lemma OAI.ArtinCAT0.Assembly.productT_injective line 418
  71. abbrev OAI.ArtinCAT0.Assembly.Model line 421
  72. def OAI.ArtinCAT0.Assembly.triangle line 422
  73. def OAI.ArtinCAT0.Assembly.braidBlock line 423
  74. def OAI.ArtinCAT0.Assembly.sentinel line 424
  75. lemma OAI.ArtinCAT0.Assembly.triangle_injective line 425
  76. lemma OAI.ArtinCAT0.Assembly.triangle_eq_right line 427
  77. lemma OAI.ArtinCAT0.Assembly.braidBlock_agree line 428
  78. lemma OAI.ArtinCAT0.Assembly.product_conjugate_not_base line 431
  79. lemma OAI.ArtinCAT0.Assembly.common_centralizer line 440
  80. def OAI.ArtinCAT0.Assembly.corner line 452
  81. lemma OAI.ArtinCAT0.Assembly.blockLetter_zero line 453
  82. lemma OAI.ArtinCAT0.Assembly.blockLetter_one line 455
  83. lemma OAI.ArtinCAT0.Assembly.braidBlock_zero line 459
  84. lemma OAI.ArtinCAT0.Assembly.braidBlock_one line 462
  85. def OAI.ArtinCAT0.Assembly.letter line 466
  86. lemma OAI.ArtinCAT0.Assembly.letter_corner line 471
  87. lemma OAI.ArtinCAT0.Assembly.letter_three line 473
  88. lemma OAI.ArtinCAT0.Assembly.letter_four line 474
  89. lemma OAI.ArtinCAT0.Assembly.letter_block line 475
  90. lemma OAI.ArtinCAT0.Assembly.letter_braid line 493
  91. lemma OAI.ArtinCAT0.Assembly.triangle_sentinel_commute line 503
  92. lemma OAI.ArtinCAT0.Assembly.letter_commute line 510
  93. def OAI.ArtinCAT0.Assembly.toModel line 532
  94. lemma OAI.ArtinCAT0.Assembly.toModel_gen line 533
  95. def OAI.ArtinCAT0.Assembly.triangleMain line 535
  96. lemma OAI.ArtinCAT0.Assembly.triangleMain_gen line 540
  97. def OAI.ArtinCAT0.Assembly.blockMain line 543
  98. lemma OAI.ArtinCAT0.Assembly.blockMain_gen line 546
  99. lemma OAI.ArtinCAT0.Assembly.blockMain_agree line 548
  100. def OAI.ArtinCAT0.Assembly.sentinelMain line 553
  101. lemma OAI.ArtinCAT0.Assembly.triangleMain_commute line 554
  102. def OAI.ArtinCAT0.Assembly.freeMain line 565
  103. lemma OAI.ArtinCAT0.Assembly.freeMain_gen line 566
  104. lemma OAI.ArtinCAT0.Assembly.factors_commute line 567
  105. def OAI.ArtinCAT0.Assembly.productMain line 576
  106. lemma OAI.ArtinCAT0.Assembly.productMain_apply line 577
  107. lemma OAI.ArtinCAT0.Assembly.productMain_triangle line 579
  108. def OAI.ArtinCAT0.Assembly.back₁ line 584
  109. lemma OAI.ArtinCAT0.Assembly.back₁_triangle line 585
  110. def OAI.ArtinCAT0.Assembly.back₂ line 589
  111. lemma OAI.ArtinCAT0.Assembly.back₂_triangle line 592
  112. def OAI.ArtinCAT0.Assembly.back₃ line 598
  113. lemma OAI.ArtinCAT0.Assembly.back₃_triangle line 601
  114. lemma OAI.ArtinCAT0.Assembly.back₃_block line 607
  115. def OAI.ArtinCAT0.Assembly.fromModel line 612
  116. lemma OAI.ArtinCAT0.Assembly.fromModel_triangle line 614
  117. lemma OAI.ArtinCAT0.Assembly.fromModel_block line 619
  118. lemma OAI.ArtinCAT0.Assembly.fromModel_sentinel line 624
  119. lemma OAI.ArtinCAT0.Assembly.letter_cover line 627
  120. lemma OAI.ArtinCAT0.Assembly.fromModel_letter line 644
  121. lemma OAI.ArtinCAT0.Assembly.fromModel_toModel line 651
  122. lemma OAI.ArtinCAT0.Assembly.toModel_injective line 656
  123. lemma OAI.ArtinCAT0.Assembly.toModel_triangleMain line 660
  124. lemma OAI.ArtinCAT0.Assembly.triangleMain_injective line 665
  125. lemma OAI.ArtinCAT0.Assembly.toModel_sentinelMain line 669
  126. lemma OAI.ArtinCAT0.Assembly.main_common_centralizer line 671
  127. def OAI.ArtinCAT0.Assembly.triangleCentralizer line 681
  128. lemma OAI.ArtinCAT0.Assembly.triangleCentralizer_bijective line 683
  129. lemma OAI.ArtinCAT0.geometric_compHom line 695
  130. lemma OAI.ArtinCAT0.stableLength_compHom line 710
  131. lemma OAI.ArtinCAT0.generator_square_positive line 716