Zulip Chat Archive

Stream: Is there code for X?

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


view this post on Zulip 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".

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Eric Wieser (Dec 07 2020 at 10:07):

#5266


Last updated: May 16 2021 at 05:21 UTC