OAI/GroupTheory/BooneHigman/AlgebraPresentations.lean

GitHub source file

100 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.FiniteAlgebraicEnvelopes.TensorPresentation.F line 15
2. def OAI.FiniteAlgebraicEnvelopes.TensorPresentation.inLeft line 16
3. def OAI.FiniteAlgebraicEnvelopes.TensorPresentation.inRight line 17
4. inductive OAI.FiniteAlgebraicEnvelopes.TensorPresentation.Rel line 22
5. abbrev OAI.FiniteAlgebraicEnvelopes.TensorPresentation.P line 28
6. def OAI.FiniteAlgebraicEnvelopes.TensorPresentation.q line 29
7. def OAI.FiniteAlgebraicEnvelopes.TensorPresentation.leftFree line 31
8. def OAI.FiniteAlgebraicEnvelopes.TensorPresentation.rightFree line 32
9. def OAI.FiniteAlgebraicEnvelopes.TensorPresentation.left line 34
10. def OAI.FiniteAlgebraicEnvelopes.TensorPresentation.right line 37
11. theorem OAI.FiniteAlgebraicEnvelopes.TensorPresentation.left_mk line 41
12. theorem OAI.FiniteAlgebraicEnvelopes.TensorPresentation.right_mk line 43
13. theorem OAI.FiniteAlgebraicEnvelopes.TensorPresentation.leftFree_ι line 46
14. theorem OAI.FiniteAlgebraicEnvelopes.TensorPresentation.rightFree_ι line 48
15. theorem OAI.FiniteAlgebraicEnvelopes.TensorPresentation.free_commute line 51
16. theorem OAI.FiniteAlgebraicEnvelopes.TensorPresentation.quotient_commute line 67
17. def OAI.FiniteAlgebraicEnvelopes.TensorPresentation.fromTensor line 73
18. def OAI.FiniteAlgebraicEnvelopes.TensorPresentation.toTensorFree line 76
19. theorem OAI.FiniteAlgebraicEnvelopes.TensorPresentation.toTensorFree_left line 81
20. theorem OAI.FiniteAlgebraicEnvelopes.TensorPresentation.toTensorFree_right line 87
21. def OAI.FiniteAlgebraicEnvelopes.TensorPresentation.toTensor line 93
22. theorem OAI.FiniteAlgebraicEnvelopes.TensorPresentation.toTensor_q line 107
23. theorem OAI.FiniteAlgebraicEnvelopes.TensorPresentation.toTensor_left line 110
24. theorem OAI.FiniteAlgebraicEnvelopes.TensorPresentation.toTensor_right line 117
25. theorem OAI.FiniteAlgebraicEnvelopes.TensorPresentation.to_from line 124
26. theorem OAI.FiniteAlgebraicEnvelopes.TensorPresentation.from_to line 129
27. def OAI.FiniteAlgebraicEnvelopes.TensorPresentation.equivalence line 143
28. theorem OAI.FiniteAlgebraicEnvelopes.TensorPresentation.rel_finite line 146
29. def OAI.FiniteAlgebraicEnvelopes.OppositePresentation.reverse line 167
30. def OAI.FiniteAlgebraicEnvelopes.OppositePresentation.unreverse line 170
31. theorem OAI.FiniteAlgebraicEnvelopes.OppositePresentation.reverse_ι line 172
32. theorem OAI.FiniteAlgebraicEnvelopes.OppositePresentation.unreverse_op line 174
33. theorem OAI.FiniteAlgebraicEnvelopes.OppositePresentation.unreverse_reverse line 176
34. theorem OAI.FiniteAlgebraicEnvelopes.OppositePresentation.reverse_unreverse line 181
35. def OAI.FiniteAlgebraicEnvelopes.OppositePresentation.freeEquivalence line 188
36. def OAI.FiniteAlgebraicEnvelopes.OppositePresentation.opRel line 194
37. def OAI.FiniteAlgebraicEnvelopes.OppositePresentation.quotientToOp line 196
38. def OAI.FiniteAlgebraicEnvelopes.OppositePresentation.quotientFromOpAux line 201
39. def OAI.FiniteAlgebraicEnvelopes.OppositePresentation.quotientFromOp line 206
40. theorem OAI.FiniteAlgebraicEnvelopes.OppositePresentation.quotientToOp_mk line 209
41. theorem OAI.FiniteAlgebraicEnvelopes.OppositePresentation.quotientFromOp_mk line 212
42. theorem OAI.FiniteAlgebraicEnvelopes.OppositePresentation.quotientToFrom line 218
43. theorem OAI.FiniteAlgebraicEnvelopes.OppositePresentation.quotientFromTo line 225
44. def OAI.FiniteAlgebraicEnvelopes.OppositePresentation.quotientEquivalence line 231
45. theorem OAI.FiniteAlgebraicEnvelopes.OppositePresentation.opRel_finite line 235
46. def OAI.FiniteAlgebraicEnvelopes.OppositePresentation.freeRel line 243
47. def OAI.FiniteAlgebraicEnvelopes.OppositePresentation.presentation line 245
48. theorem OAI.FiniteAlgebraicEnvelopes.OppositePresentation.freeRel_finite line 248
49. def OAI.FiniteAlgebraicEnvelopes.AlgebraGenerators.tensorGenerators line 263
50. theorem OAI.FiniteAlgebraicEnvelopes.AlgebraGenerators.tensorGenerators_finite line 266
51. theorem OAI.FiniteAlgebraicEnvelopes.AlgebraGenerators.tensorGenerators_generate line 269
52. theorem OAI.FiniteAlgebraicEnvelopes.AlgebraGenerators.oppositeGenerators_generate line 297
53. def OAI.FiniteAlgebraicEnvelopes.AlgebraGenerators.envelopingGenerators line 312
54. theorem OAI.FiniteAlgebraicEnvelopes.AlgebraGenerators.envelopingGenerators_finite line 315
55. theorem OAI.FiniteAlgebraicEnvelopes.AlgebraGenerators.envelopingGenerators_generate line 318
56. def OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.linearLimitEquivalence line 330
57. theorem OAI.FiniteAlgebraicEnvelopes.ContractedPresentation.monoidBasis_injective_nonzero line 339
58. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.groupAlgebraEmbedding line 356

    Source documentation

    Input units in the simple algebra, whose internal identity is preserved.

    def groupAlgebraEmbedding : G →* SmallAlgebra s h k :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.SmallAlgebra

59. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.groupAlgebraEmbedding_injective line 359
60. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.groupAlgebraUnits line 365
61. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.groupAlgebraUnits_injective line 367
62. theorem OAI.FiniteAlgebraicEnvelopes.Unitize.support_left line 378
63. theorem OAI.FiniteAlgebraicEnvelopes.Unitize.support_right line 379
64. def OAI.FiniteAlgebraicEnvelopes.Unitize.hom line 382

    Source documentation

    Extend a group represented in a nonunital corner to units of the ambient ring.

    def hom : G →* B where
    …

65. theorem OAI.FiniteAlgebraicEnvelopes.Unitize.hom_apply line 392
66. theorem OAI.FiniteAlgebraicEnvelopes.Unitize.hom_injective line 394
67. def OAI.FiniteAlgebraicEnvelopes.Unitize.unitsHom line 398
68. theorem OAI.FiniteAlgebraicEnvelopes.Unitize.unitsHom_injective line 400
69. def OAI.FiniteAlgebraicEnvelopes.Enveloping.includeLeft line 410
70. theorem OAI.FiniteAlgebraicEnvelopes.Enveloping.includeLeft_apply line 412
71. theorem OAI.FiniteAlgebraicEnvelopes.Enveloping.eval_includeLeft line 414
72. theorem OAI.FiniteAlgebraicEnvelopes.Enveloping.includeLeft_injective line 417
73. def OAI.FiniteAlgebraicEnvelopes.Enveloping.unitsInclude line 420
74. theorem OAI.FiniteAlgebraicEnvelopes.Enveloping.unitsInclude_injective line 422
75. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.ambientUnits line 437
76. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.ambientUnits_injective line 440
77. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.coefficientUnits line 443
78. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.coefficientUnits_injective line 446
79. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.ringPsi_injective line 455
80. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.linearTransition line 457
81. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.linearTransition_injective line 459
82. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.linearLimitEquivalence line 462
83. def OAI.FiniteAlgebraicEnvelopes.HasKernelRing line 470

    Source documentation

    A construction interface; every field is discharged below from the source algebra.

    def HasKernelRing (H : Type*) [Group H] : Prop :=
    …

84. theorem OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.kernelRingPackage line 482
85. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.kernelRing line 493
86. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.ringGenerators line 510
87. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.ringGenerators_finite line 514
88. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.ringGenerators_generate line 518
89. instance OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.steinberg_finitelyGenerated line 521
90. abbrev OAI.FiniteAlgebraicEnvelopes.EnvelopingPresentation.Generators line 531
91. def OAI.FiniteAlgebraicEnvelopes.EnvelopingPresentation.Rel line 532
92. def OAI.FiniteAlgebraicEnvelopes.EnvelopingPresentation.equivalence line 535
93. theorem OAI.FiniteAlgebraicEnvelopes.EnvelopingPresentation.rel_finite line 540
94. def OAI.FiniteAlgebraicEnvelopes.EnvelopingPresentation.ofPresentation line 548
95. def OAI.FiniteAlgebraicEnvelopes.Steinberg.coefficientEquiv line 556
96. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.CoefficientGenerators line 587
97. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.CoefficientRelations line 589
98. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.coefficientPresentation line 591
99. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.coefficientRelations_finite line 594
100. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.steinberg_finitePresentation_of_free line 601

     Source documentation

     Finite-presentation reduction to the finite free algebra case.

     theorem steinberg_finitePresentation_of_free
         [Group.IsFinitelyPresented (Steinberg.Group (Fin 6) (FreeAlgebra k (CoefficientGenerators s h)))] :
         Group.IsFinitelyPresented (Steinberg.Group (Fin 6) (R s h k)) := by
     …

     Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.Group, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.CoefficientGenerators, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.R