English
Given a list of elements and a permutation with non-fixed points in that list, recursively factor the permutation into a product of transpositions.
Русский
Дано список элементов и перестановка с неподвижными точками среди этого списка, рекурсивно разложить перестановку на произведение транспозиций.
LaTeX
$$$ \\text{swapFactorsAux} : (l : List\\ α) \\to (f : Perm\\ α) \\to (\\forall {x}, f\\ x \\neq x \\to x \\in l) \\to { l : List (Perm\\ α) // l.prod = f ∧ \\forall g \\in l, g.isSwap } $$$
Lean4
/-- Given a list `l : List α` and a permutation `f : Perm α` such that the nonfixed points of `f`
are in `l`, recursively factors `f` as a product of transpositions. -/
def swapFactorsAux :
∀ (l : List α) (f : Perm α), (∀ {x}, f x ≠ x → x ∈ l) → { l : List (Perm α) // l.prod = f ∧ ∀ g ∈ l, IsSwap g }
| [] => fun f h =>
⟨[],
Equiv.ext fun x => by
rw [List.prod_nil]
exact (Classical.not_not.1 (mt h List.not_mem_nil)).symm,
by simp⟩
| x :: l => fun f h =>
if hfx : x = f x then
swapFactorsAux l f fun {y} hy => List.mem_of_ne_of_mem (fun h : y = x => by simp [h, hfx.symm] at hy) (h hy)
else
let m :=
swapFactorsAux l (swap x (f x) * f) fun {y} hy =>
have : f y ≠ y ∧ y ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hy
List.mem_of_ne_of_mem this.2 (h this.1)
⟨swap x (f x) :: m.1, by
rw [List.prod_cons, m.2.1, ← mul_assoc, mul_def (swap x (f x)), swap_swap, ← one_def, one_mul], fun {_} hg =>
((List.mem_cons).1 hg).elim (fun h => ⟨x, f x, hfx, h⟩) (m.2.2 _)⟩
