OAI/GroupTheory/BooneHigman/DecoratedPresentation.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FiniteAlgebraicEnvelopes.FiniteLocalizationClosure.baseRelations_mono line 18
2. lemma OAI.FiniteAlgebraicEnvelopes.FiniteLocalizationClosure.relations_mono line 21
3. lemma OAI.FiniteAlgebraicEnvelopes.FiniteLocalizationClosure.kernel_mono line 25
4. def OAI.FiniteAlgebraicEnvelopes.FiniteLocalizationClosure.quotientMap line 28
5. lemma OAI.FiniteAlgebraicEnvelopes.FiniteLocalizationClosure.quotientMap_project line 31
6. lemma OAI.FiniteAlgebraicEnvelopes.FiniteLocalizationClosure.quotientMap_surjective line 34
7. lemma OAI.FiniteAlgebraicEnvelopes.FiniteLocalizationClosure.quotientMap_localization line 39
8. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedRelations line 57

   Source documentation

   Finite structural laws together with the point stabilizer laws.

   def decoratedRelations : Finset (Seed (Γ:=Γ) x) :=
   …

   Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Seed

9. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedRelations_valid line 60
10. abbrev OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.DecoratedQuotient line 67
11. instance OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedQuotient_finitelyPresented line 69
12. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedEvaluation line 72
13. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedEvaluation_surjective line 75
14. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedProject line 78
15. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralToDecorated line 81
16. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralToDecorated_project line 84
17. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedRoot line 87
18. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedHalf line 88
19. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedRight line 89
20. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decorated_commute line 94
21. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedDiagonal line 100
22. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decorated_fixed line 107
23. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decorated_fixed_all line 117
24. lemma OAI.FiniteAlgebraicEnvelopes.StabilizerCocycle.equal_of_smul_eq line 140

    Source documentation

    The difference of two copies of the acting group descends to its orbit when those copies agree on the point stabilizer.

    lemma equal_of_smul_eq {g h : Γ} (he : g • x=h • x) :
        R g * (D g)⁻¹=R h * (D h)⁻¹ := by
    …

25. def OAI.FiniteAlgebraicEnvelopes.StabilizerCocycle.value line 158

    Source documentation

    The orbit-indexed difference; the selected representative is immaterial.

    def value (y : X) : H :=
    …

26. lemma OAI.FiniteAlgebraicEnvelopes.StabilizerCocycle.value_smul line 162
27. lemma OAI.FiniteAlgebraicEnvelopes.StabilizerCocycle.value_base line 165
28. lemma OAI.FiniteAlgebraicEnvelopes.StabilizerCocycle.covariance line 169

    Source documentation

    Exact covariance of the orbit-indexed difference.

    lemma covariance (g : Γ) (y : X) :
        R g*value x R D y=value x R D (g • y)*D g := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.StabilizerCocycle.value

29. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedBaker line 192

    Source documentation

    A baker element defined inside the finitely presented quotient, before any injectivity or table-presentation completeness theorem.

    def decoratedBaker (y : X) : DecoratedQuotient x s t :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.DecoratedQuotient

30. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedBaker_smul line 196
31. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedBaker_base line 201
32. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedBaker_covariance line 206

    Source documentation

    The complete colour covariance family follows from the finite stabilizer relations. It is not imposed once for each point of the infinite set.

    lemma decoratedBaker_covariance (g : Γ) (y : X) :
        decoratedRoot x s t g*decoratedBaker x s t hs y=
          decoratedBaker x s t hs (g • y)*decoratedDiagonal x s t hs g :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedRoot, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedBaker, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedDiagonal

33. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedEvaluation_project line 212
34. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedEvaluation_diagonal line 216
35. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedEvaluation_baker line 225

    Source documentation

    The internally descended baker evaluates to the literal coordinate baker.

    lemma decoratedEvaluation_baker (y : X) :
        decoratedEvaluation x s t (decoratedBaker x s t hs y)=baker x y := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedEvaluation, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedBaker, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.baker

36. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedProject_surjective line 244
37. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralToDecorated_surjective line 247
38. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedLocalization line 250
39. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedRightLocalization line 253
40. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedLocalization_project line 257
41. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedRightLocalization_project line 261
42. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedLocalizations_commute line 269
43. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedTensor line 276
44. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedTensor_apply line 281
45. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedDiagonal_tensor line 285
46. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralToDecorated_localization line 289
47. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralToDecorated_rightLocalization line 294
48. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralToDecorated_tensor line 302
49. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedColourTensor line 309

    Source documentation

    A binary tensor at any colour, constructed internally from the descended baker.

    def decoratedColourTensor (y : X) : DecoratedQuotient (Γ:=Γ) x s t × DecoratedQuotient x s t →*
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.DecoratedQuotient

50. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedColourTensor_apply line 313
51. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedColourTensor_covariance line 322

    Source documentation

    The full label/split naturality law follows internally from the finite stabilizer relations, rather than being assumed as an infinite relator family.

    lemma decoratedColourTensor_covariance (g : Γ) (y : X) (a b : DecoratedQuotient (Γ:=Γ) x s t) :
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.DecoratedQuotient

52. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.bakerWord line 355
53. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.evaluation_bakerWord line 359
54. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.middleSwapWord line 367
55. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.middleSwapMove line 371
56. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.evaluation_middleSwapWord line 381
57. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.middleSwap_attach line 388
58. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.gridWord line 415
59. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.evaluation_gridWord line 418
60. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.gridWord_attach line 423
61. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.interchangeWord line 433

    Source documentation

    One coordinate-interchange relation, between the two literal grids.

    def interchangeWord (y z : X) : Seed (Γ:=Γ) x :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Seed

62. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.eq_of_doubleBit line 437
63. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.grid_interchange line 447
64. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.evaluation_interchangeWord line 460
65. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.halfAssociatorBinding line 475
66. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.halfFlipBinding line 479
67. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.evaluation_halfAssociatorBinding line 483
68. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.evaluation_halfFlipBinding line 487
69. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointRelations line 496

    Source documentation

    Explicit finite presentation candidate: structure, stabilizer, generator bindings, and one orbit representative of distinct-colour interchange. Its completeness is not built into this definition.

    def endpointRelations : Finset (Seed (Γ:=Γ) x) :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Seed

70. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointRelations_valid line 499
71. abbrev OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.EndpointQuotient line 512

    Source documentation

    A finite presentation with a surjection to the concrete simple table group.

    abbrev EndpointQuotient := LocalQuotient x s (endpointRelations x s t y)

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.LocalQuotient, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointRelations

72. instance OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointQuotient_finitelyPresented line 514
73. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointEvaluation line 517
74. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointEvaluation_surjective line 520
75. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointProject line 524
76. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedToEndpoint line 527
77. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedToEndpoint_project line 530
78. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointProject_rel line 533
79. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpoint_halfAssociatorBinding line 537
80. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpoint_halfFlipBinding line 547
81. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpoint_interchange line 557
82. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedGrid line 576
83. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedProject_bakerWord line 580
84. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedProject_gridWord line 585
85. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedGrid_covariance line 597

    Source documentation

    A label at the root passes through a two-colour grid as four identical leaf labels. All colours here are arbitrary; only finite stabilizer laws were used.

    lemma decoratedGrid_covariance (g : Γ) (y z : X) :
        decoratedRoot x s t g*decoratedGrid x s t hs y z=
          decoratedGrid x s t hs (g • y) (g • z)*decoratedTensor x s t hs
            (decoratedDiagonal x s t hs g,decoratedDiagonal x s t hs g) := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedRoot, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedGrid, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedTensor, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedDiagonal