## Stream: Is there code for X?

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

#### Eric Wieser (Dec 06 2020 at 12:16):

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 (Dec 06 2020 at 12:17):

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

#### Eric Wieser (Dec 06 2020 at 13:07):

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 (Dec 07 2020 at 10:07):

#5266

Last updated: May 16 2021 at 05:21 UTC