OAI/GroupTheory/BooneHigman/SteinbergPresentation.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

Finite free-algebra Steinberg presentations and transport to finitely presented algebras.

  1. theorem OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.commute_commutator line 17
  2. theorem OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.associate_commutator line 22

    Source documentation

    The rank-four commutator calculus needed for the finite free-algebra presentation.

    theorem associate_commutator (a b c : Q) (hac : Commute a c)
    (hde : Commute ⁅a,b⁆ ⁅b,c⁆) (hec : Commute ⁅b,c⁆ c) :
    ⁅⁅a,b⁆,c⁆=⁅a,⁅b,c⁆⁆ := by
…
  3. theorem OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.commutator_square line 37

    Source documentation

    A central commutator of an involution is itself an involution.

    theorem commutator_square (a b : Q) (ha : a*a=1) (hc : Commute a ⁅a,b⁆) :
    ⁅a,b⁆*⁅a,b⁆=1 := by
…
  4. structure OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem line 48
  5. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.freshIndex line 56
  6. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.fresh5 line 61
  7. def OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.middle line 72
  8. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.middle_ne_left line 73
  9. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.middle_ne_right line 74
  10. def OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.word line 79
  11. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.word_nil line 84
  12. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.word_singleton line 85
  13. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.word_diagonal line 86
  14. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.word_cons line 91
  15. structure OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.Valid line 99

    Source documentation

    Finite-length invariants for the simultaneous noncommutative-root induction. The distant invariant bounds the maximum, not the sum, of the two word lengths.

    structure Valid (n : ℕ) : Prop where
…
  16. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.valid_zero line 108
  17. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.factor_step line 126
  18. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.short_word line 160
  19. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.word_option line 168
  20. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.valid_one line 171
  21. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.distant_step_short line 194
  22. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.distant_step line 212
  23. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.chain_step line 247
  24. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.square_step line 300
  25. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.valid_succ line 319
  26. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.valid line 325
  27. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.word_distant line 333
  28. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.word_chain line 337
  29. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.word_square line 341
  30. abbrev OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.Polynomial line 349
  31. def OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.rootSubgroup line 351
  32. instance OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.root_commutative line 352
  33. def OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.wordInRoot line 359
  34. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.scalar_cases line 362
  35. def OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.wordScalar line 367
  36. def OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.polynomialAdd line 377
  37. def OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.polynomial line 381
  38. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.polynomial_zero line 384
  39. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.polynomial_add line 387
  40. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.polynomial_single line 391
  41. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.polynomial_induction line 395
  42. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.polynomial_distant line 404
  43. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.polynomial_diagonal line 415
  44. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.polynomial_chain_add_left line 421
  45. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.polynomial_chain_add_right line 432
  46. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.polynomial_chain line 443
  47. abbrev OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallGenerator line 467
  48. def OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.freeSmall line 469
  49. def OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.smallRelator line 471
  50. def OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.smallRelations line 480
  51. abbrev OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.Presentation line 484
  52. instance OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.(instance at line 485) line 485
  53. def OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.presentSmall line 489
  54. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.present_relator line 490
  55. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.present_diagonal line 494
  56. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.present_square line 496
  57. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.present_distant line 498
  58. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.present_unit_left line 502
  59. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.present_unit_right line 506
  60. def OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.presentSystem line 511
  61. def OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.fromPresentation line 520
  62. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.fromPresentation_small line 532
  63. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.map_word line 545
  64. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.SmallSystem.map_polynomial line 559
  65. def OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.polynomialBackward line 567
  66. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.polynomialBackward_root line 582
  67. def OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.actualSmall line 592
  68. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.actualSmall_diagonal line 595
  69. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.actualSmall_off line 596
  70. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.actualSmall_square line 600
  71. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.actualSmall_distant line 606
  72. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.actualSmall_unit_left line 615
  73. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.actualSmall_unit_right line 621
  74. def OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.actualSystem line 627
  75. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.actual_word line 635
  76. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.actual_polynomial line 652
  77. def OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.polynomialForward line 661
  78. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.polynomial_forward_backward line 664
  79. lemma OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.polynomial_backward_forward line 673
  80. def OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.polynomialEquivalence line 687
  81. instance OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.polynomial_finitelyPresented line 693
  82. instance OAI.FiniteAlgebraicEnvelopes.SteinbergFiniteFree.freeAlgebra_finitelyPresented line 698

    Source documentation

    A finite rank-six presentation for the noncommutative free algebra over F₂. All long-word and additive Steinberg relations follow from the finite small-root relations.

    instance freeAlgebra_finitelyPresented [Finite A] :
    Group.IsFinitelyPresented (Steinberg.Group (Fin 6) (FreeAlgebra (ZMod 2) A)) :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.Group