Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC