OAI/GroupTheory/BooneHigman/FinitePresentation.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Seed line 24

   Source documentation

   An actual finitely presented source for the finite-table group. The two copies of Γ map to the root and one half-cube, and the free factor maps to the four explicit untwisted generators. Its quotient kernel is a construction, not an extra main-theorem hypothesis.

   def Seed := Monoid.Coprod (Monoid.Coprod Γ Γ)
   …

2. instance OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.(instance at line 27) line 27
3. instance OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.seed_finitelyPresented line 31
4. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.evaluation line 36
5. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.evaluation_range line 41
6. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.evaluation_surjective line 51
7. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.quotientEquivalence line 58

   Source documentation

   The exact quotient already known to be the desired concrete simple group. Only finite normal generation of this explicitly defined kernel remains for finite presentation; neither that property nor a main theorem is asserted here.

   def quotientEquivalence [MulAction.IsPretransitive Γ X] :
       (Seed (Γ:=Γ) x ⧸ (evaluation x).ker) ≃* group (Γ:=Γ) (X:=X) :=
   …

   Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Seed, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.evaluation, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.group

8. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.half_copies_commute line 70
9. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.embedding_eq_diagonal_of_fixed line 89
10. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.rootWord line 102
11. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.halfWord line 103
12. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.flipWord line 105
13. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.rightWord line 108
14. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.evaluation_rootWord line 111
15. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.evaluation_halfWord line 113
16. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.evaluation_flipWord line 116
17. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.evaluation_rightWord line 118
18. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.commutingWord line 125

    Source documentation

    The commutation relator for the two different halves.

    def commutingWord (g h : Γ) : Seed (Γ:=Γ) x :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Seed

19. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.fixedWord line 129

    Source documentation

    A point-stabilizer relation: its root copy equals its two half-copies.

    def fixedWord (g : MulAction.stabilizer Γ x) : Seed (Γ:=Γ) x :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Seed

20. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.evaluation_commutingWord line 132
21. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.evaluation_fixedWord line 137
22. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.finiteRelations line 145

    Source documentation

    Two finite families of genuine evaluation-kernel relations. Completeness of these (plus the necessary tree-interchange and V relations) is NOT asserted.

    def finiteRelations (s : Finset Γ) (t : Finset (MulAction.stabilizer Γ x)) :
        Finset (Seed (Γ:=Γ) x) :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Seed

23. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.finiteRelations_mem_ker line 149
24. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.finiteRelations_closure_le_ker line 157
25. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.commute_homs_of_generators line 169
26. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.relationKernel line 191
27. instance OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.(instance at line 193) line 193
28. abbrev OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.RelationQuotient line 194
29. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.projection line 196
30. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.projectedRoot line 199
31. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.projectedHalf line 200
32. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.projectedRight line 201
33. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.projection_rel line 203
34. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.projected_commute line 207
35. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.projected_commute_all line 223
36. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.projectedDiagonal line 228
37. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.projected_fixed line 235
38. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.projected_fixed_all line 244
39. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.commutingWord_mem_relationKernel line 254
40. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.fixedWord_mem_relationKernel line 264
41. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.labelRelations line 285

    Source documentation

    The two universal label families. Other finite-table relations are not included here: in particular this is not asserted to be the evaluation kernel.

    def labelRelations : Set (Seed (Γ:=Γ) x) :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Seed

42. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.labelRelations_mem_ker line 289
43. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.finiteRelations_subset_labelRelations line 295
44. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.labelRelations_normalClosure line 306

    Source documentation

    All the infinitely many disjoint half-copy commutators and point-stabilizer splitting relations follow from their values on finite generating sets.

    lemma labelRelations_normalClosure (s : Finset Γ)
        (t : Finset (MulAction.stabilizer Γ x))
        (hs : Subgroup.closure (s : Set Γ)=⊤)
        (ht : Subgroup.closure (t : Set (MulAction.stabilizer Γ x))=⊤) :
        Subgroup.normalClosure (labelRelations x)=relationKernel x s t := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.labelRelations, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.relationKernel

45. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.labelRelations_finitelyNormallyGenerated line 318
46. abbrev OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.LabelQuotient line 329

    Source documentation

    A genuine finitely presented intermediate quotient. The still-missing relations cannot be discarded: this quotient is not identified with the finite-table group.

    abbrev LabelQuotient := Seed (Γ:=Γ) x ⧸ Subgroup.normalClosure (labelRelations (Γ:=Γ) x)

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Seed, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.labelRelations

47. instance OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.labelQuotient_finitelyPresented line 331
48. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.labelEvaluation line 336
49. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.labelEvaluation_surjective line 340
50. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.untwistedSum line 357

    Source documentation

    Detect the missing untwisted relators by an actual abelian quotient of the partially presented group. This is a diagnostic, not the desired endpoint.

    def untwistedSum : Seed (Γ:=Γ) x →* Multiplicative ℤ :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Seed

51. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.untwistedSum_root line 361
52. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.untwistedSum_half line 362
53. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.untwistedSum_flip line 363
54. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.untwistedSum_right line 365
55. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.labelRelations_mem_untwistedSum_ker line 369
56. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.flip_mul_self line 377
57. theorem OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.labelRelations_strictly_incomplete line 388

    Source documentation

    An explicit genuine table relation that is NOT a consequence of the two finite label families, even after using every acting-group and stabilizer element.

    theorem labelRelations_strictly_incomplete :
        (flipWord (Γ:=Γ) x)^2∈(evaluation (Γ:=Γ) x).ker ∧
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.flipWord, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.evaluation

58. def OAI.FiniteAlgebraicEnvelopes.FiniteLocalizationClosure.discrepancy line 412

    Source documentation

    The discrepancy between twice-localizing and conjugating a localization.

    def discrepancy (g : K) : K := f (f g) * (a * f g * a⁻¹)⁻¹

59. def OAI.FiniteAlgebraicEnvelopes.FiniteLocalizationClosure.baseRelations line 414
60. def OAI.FiniteAlgebraicEnvelopes.FiniteLocalizationClosure.relations line 415
61. def OAI.FiniteAlgebraicEnvelopes.FiniteLocalizationClosure.kernel line 417
62. instance OAI.FiniteAlgebraicEnvelopes.FiniteLocalizationClosure.(instance at line 418) line 418
63. abbrev OAI.FiniteAlgebraicEnvelopes.FiniteLocalizationClosure.Quotient line 419
64. def OAI.FiniteAlgebraicEnvelopes.FiniteLocalizationClosure.project line 421
65. lemma OAI.FiniteAlgebraicEnvelopes.FiniteLocalizationClosure.project_base line 423
66. lemma OAI.FiniteAlgebraicEnvelopes.FiniteLocalizationClosure.project_local_base line 427
67. lemma OAI.FiniteAlgebraicEnvelopes.FiniteLocalizationClosure.twice_eq_conjugate line 434
68. lemma OAI.FiniteAlgebraicEnvelopes.FiniteLocalizationClosure.kernel_stable line 449

    Source documentation

    Adding a finite set of relations, their first localizations, and the finite self-similarity checks suffices to make the entire normal closure stable under f. No infinitely iterated family is silently assumed finite.

    lemma kernel_stable : kernel f a s r ≤ (kernel f a s r).comap f := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.FiniteLocalizationClosure.kernel

69. def OAI.FiniteAlgebraicEnvelopes.FiniteLocalizationClosure.localization line 461
70. lemma OAI.FiniteAlgebraicEnvelopes.FiniteLocalizationClosure.localization_project line 464
71. lemma OAI.FiniteAlgebraicEnvelopes.FiniteLocalizationClosure.localizations_in_kernel line 467
72. lemma OAI.FiniteAlgebraicEnvelopes.FiniteLocalizationClosure.kernel_finitelyNormallyGenerated line 476
73. instance OAI.FiniteAlgebraicEnvelopes.FiniteLocalizationClosure.quotient_finitelyPresented line 480
74. lemma OAI.FiniteAlgebraicEnvelopes.FiniteLocalizationClosure.relations_valid line 492
75. def OAI.FiniteAlgebraicEnvelopes.FiniteLocalizationClosure.evaluate line 508
76. lemma OAI.FiniteAlgebraicEnvelopes.FiniteLocalizationClosure.evaluate_surjective line 512
77. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.generatorWord line 528
78. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.evaluation_generatorWord line 531
79. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.associatorWord line 534
80. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.evaluation_associatorWord line 537
81. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.localize_twice line 540
82. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.localizationSeed line 550

    Source documentation

    An actual lift of prefix localization to the presentation seed. It respects both Γ factors as homomorphisms; only the free factor uses chosen preimages.

    def localizationSeed : Seed (Γ:=Γ) x →* Seed (Γ:=Γ) x :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Seed

83. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.localizationSeed_correct line 557
84. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.evaluation_localizationSeed line 580
85. abbrev OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.LocalQuotient line 586

    Source documentation

    The finite self-similar closure of any given finite family of actual table relations. Completeness of a particular family still has to be proved.

    abbrev LocalQuotient (s r : Finset (Seed (Γ:=Γ) x)) :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Seed

86. instance OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.localQuotient_finitelyPresented line 589
87. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.localEvaluation line 593
88. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.localEvaluation_surjective line 600