English
If f is antisymmetric (f(i,j) = -f(j,i)) and σ is a permutation, then the product of f(σi, σj) over all i<j equals the sign of σ times the product of f(i,j) over all i<j, up to aligning the order.
Русский
Если f антисимметрична (f(i,j) = −f(j,i)) и σ — перестановка, то произведение f(σi, σj) по всем i<j равно знаку σ умноженному на произведение f(i,j) по всем i<j (с корректировкой порядка).
LaTeX
$$$\\forall {R : \\mathrm{CommRing}} [\\mathrm{R} \\text{-конструкция}] (\\sigma : \\mathrm{Equiv.Perm}(\\mathrm{Fin}(n))) \\; \\{ f : \\mathrm{Fin}(n) \\to \\mathrm{Fin}(n) \\to R \\} (hf : \\forall i j, f(i,j) = -f(j,i)) : \n\\\n \\prod_{j} \\prod_{i \\in \\mathrm{Iio}(j)} f(\\sigma i)(\\sigma j) = \\sigma.\\mathrm{sign} \\; \\Big( \\prod_{j} \\prod_{i \\in \\mathrm{Iio}(j)} f(i,j) \\Big)$$$
Lean4
theorem prod_Iio_comp_eq_sign_mul_prod {R : Type*} [CommRing R] (σ : Equiv.Perm (Fin n)) {f : Fin n → Fin n → R}
(hf : ∀ i j, f i j = -f j i) : ∏ j, ∏ i ∈ Finset.Iio j, f (σ i) (σ j) = σ.sign * ∏ j, ∏ i ∈ Finset.Iio j, f i j :=
by
simp_rw [← σ.sign_inv, σ⁻¹.sign_eq_prod_prod_Iio, Finset.prod_sigma', Units.coe_prod, Int.cast_prod, ←
Finset.prod_mul_distrib]
set D := (Finset.univ : Finset (Fin n)).sigma Finset.Iio with hD
have hφD : D.image (fun x ↦ ⟨σ x.1 ⊔ σ x.2, σ x.1 ⊓ σ x.2⟩) = D :=
by
ext ⟨x1, x2⟩
suffices (∃ a, ∃ b < a, σ a ⊔ σ b = x1 ∧ σ a ⊓ σ b = x2) ↔ x2 < x1 by simpa [hD]
refine ⟨?_, fun hlt ↦ ?_⟩
· rintro ⟨i, j, hij, rfl, rfl⟩
exact inf_le_sup.lt_of_ne <| by simp [hij.ne.symm]
obtain hlt' | hle := lt_or_ge (σ.symm x1) (σ.symm x2)
· exact ⟨_, _, hlt', by simp [hlt.le]⟩
exact ⟨_, _, hle.lt_of_ne (by simp [hlt.ne]), by simp [hlt.le]⟩
nth_rw 2 [← hφD]
rw [Finset.prod_image fun x hx y hy ↦ Finset.injOn_of_card_image_eq (by rw [hφD]) hx hy]
refine Finset.prod_congr rfl fun ⟨x₁, x₂⟩ hx ↦ ?_
replace hx : x₂ < x₁ := by simpa [hD] using hx
obtain hlt | hle := lt_or_ge (σ x₁) (σ x₂)
· simp [inf_eq_left.2 hlt.le, sup_eq_right.2 hlt.le, hx.not_gt, ← hf]
simp [inf_eq_right.2 hle, sup_eq_left.2 hle, hx]
