feat(group_theory/perm/sign): Add sign_sum_congr (#5266)

src/data/equiv/basic.lean

@@ -1587,6 +1587,30 @@ begin
   rw swap_apply_of_ne_of_ne hi hj,
 end
 
+namespace perm
+
+@[simp] lemma sum_congr_swap_refl {α β : Sort*} [decidable_eq α] [decidable_eq β] (i j : α) :
+  equiv.perm.sum_congr (equiv.swap i j) (equiv.refl β) = equiv.swap (sum.inl i) (sum.inl j) :=
+begin
+  ext x,
+  cases x,
+  { simp [sum.map, swap_apply_def],
+    split_ifs; refl},
+  { simp [sum.map, swap_apply_of_ne_of_ne] },
+end
+
+@[simp] lemma sum_congr_refl_swap {α β : Sort*} [decidable_eq α] [decidable_eq β] (i j : β) :
+  equiv.perm.sum_congr (equiv.refl α) (equiv.swap i j) = equiv.swap (sum.inr i) (sum.inr j) :=
+begin
+  ext x,
+  cases x,
+  { simp [sum.map, swap_apply_of_ne_of_ne] },
+  { simp [sum.map, swap_apply_def],
+    split_ifs; refl},
+end
+
+end perm
+
 /-- Augment an equivalence with a prescribed mapping `f a = b` -/
 def set_value (f : α ≃ β) (a : α) (b : β) : α ≃ β :=
 (swap a (f.symm b)).trans f

src/group_theory/perm/basic.lean

@@ -62,6 +62,14 @@ sum_congr_symm e f
   sum_congr (1 : perm α) (1 : perm β) = 1 :=
 sum_congr_refl
 
+@[simp] lemma sum_congr_swap_one {α β : Type*} [decidable_eq α] [decidable_eq β] (i j : α) :
+  sum_congr (equiv.swap i j) (1 : perm β) = equiv.swap (sum.inl i) (sum.inl j) :=
+sum_congr_swap_refl i j
+
+@[simp] lemma sum_congr_one_swap {α β : Type*} [decidable_eq α] [decidable_eq β] (i j : β) :
+  sum_congr (1 : perm α) (equiv.swap i j) = equiv.swap (sum.inr i) (sum.inr j) :=
+sum_congr_refl_swap i j
+
 /-! Lemmas about `equiv.perm.sigma_congr_right` re-expressed via the group structure. -/
 
 @[simp] lemma sigma_congr_right_mul {α} {β : α → Type*}

src/group_theory/perm/sign.lean

@@ -792,6 +792,24 @@ equiv.perm.sign_eq_sign_of_equiv _ _ e.symm (by simp)
 
 end
 
+@[simp] lemma sign_sum_congr {α β : Type*} [decidable_eq α] [decidable_eq β]
+  [fintype α] [fintype β] (σa : perm α) (σb : perm β) :
+  (sum_congr σa σb).sign = σa.sign * σb.sign :=
+begin
+  suffices : (sum_congr σa (1 : perm β)).sign = σa.sign ∧
+             (sum_congr (1 : perm α) σb).sign = σb.sign,
+  { rw [←this.1, ←this.2, ←sign_mul, sum_congr_mul, one_mul, mul_one], },
+  split,
+  { apply σa.swap_induction_on _ (λ σa' a₁ a₂ ha ih, _),
+    { simp },
+    { rw [←one_mul (1 : perm β), ←sum_congr_mul, sign_mul, sign_mul, ih, sum_congr_swap_one,
+          sign_swap ha, sign_swap (sum.injective_inl.ne_iff.mpr ha)], }, },
+  { apply σb.swap_induction_on _ (λ σb' b₁ b₂ hb ih, _),
+    { simp },
+    { rw [←one_mul (1 : perm α), ←sum_congr_mul, sign_mul, sign_mul, ih, sum_congr_one_swap,
+          sign_swap hb, sign_swap (sum.injective_inr.ne_iff.mpr hb)], }, }
+end
+
 end sign
 
 end equiv.perm