English
The sign of the product-conjugation over a family of permutations equals the product of the signs.
Русский
Знак произведения конгруэнтности равен произведению знаков.
LaTeX
$$$\\operatorname{sign}(\\operatorname{prodCongrRight}(\\sigma)) = \\prod k\\; \\operatorname{sign}(\\sigma(k))$$$
Lean4
/-- If we apply `prod_extendRight a (σ a)` for all `a : α` in turn,
we get `prod_congrRight σ`. -/
theorem prod_prodExtendRight {α : Type*} [DecidableEq α] (σ : α → Perm β) {l : List α} (hl : l.Nodup)
(mem_l : ∀ a, a ∈ l) : (l.map fun a => prodExtendRight a (σ a)).prod = prodCongrRight σ :=
by
ext ⟨a, b⟩ : 1
-- We'll use induction on the list of elements,
-- but we have to keep track of whether we already passed `a` in the list.
suffices
a ∈ l ∧ (l.map fun a => prodExtendRight a (σ a)).prod (a, b) = (a, σ a b) ∨
a ∉ l ∧ (l.map fun a => prodExtendRight a (σ a)).prod (a, b) = (a, b)
by
obtain ⟨_, prod_eq⟩ := Or.resolve_right this (not_and.mpr fun h _ => h (mem_l a))
rw [prod_eq, prodCongrRight_apply]
clear mem_l
induction l with
| nil =>
refine Or.inr ⟨List.not_mem_nil, ?_⟩
rw [List.map_nil, List.prod_nil, one_apply]
| cons a' l ih =>
rw [List.map_cons, List.prod_cons, mul_apply]
rcases ih (List.nodup_cons.mp hl).2 with (⟨mem_l, prod_eq⟩ | ⟨notMem_l, prod_eq⟩) <;> rw [prod_eq]
· refine Or.inl ⟨List.mem_cons_of_mem _ mem_l, ?_⟩
rw [prodExtendRight_apply_ne _ fun h : a = a' => (List.nodup_cons.mp hl).1 (h ▸ mem_l)]
by_cases ha' : a = a'
· rw [← ha'] at *
refine Or.inl ⟨l.mem_cons_self, ?_⟩
rw [prodExtendRight_apply_eq]
· refine Or.inr ⟨fun h => not_or_intro ha' notMem_l ((List.mem_cons).mp h), ?_⟩
rw [prodExtendRight_apply_ne _ ha']
