OAI/GroupTheory/BooneHigman/ActionEnvelope.lean

GitHub source file

100 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteAlgebraicEnvelopes.intertwine_zpow line 17

   Source documentation

   Intertwining of bijections propagates to every integer iterate.

   theorem intertwine_zpow (F : A → B) (s : MulAut A) (t : MulAut B)
       (h : ∀ x, F (s x)=t (F x)) (n : ℤ) (x : A) : F ((s^n) x)=(t^n) (F x) := by
   …

2. def OAI.FiniteAlgebraicEnvelopes.SequentialLimit.torusCongr line 36
3. def OAI.FiniteAlgebraicEnvelopes.SequentialLimit.quotientTorusEquiv line 43
4. def OAI.FiniteAlgebraicEnvelopes.LimitAction.affineShift line 58
5. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.affineShift_left line 61
6. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.affineShift_right line 63
7. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.affineShift_zpow_left line 66
8. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.affineShift_zpow_right line 69
9. abbrev OAI.FiniteAlgebraicEnvelopes.LimitAction.AffineTorus line 73
10. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.affineLimitEquivalence_shift line 75
11. def OAI.FiniteAlgebraicEnvelopes.LimitAction.affineTorusEquivalence line 81
12. def OAI.FiniteAlgebraicEnvelopes.LimitAction.reassociateTorus line 90

    Source documentation

    Reassociation retains the same translation, linear and stable coordinates.

    def reassociateTorus : AffineTorus α f g hc ≃* (Limit g) ⋊[torusAction α f g hc] Torus f where
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.LimitAction.AffineTorus, OAI.FiniteAlgebraicEnvelopes.LimitAction.torusAction

13. def OAI.FiniteAlgebraicEnvelopes.LimitAction.fullGroupEquivalence line 106
14. def OAI.FiniteAlgebraicEnvelopes.LimitAction.affineQuotient line 120
15. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.affineQuotient_surjective line 123
16. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.affineQuotient_natural line 130
17. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.affineQuotient_kernel line 135
18. def OAI.FiniteAlgebraicEnvelopes.LimitAction.affineQuotientTorusEquivalence line 144
19. def OAI.FiniteAlgebraicEnvelopes.LimitAction.affineQuotientFullEquivalence line 150
20. def OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.torusAction line 164
21. theorem OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.torusAction_injective line 168
22. theorem OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.torusAction_inl line 175
23. abbrev OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.SteinbergGroup line 179
24. def OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.steinbergStep line 180
25. theorem OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.steinberg_column_compatible line 183
26. def OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.affineSteinbergStep line 191
27. def OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.affineTorusFullEquivalence line 195
28. theorem OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.columnStep_transitive line 213
29. theorem OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.limit_transitive line 231
30. instance OAI.FiniteAlgebraicEnvelopes.Contracted.countableAlgebra line 241
31. instance OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.bigAlgebra_countable line 250
32. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.columnTransition line 254
33. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.ColumnSpace line 257
34. instance OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.columnSpace_countable line 259
35. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.columnSpace_infinite line 263
36. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.fixed_tensor_detector line 277
37. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.linearAction line 282
38. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.linearAction_injective line 284
39. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.linear_transitive line 293
40. instance OAI.FiniteAlgebraicEnvelopes.SequentialLimit.torus_finitelyGenerated line 306
41. instance OAI.FiniteAlgebraicEnvelopes.AffinePermutation.action line 346
42. theorem OAI.FiniteAlgebraicEnvelopes.AffinePermutation.smul_apply line 355
43. theorem OAI.FiniteAlgebraicEnvelopes.AffinePermutation.faithful line 357
44. theorem OAI.FiniteAlgebraicEnvelopes.AffinePermutation.two_transitive line 370

    Source documentation

    The ordinary affine formula upgrades linear nonzero transitivity to ordered-pair transitivity.

    theorem two_transitive
        (ht : ∀ v w : V, v≠1 → w≠1 → ∃ x : Q, α x v=w)
        (x₁ x₂ y₁ y₂ : V) (hx : x₁≠x₂) (hy : y₁≠y₂) :
        ∃ a : V ⋊[α] Q, a • x₁=y₁ ∧ a • x₂=y₂ := by
    …

45. def OAI.FiniteAlgebraicEnvelopes.AffinePermutation.stabilizerEquivalence line 385

    Source documentation

    The stabilizer of the distinguished identity point is exactly the linear factor.

    def stabilizerEquivalence : MulAction.stabilizer (V ⋊[α] Q) (1:V) ≃* Q :=
    …

46. def OAI.FiniteAlgebraicEnvelopes.AffinePermutation.stabilizerEquivalenceAt line 405

    Source documentation

    At every point, evaluation determines the translation from the linear component.

    def stabilizerEquivalenceAt (v : V) : MulAction.stabilizer (V ⋊[α] Q) v ≃* Q :=
    …

47. instance OAI.FiniteAlgebraicEnvelopes.AffinePermutation.stabilizer_finitelyGenerated line 422
48. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.LinearTorus line 433
49. instance OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.elementary_finitelyGenerated line 435
50. instance OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.linearTorus_finitelyGenerated line 438
51. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.fullLinearAction line 441
52. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.fullLinearAction_injective line 444
53. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.fullLinear_transitive line 449
54. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.FullGroup line 455
55. instance OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.fullAction_faithful line 457
56. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.fullAction_two_transitive line 460
57. instance OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.fullAction_stabilizer_fg line 464
58. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.affineTransition line 468
59. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.affineTorusEquivalence line 471

    Source documentation

    The literal affine-Steinberg mapping torus is the previously constructed full action group.

    def affineTorusEquivalence : SequentialLimit.Torus (affineTransition s h) ≃* FullGroup s h :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.SequentialLimit.Torus, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.affineTransition, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.FullGroup

60. def OAI.FiniteAlgebraicEnvelopes.Steinberg.diagonalUnits line 481
61. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.diagonalUnits_val line 490
62. def OAI.FiniteAlgebraicEnvelopes.Steinberg.weylUnit line 493
63. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.weylUnit_matrix line 496
64. def OAI.FiniteAlgebraicEnvelopes.Steinberg.balancedUnit line 505
65. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.balancedUnit_matrix line 508
66. def OAI.FiniteAlgebraicEnvelopes.Steinberg.singleDiagonal line 522
67. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.singleDiagonal_val line 527
68. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.singleDiagonal_injective line 534
69. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.balancedUnit_commutator line 540
70. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.singleDiagonal_commutator_mem line 550
71. def OAI.FiniteAlgebraicEnvelopes.Steinberg.firstFactor line 557
72. def OAI.FiniteAlgebraicEnvelopes.Steinberg.inputDiagonal line 562
73. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.inputDiagonal_injective line 564
74. def OAI.FiniteAlgebraicEnvelopes.Steinberg.elementaryEmbedding line 567
75. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.elementaryEmbedding_injective line 576
76. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.elementaryInput line 590
77. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.elementaryInput_injective line 598
78. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.elementaryInFull line 603
79. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.elementaryInFull_injective line 607
80. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.inputInFull line 611
81. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.inputInFull_injective line 614
82. theorem OAI.FiniteAlgebraicEnvelopes.input_full_action line 623

    Source documentation

    The actual constructed group, all action invariants and the original input embedding. This lemma deliberately does not claim finite presentation and is not the envelope theorem.

    theorem input_full_action {G : Type*} [Group G] (hG : HasDecidableWordProblem G) :
        ∃ (Γ : Type) (_ : Group Γ) (X : Type) (_ : MulAction Γ X),
          Countable X ∧ Infinite X ∧ FaithfulSMul Γ X ∧
          (∀ x₁ x₂ y₁ y₂ : X, x₁≠x₂ → y₁≠y₂ → ∃ g : Γ, g • x₁=y₁ ∧ g • x₂=y₂) ∧
          (∀ x : X, Group.FG (MulAction.stabilizer Γ x)) ∧
          ∃ f : G →* Γ, Function.Injective f := by
    …

83. instance OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.steinberg_finitelyPresented line 644
84. instance OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.affine_finitelyPresented line 647
85. instance OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.full_finitelyPresented line 652
86. theorem OAI.FiniteAlgebraicEnvelopes.input_finite_action_envelope line 660

    Source documentation

    The source's complete action envelope, in a small universe.

    theorem input_finite_action_envelope {G : Type*} [Group G] (hG : HasDecidableWordProblem G) :
        ∃ (Γ : Type) (_ : Group Γ) (X : Type) (_ : MulAction Γ X),
          Group.IsFinitelyPresented Γ ∧ Countable X ∧ Infinite X ∧ FaithfulSMul Γ X ∧
          (∀ x₁ x₂ y₁ y₂ : X, x₁≠x₂ → y₁≠y₂ → ∃ g : Γ, g • x₁=y₁ ∧ g • x₂=y₂) ∧
          (∀ x : X, Group.FG (MulAction.stabilizer Γ x)) ∧
          ∃ f : G →* Γ, Function.Injective f := by
    …

87. def OAI.FiniteAlgebraicEnvelopes.LiftedAction.action line 684
88. lemma OAI.FiniteAlgebraicEnvelopes.LiftedAction.down_smul line 691
89. instance OAI.FiniteAlgebraicEnvelopes.LiftedAction.faithful line 693
90. def OAI.FiniteAlgebraicEnvelopes.LiftedAction.stabilizerEquivalence line 701
91. theorem OAI.FiniteAlgebraicEnvelopes.envelope line 717

    Source documentation

    Manuscript Theorem 1.2, with the exact frozen universe and action requirements.

    theorem envelope (G : Type u) [Group G] [Group.FG G]
        (hG : HasDecidableWordProblem G) : HasActionEnvelope G := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.HasActionEnvelope

92. theorem OAI.FiniteAlgebraicEnvelopes.input_elementary line 742

    Source documentation

    The original input, not merely its auxiliary double, embeds in the actual elementary part. The ring and kernel-annihilating coefficient transition are constructed from its algorithmic WP.

    theorem input_elementary {G : Type*} [Group G] (hG : HasDecidableWordProblem G) :
        ∃ (R : Type) (_ : Ring R) (ψ : R →ₙ+* R), Function.Injective ψ ∧
          (∀ z : Steinberg.Group (Fin 6) R, Steinberg.matrixMap z=1 → Steinberg.coefficientMap ψ z=1) ∧
          ∃ f : G →* Steinberg.ElementaryGroup R, Function.Injective f := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.Group, OAI.FiniteAlgebraicEnvelopes.Steinberg.matrixMap, OAI.FiniteAlgebraicEnvelopes.Steinberg.coefficientMap, OAI.FiniteAlgebraicEnvelopes.Steinberg.ElementaryGroup

93. theorem OAI.FiniteAlgebraicEnvelopes.input_steinberg_torus line 762

    Source documentation

    The original input embeds in the constructed Steinberg mapping torus. This does not yet assert finite presentation or simplicity.

    theorem input_steinberg_torus {G : Type*} [Group G] (hG : HasDecidableWordProblem G) :
        ∃ (R : Type) (_ : Ring R) (ψ : R →ₙ+* R), Function.Injective ψ ∧
          (∀ z : Steinberg.Group (Fin 6) R, Steinberg.matrixMap z=1 → Steinberg.coefficientMap ψ z=1) ∧
          ∃ f : G →* SequentialLimit.Torus (Steinberg.coefficientMap (ι:=Fin 6) ψ), Function.Injective f := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.Group, OAI.FiniteAlgebraicEnvelopes.Steinberg.matrixMap, OAI.FiniteAlgebraicEnvelopes.Steinberg.coefficientMap, OAI.FiniteAlgebraicEnvelopes.SequentialLimit.Torus

94. def OAI.FiniteAlgebraicEnvelopes.TypeAAction.Pairs line 783

    Source documentation

    Unordered two-element subsets, without an ordering or repetitions.

    def Pairs (X : Type v) := {s : Finset X // s.card=2}
    …

95. def OAI.FiniteAlgebraicEnvelopes.TypeAAction.pairAction line 787
96. lemma OAI.FiniteAlgebraicEnvelopes.TypeAAction.pairs_pretransitive line 794
97. lemma OAI.FiniteAlgebraicEnvelopes.TypeAAction.pairs_single_orbit line 809
98. lemma OAI.FiniteAlgebraicEnvelopes.TypeAAction.pairs_finite_orbits line 815
99. def OAI.FiniteAlgebraicEnvelopes.TypeAAction.Hypotheses line 823

    Source documentation

    Type-(A) action hypotheses.

    def Hypotheses (Γ : Type u) [Group Γ] (X : Type v) [MulAction Γ X] : Prop :=
    …

100. theorem OAI.FiniteAlgebraicEnvelopes.TypeAAction.envelope_hypotheses line 828