equiv.perm.sign (equiv.sum_congr σa σb) = σa.sign * σb.sign

Stream: Is there code for X?

[Eric Wieser]

I'm getting stuck on the last, "well, obviously" step of this proof:

import group_theory.perm.sign

@[simp] lemma sign_sum_congr {α β : Type*} [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] (σa : equiv.perm α) (σb : equiv.perm β) :
  equiv.perm.sign (equiv.sum_congr σa σb) = σa.sign * σb.sign :=
begin
  suffices : equiv.perm.sign (equiv.sum_congr σa 1) = σa.sign ∧
             equiv.perm.sign (equiv.sum_congr 1 σb) = σb.sign,
  { rw [←this.1, ←this.2, ←equiv.perm.sign_mul],
    simp only [equiv.perm.mul_def, equiv.perm.one_def],
    rw [equiv.sum_congr_trans],
    congr, },
  sorry,  -- obviously
end

The argument is along the lines of "sign counts the number of swaps, inserting elements which remain in place does not affect the number of swaps".

[Eric Wieser]

(it would also be cool if I could apply wlog to unify those two goals into a single goal)

[Eric Wieser]

Reduced to an even more obvious statement,

@[simp] lemma sum_congr_swap_left {α β : Type*} [decidable_eq α] [decidable_eq β] (i j : α) :
  equiv.sum_congr (equiv.swap i j) (1 : equiv.perm β) = equiv.swap (sum.inl i) (sum.inl j) :=
begin
  sorry
end

@[simp] lemma sum_congr_swap_right {α β : Type*} [decidable_eq α] [decidable_eq β] (i j : β) :
  equiv.sum_congr (1 : equiv.perm α) (equiv.swap i j) = equiv.swap (sum.inr i) (sum.inr j) :=
begin
  sorry
end

as

@[simp] lemma sign_sum_congr {α β : Type*} [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] (σa : equiv.perm α) (σb : equiv.perm β) :
  equiv.perm.sign (equiv.sum_congr σa σb) = σa.sign * σb.sign :=
begin
  suffices : equiv.perm.sign (equiv.sum_congr σa 1) = σa.sign ∧
             equiv.perm.sign (equiv.sum_congr 1 σb) = σb.sign,
  { rw [←this.1, ←this.2, ←equiv.perm.sign_mul],
    simp only [equiv.perm.mul_def, equiv.perm.one_def],
    rw [equiv.sum_congr_trans],
    congr, },
  split,
  { apply σa.swap_induction_on _ (λ σa' a₁ a₂ ha ih, _),
    { erw [equiv.sum_congr_refl], simp },
    { erw [←one_mul (1 : equiv.perm β), ←equiv.sum_congr_trans, equiv.perm.sign_mul,
           equiv.perm.sign_mul, ih],
      congr,
      rw perm.sign_swap ha,
      erw equiv.sum_congr_swap_left,
      exact perm.sign_swap (sum.injective_inl.ne_iff.mpr ha), }, },
  { apply σb.swap_induction_on _ (λ σb' b₁ b₂ hb ih, _),
    { erw [equiv.sum_congr_refl], simp },
    { erw [←one_mul (1 : equiv.perm α), ←equiv.sum_congr_trans, equiv.perm.sign_mul,
           equiv.perm.sign_mul, ih],
      congr,
      rw perm.sign_swap hb,
      erw equiv.sum_congr_swap_right,
      exact perm.sign_swap (sum.injective_inr.ne_iff.mpr hb), }, }
end

[Eric Wieser]

#5266