AdjacentPermutations.lean`

52 declarations, 0 contain sorry, 0 declared as axioms

Coxeter presentation and universal lifts of finite symmetric groups.

structure OAI.FiniteAlgebraicEnvelopes.Adjacent.Relations line 18
Source documentation
The Coxeter relations on the first n adjacent generators.
```
structure Relations (r : ℕ → H) (n : ℕ) : Prop where
…
```
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.Relations.mono line 23
def OAI.FiniteAlgebraicEnvelopes.Adjacent.descending line 30
Source documentation
r (n-1) ... r i, with the empty product when n ≤ i.
```
def descending (r : ℕ → H) (i : ℕ) : ℕ → H
  | 0 => 1
  | n+1 => if i ≤ n then r n * descending r i n else 1
```
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.descending_zero line 34
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.descending_step line 35
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.descending_empty line 38
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.descending_commute line 43
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.descending_extend line 55
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.descending_cancel line 67
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.descending_last line 71

lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.descending_mul line 87

Source documentation

The elementary normal-form multiplication rules.

lemma descending_mul {r : ℕ → H} {n : ℕ} (h : Relations r n)
    (i : ℕ) (hi : i ≤ n) (j : ℕ) (hj : j < n) :
    descending r i n * r j =
      if j+1 < i then r j * descending r i n else
      if j+1 = i then descending r j n else
      if j = i then descending r (i+1) n else
        r (j-1) * descending r i n := by
…

Mentions: OAI.FiniteAlgebraicEnvelopes.Adjacent.Relations, OAI.FiniteAlgebraicEnvelopes.Adjacent.descending

def OAI.FiniteAlgebraicEnvelopes.Adjacent.first line 124
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.normal_form line 128
Source documentation
Every element generated by n+1 adjacent generators is in one of n+2 right cosets of the subgroup generated by the first n.
```
lemma normal_form {r : ℕ → H} {n : ℕ} (h : Relations r (n+1)) {g : H}
    (hg : g ∈ Subgroup.closure (first r (n+1))) :
    ∃ (i : ℕ), i ≤ n+1 ∧ ∃ k ∈ Subgroup.closure (first r n),
      g = k * descending r i (n+1) := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Adjacent.Relations, OAI.FiniteAlgebraicEnvelopes.Adjacent.first, OAI.FiniteAlgebraicEnvelopes.Adjacent.descending
def OAI.FiniteAlgebraicEnvelopes.Adjacent.relators line 163
Source documentation
The usual finite type-A Coxeter presentation.
```
def relators (n : ℕ) : Set (FreeGroup (Fin n)) := {w |
…
```
abbrev OAI.FiniteAlgebraicEnvelopes.Adjacent.Presentation line 171
def OAI.FiniteAlgebraicEnvelopes.Adjacent.generator line 173
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.generator_lt line 176
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.generator_ge line 178
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.generator_relations line 181
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.relators_valid line 204
def OAI.FiniteAlgebraicEnvelopes.Adjacent.lift line 213
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.lift_of line 216
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.lift_generator line 218
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.closure_first line 221
def OAI.FiniteAlgebraicEnvelopes.Adjacent.inclusion line 229
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.inclusion_of line 232
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.presentation_normal line 235
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.map_descending line 252
def OAI.FiniteAlgebraicEnvelopes.Adjacent.natSwap line 258
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.natSwap_relations line 260
def OAI.FiniteAlgebraicEnvelopes.Adjacent.natEvaluation line 274
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.natEvaluation_of line 277
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.natEvaluation_generator line 279
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.natEvaluation_inclusion line 282
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.natEvaluation_fixes line 288
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.descending_nat_apply line 303
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.natEvaluation_descending line 317
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.natEvaluation_injective line 329
def OAI.FiniteAlgebraicEnvelopes.Adjacent.natExtend line 355
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.natExtend_injective line 358
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.natExtend_swap line 361
def OAI.FiniteAlgebraicEnvelopes.Adjacent.finSwap line 369
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.finSwap_lt line 372
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.natExtend_finSwap line 375
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.finSwap_relations line 379
def OAI.FiniteAlgebraicEnvelopes.Adjacent.finEvaluation line 393
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.finEvaluation_of line 396
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.natExtend_finEvaluation line 400
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.finEvaluation_bijective line 407
def OAI.FiniteAlgebraicEnvelopes.Adjacent.permutationEquiv line 425
def OAI.FiniteAlgebraicEnvelopes.Adjacent.permutationLift line 430
Source documentation
Coxeter's relations are sufficient, not just necessary: any adjacent family satisfying the three local laws gives a canonical finite permutation action.
```
noncomputable def permutationLift {H : Type u} [Group H] {n : ℕ} {r : ℕ → H}
    (h : Relations r n) : Equiv.Perm (Fin (n+1)) →* H :=
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Adjacent.Relations
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.permutationLift_swap line 434