Generators.lean`

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

Concrete finite generators of the twisted group.

abbrev OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.left line 19
abbrev OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.right line 20
def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.associator line 22
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.associator_left line 27
def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.flip line 36
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.flip_left line 39
def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.finiteSet line 45
Source documentation
Four untwisted elements, together with the root and one half-copy of the acting group. This is an explicitly finitely generated subgroup when Γ is FG.
```
def finiteSet (x : X) : Finset (group (Γ:=Γ) (X:=X)) :=
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.group
def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.subgroup line 48
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.root_mem line 52
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.half_root_mem line 55
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.finite_mem line 58
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.associator_mem line 64
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.flip_mem line 66
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.half_associator_mem line 68
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.half_flip_mem line 70
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.double_local_mem line 73
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.left_local_mem line 80
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.right_local_mem line 98
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.subgroup_fg line 104
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.twistPrefix_oneBit line 121
def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.baker line 128
Source documentation
The untwisted coordinate baker: move a leading bit from x to y.
```
def baker (x y : X) : group (Γ:=Γ) (X:=X) :=
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.group
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.baker_attach line 131
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.baker_inverse line 136
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.baker_smul line 146
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.baker_smul_mem line 159
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.baker_mem line 167
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.bit_local_mem line 172
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.word_local_mem line 182
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.prefix_local_mem line 190
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.oneBit_outside line 223
def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.sumElement line 229
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.sumElement_left line 232
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.sumElement_right line 239
structure OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Move line 250
Source documentation
A complete chart change between coloured splitting trees, already lying in the proposed finite-generator subgroup. Leaf order is not imposed.
```
structure Move (s t : Tree X) where
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree
def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Move.refl line 259
def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Move.trans line 265
def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Move.symm line 274
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Move.element_eq_chart line 283
def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Move.join line 293
def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Move.recolor line 313
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.associator_middle line 333
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.associator_right line 343
def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Move.rotate line 355
abbrev OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.linear line 389
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.linear_card line 393
def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.linearJoin line 406
Source documentation
Binary associativity reduces two right combs to one right comb.
```
def linearJoin (m n : ℕ) :
    Move (Γ:=Γ) x (Tree.split x (Tree.linear x m) (Tree.linear x n))
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Move, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.linear
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.exists_linear line 418
abbrev OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.fixedSwap line 439
Source documentation
Use one fixed equality decision so dependent comb induction does not change which decision procedure is stored in a transposition. The permutation is the usual Mathlib transposition.
```
abbrev fixedSwap {A : Type*} (a b : A) : Equiv.Perm A :=
…
```
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.join_permute_mem line 444
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.flip_attach line 455
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.linear_two_swap line 461
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.linear_front_swap line 483
Source documentation
The first two leaves of every nontrivial right comb can be interchanged using the associator and a half-flip.
```
lemma linear_front_swap (n : ℕ) :
    (Tree.linear x (n+2)).partition.permute (Γ:=Γ)
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.linear
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.linear_front_mem line 525
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.swap_eq_fixedSwap line 543
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.fixedSwap_self line 548
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.fixedSwap_comm line 552
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.sum_swap_right line 555
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.linear_permute_mem line 565
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.tree_chart_mem line 635
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.tree_decorate_mem line 664
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.all_mem line 704
lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.subgroup_eq_top line 722
theorem OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.finite_generation line 730
Source documentation
Finite generation is proved for the concrete finite-table group. This is not the finite-presentation theorem still required at the main endpoint.
```
theorem finite_generation [Group.FG Γ] : Group.FG (group (Γ:=Γ) (X:=X)) := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.group