English
Let s be a finite set and f: s → Perm β with pairwise commuting or noncommuting as specified; then the support of the noncommutative product (s.noncommProd f comm) contains moves coming from individual components: there exists a ∈ s with x in (f a).support.
Русский
Пусть s конечное множество и f: s → Perm β; тогда опора некоммтового произведения содержит переносы от отдельных членов: найдется a ∈ s такое, что x переноси по f(a).
LaTeX
$$$\exists a \in s, x \in (f(a)).\operatorname{support}$ given $x \in (s.\operatorname{noncommProd} f comm).\operatorname{support}.$$$
Lean4
theorem mem_support_of_mem_noncommProd_support {α β : Type*} [DecidableEq β] [Fintype β] {s : Finset α} {f : α → Perm β}
{comm : (s : Set α).Pairwise (Commute on f)} {x : β} (hx : x ∈ (s.noncommProd f comm).support) :
∃ a ∈ s, x ∈ (f a).support := by
contrapose! hx
classical
revert hx comm s
apply Finset.induction
· simp
· intro a s ha ih comm hs
rw [Finset.noncommProd_insert_of_notMem s a f comm ha]
apply mt (Finset.mem_of_subset (support_mul_le _ _))
rw [Finset.sup_eq_union, Finset.notMem_union]
exact ⟨hs a (s.mem_insert_self a), ih (fun a ha ↦ hs a (Finset.mem_insert_of_mem ha))⟩
