Product with permutation sign

Stream: Is there code for X?

[Peter Nelson]

Is there a non-painful way to do the following?

The first lemma isn't in mathlib, and may be relevant, so I've included that proof.

import Mathlib.GroupTheory.Perm.Sign
import Mathlib.Order.Interval.Finset.Fin
import Mathlib.Order.Fin.Finset

theorem Equiv.Perm.sign_eq_prod_ite_fin {n : ℕ} (σ : Equiv.Perm (Fin n)) :
    σ.sign = ∏ j, ∏ i ∈ Finset.Iio j, (if σ i < σ j then 1 else -1) := by
  suffices h : σ.sign = σ.signAux by
    rw [h, Finset.prod_sigma', Equiv.Perm.signAux]
    convert rfl using 2 with x hx
    · simp [Finset.ext_iff, Equiv.Perm.mem_finPairsLT]
    simp [not_lt, ← ite_not (p := _ ≤ _)]
  refine σ.swap_induction_on (by simp) fun π i j hne h_eq ↦ ?_
  rw [Equiv.Perm.signAux_mul, Equiv.Perm.sign_mul, h_eq, Equiv.Perm.sign_swap hne,
    Equiv.Perm.signAux_swap hne]

theorem prod_comp_eq_of_swap_eq_neg {n : ℕ} {R : Type*} [CommRing R] (f : Fin n → Fin n → R)
    (hf : ∀ i j, f i j = - f j i) (σ : Equiv.Perm (Fin n)) :
    ∏ j, ∏ i ∈ Finset.Iio j, f (σ i) (σ j) = σ.sign * ∏ j, ∏ i ∈ Finset.Iio j, f i j := by
  sorry

[Antoine Chambert-Loir]

For the second one, an induction on permutations, you will just need to check what happens for transpositions.

[Peter Nelson]

Yes - the API for that is suboptimal though.

[Peter Nelson]

I eventually managed it.

import Mathlib.GroupTheory.Perm.Sign
import Mathlib.Algebra.BigOperators.Fin

theorem Equiv.Perm.sign_eq_prod_ite_fin {n : ℕ} (σ : Equiv.Perm (Fin n)) :
    σ.sign = ∏ j, ∏ i ∈ Finset.Iio j, (if σ i < σ j then 1 else -1) := by
  suffices h : σ.sign = σ.signAux by
    rw [h, Finset.prod_sigma', Equiv.Perm.signAux]
    convert rfl using 2 with x hx
    · simp [Finset.ext_iff, Equiv.Perm.mem_finPairsLT]
    simp [not_lt, ← ite_not (p := _ ≤ _)]
  refine σ.swap_induction_on (by simp) fun π i j hne h_eq ↦ ?_
  rw [Equiv.Perm.signAux_mul, Equiv.Perm.sign_mul, h_eq, Equiv.Perm.sign_swap hne,
    Equiv.Perm.signAux_swap hne]

theorem prod_comp_eq_of_swap_eq_neg {n : ℕ} {R : Type*} [CommRing R] (f : Fin n → Fin n → R)
    (hf : ∀ i j, f i j = - f j i) (σ : Equiv.Perm (Fin n)) :
    ∏ j, ∏ i ∈ Finset.Iio j, f (σ i) (σ j) = σ.sign * ∏ j, ∏ i ∈ Finset.Iio j, f i j := by
  rw [← σ.sign_inv, Equiv.Perm.sign_eq_prod_ite_fin, Finset.prod_sigma', Finset.prod_sigma',
    Finset.prod_sigma']
  simp only [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_le (σ.symm x1) (σ.symm x2)
    · exact ⟨_, _, hlt', by simp [hlt.le]⟩
    exact ⟨_, _, hle.lt_of_ne (by simp [hlt.ne]), by simp [hlt.le]⟩
  have hinj := Finset.injOn_of_card_image_eq (s := D) (by rw [hφD])
  nth_rw 2 [← hφD]
  rw [Finset.prod_image (fun x hx y hy hxy ↦ hinj hx hy hxy)]
  refine Finset.prod_congr rfl fun ⟨x₁, x₂⟩ hx ↦ ?_
  replace hx : x₂ < x₁ := by simpa [hD] using hx
  obtain hlt | hle := lt_or_le (σ x₁) (σ x₂)
  · simp [inf_eq_left.2 hlt.le, sup_eq_right.2 hlt.le, hx.not_lt, ← hf]
  simp [inf_eq_right.2 hle, sup_eq_left.2 hle, hx]
    obtain hlt' | hle := lt_or_le (σ.symm x1) (σ.symm x2)
    · exact ⟨_, _, hlt', by simp [hlt.le]⟩
    exact ⟨_, _, hle.lt_of_ne (by simp [hlt.ne]), by simp [hlt.le]⟩
  have hinj := Finset.injOn_of_card_image_eq (s := D) (by rw [hφD])
  nth_rw 2 [← hφD]
  rw [Finset.prod_image (fun x hx y hy hxy ↦ hinj hx hy hxy)]
  refine Finset.prod_congr rfl fun ⟨x₁, x₂⟩ hx ↦ ?_
  simp [D] at hx
  obtain hlt | hle := lt_or_le (σ x₁) (σ x₂)
  · simp [inf_eq_left.2 hlt.le, sup_eq_right.2 hlt.le, hx.not_lt, ← hf]
  simp [inf_eq_right.2 hle, sup_eq_left.2 hle, hx]

It isn't too hard to write an induction lemma for adjacent transpositions, but I couldn't find a proof using that method that was nearly as clean.

[Eric Wieser]

I think we already have an induction principle for adjacent transpositions somewhere - but perhaps I'm thinking of a stale mathlib3 branch.

[Michael Stoll]

Maybe docs#Tuple.bubble_sort_induction or docs#Tuple.bubble_sort_induction' are relevant?

[Peter Nelson]

It’s not the existence of the lemma, really - it’s more the faffing around with indices that comes with applying it. Even if you swap two adjacent things in the permutation, you’re flipping the sign and position of linearly many terms in the product. I couldn’t see how to write a proof that handles all that in less space than the above.

[Peter Nelson]

Here are the induction principles I wrote (the bubble-sort lemma isn't the right thing, since that is an increasing swap rather than an adjacent one). A shorter proof of prod_comp_eq_of_swap_eq_neg using either of these would be welcome.

theorem Equiv.Perm.transpose_induction_on_right {P : Equiv.Perm (Fin (n+1)) → Prop}
    (f : Equiv.Perm (Fin (n+1))) (h1 : P 1) (ih : ∀ (i : Fin n) (g : Equiv.Perm (Fin (n+1))),
      P g → P (g * Equiv.swap i.castSucc i.succ)) : P f :=
  Submonoid.induction_of_closure_eq_top_right (Equiv.Perm.mclosure_swap_castSucc_succ n) f h1 <| by
    rintro σ _ ⟨i, hi, rfl⟩ hσ
    exact ih _ _ hσ

theorem Equiv.Perm.transpose_induction_on_left {P : Equiv.Perm (Fin (n+1)) → Prop}
    (f : Equiv.Perm (Fin (n+1))) (h1 : P 1) (ih : ∀ (i : Fin n) (g : Equiv.Perm (Fin (n+1))),
      P g → P (Equiv.swap i.castSucc i.succ * g)) : P f :=
  Submonoid.induction_of_closure_eq_top_left (Equiv.Perm.mclosure_swap_castSucc_succ n) f h1 <| by
    rintro _ ⟨i, hi, rfl⟩ σ hσ
    exact ih _ _ hσ