feat(group_theory/perm): signatures of permutations (#231)

Author: ChrisHughes24

algebra/big_operators.lean

@@ -378,11 +378,11 @@ section group
 open list
 variables [group α] [group β]
 
-theorem is_group_hom.prod {f : α → β} [is_group_hom f] (l : list α) :
+theorem is_group_hom.prod (f : α → β) [is_group_hom f] (l : list α) :
   f (prod l) = prod (map f l) :=
 by induction l; simp [*, is_group_hom.mul f, is_group_hom.one f]
 
-theorem is_group_anti_hom.prod {f : α → β} [is_group_anti_hom f] (l : list α) :
+theorem is_group_anti_hom.prod (f : α → β) [is_group_anti_hom f] (l : list α) :
   f (prod l) = prod (map f (reverse l)) :=
 by induction l; simp [*, is_group_anti_hom.mul f, is_group_anti_hom.one f]
 

algebra/group.lean

@@ -247,6 +247,8 @@ by refine {mul := (*), one := 1, inv := has_inv.inv, ..};
 instance {α} [comm_monoid α] : comm_group (units α) :=
 { mul_comm := λ u₁ u₂, ext $ mul_comm _ _, ..units.group }
 
+instance [has_repr α] : has_repr (units α) := ⟨repr ∘ val⟩
+
 @[simp] theorem mul_left_inj (a : units α) {b c : α} : (a:α) * b = a * c ↔ b = c :=
 ⟨λ h, by simpa using congr_arg ((*) ↑(a⁻¹ : units α)) h, congr_arg _⟩
 
@@ -576,6 +578,19 @@ end add_comm_group
 
 variables {β : Type*} [group α] [group β]
 
+def is_conj (a b : α) := ∃ c : α, c * a * c⁻¹ = b
+
+@[refl] lemma is_conj_refl (a : α) : is_conj a a := ⟨1, by simp⟩
+
+@[symm] lemma is_conj_symm (a b : α) : is_conj a b → is_conj b a
+| ⟨c, hc⟩ := ⟨c⁻¹, by simp [hc.symm, mul_assoc]⟩
+
+@[trans] lemma is_conj_trans (a b c : α) : is_conj a b → is_conj b c → is_conj a c
+| ⟨c₁, hc₁⟩ ⟨c₂, hc₂⟩ := ⟨c₂ * c₁, by simp [hc₁.symm, hc₂.symm, mul_assoc]⟩
+
+@[simp] lemma is_conj_iff_eq {α : Type*} [comm_group α] {a b : α} : is_conj a b ↔ a = b :=
+⟨λ ⟨c, hc⟩, by rw [← hc, mul_right_comm, mul_inv_self, one_mul], λ h, by rw h⟩
+
 /-- Predicate for group homomorphism. -/
 class is_group_hom (f : α → β) : Prop :=
 (mul : ∀ a b : α, f (a * b) = f a * f b)
@@ -598,6 +613,9 @@ instance comp {γ} [group γ] (g : β → γ) [is_group_hom g] :
   g (f (x * y)) = g (f x * f y)       : by rw mul f
   ...           = g (f x) * g (f y)   : by rw mul g⟩
 
+protected lemma is_conj (f : α → β) [is_group_hom f] {a b : α} : is_conj a b → is_conj (f a) (f b)
+| ⟨c, hc⟩ := ⟨f c, by rw [← is_group_hom.mul f, ← is_group_hom.inv f, ← is_group_hom.mul f, hc]⟩
+
 end is_group_hom
 
 /-- Predicate for group anti-homomorphism, or a homomorphism

data/equiv/basic.lean

@@ -82,7 +82,7 @@ rfl
 @[simp] theorem inverse_apply_apply : ∀ (e : α ≃ β) (x : α), e.symm (e x) = x
 | ⟨f₁, g₁, l₁, r₁⟩ x := by simp [equiv.symm]; rw l₁
 
-@[simp] lemma inverse_trans_apply (f : α ≃ β) (g : β ≃ γ) (a : γ) : 
+@[simp] lemma inverse_trans_apply (f : α ≃ β) (g : β ≃ γ) (a : γ) :
   (f.trans g).symm a = f.symm (g.symm a) := rfl
 
 @[simp] theorem apply_eq_iff_eq : ∀ (f : α ≃ β) (x y : α), f x = f y ↔ x = y
@@ -98,6 +98,14 @@ theorem apply_eq_iff_eq_inverse_apply : ∀ (f : α ≃ β) (x : α) (y : β), f
 
 @[simp] theorem symm_symm (e : α ≃ β) : e.symm.symm = e := by cases e; refl
 
+@[simp] theorem trans_refl (e : α ≃ β) : e.trans (equiv.refl β) = e := by cases e; refl
+
+@[simp] theorem refl_trans (e : α ≃ β) : (equiv.refl α).trans e = e := by cases e; refl
+
+@[simp] theorem symm_trans (e : α ≃ β) : e.symm.trans e = equiv.refl β :=  ext _ _ (by simp)
+
+@[simp] theorem trans_symm (e : α ≃ β) : e.trans e.symm = equiv.refl α := ext _ _ (by simp)
+
 theorem left_inverse_symm (f : equiv α β) : left_inverse f.symm f := f.left_inv
 
 theorem right_inverse_symm (f : equiv α β) : function.right_inverse f.symm f := f.right_inv
@@ -562,6 +570,18 @@ theorem swap_comp_apply {a b x : α} (π : perm α) :
   π.trans (swap a b) x = if π x = a then b else if π x = b then a else π x :=
 by cases π; refl
 
+@[simp] lemma swap_inv {α : Type*} [decidable_eq α] (x y : α) :
+  (swap x y)⁻¹ = swap x y := rfl
+
+@[simp] lemma symm_trans_swap_trans [decidable_eq α] [decidable_eq β] (a b : α)
+  (e : α ≃ β) : (e.symm.trans (swap a b)).trans e = swap (e a) (e b) :=
+equiv.ext _ _ (λ x, begin
+  have : ∀ a, e.symm x = a ↔ x = e a :=
+    λ a, by rw @eq_comm _ (e.symm x); split; intros; simp * at *,
+  simp [swap_apply_def, this],
+  split_ifs; simp
+end)
+
 /-- Augment an equivalence with a prescribed mapping `f a = b` -/
 def set_value (f : α ≃ β) (a : α) (b : β) : α ≃ β :=
 (swap a (f.symm b)).trans f

data/fin.lean

@@ -21,12 +21,13 @@ by cases j; simp [fin.pred]
 @[simp] protected lemma eta (a : fin n) (h : a.1 < n) : (⟨a.1, h⟩ : fin n) = a :=
 by cases a; refl
 
-instance {n : ℕ} : linear_order (fin n) :=
+instance {n : ℕ} : decidable_linear_order (fin n) :=
 { le_refl := λ a, @le_refl ℕ _ _,
   le_trans := λ a b c, @le_trans ℕ _ _ _ _,
   le_antisymm := λ a b ha hb, fin.eq_of_veq $ le_antisymm ha hb,
   le_total := λ a b, @le_total ℕ _ _ _,
   lt_iff_le_not_le := λ a b, @lt_iff_le_not_le ℕ _ _ _,
+  decidable_le := fin.decidable_le,
   ..fin.has_le,
   ..fin.has_lt }
 

data/finset.lean

@@ -127,6 +127,9 @@ instance : inhabited (finset α) := ⟨∅⟩
 theorem eq_empty_of_forall_not_mem {s : finset α} (H : ∀x, x ∉ s) : s = ∅ :=
 eq_of_veq (eq_zero_of_forall_not_mem H)
 
+lemma eq_empty_iff_forall_not_mem {s : finset α} : s = ∅ ↔ ∀ x, x ∉ s :=
+⟨λ h, by simp [h], λ h, eq_empty_of_forall_not_mem h⟩
+
 @[simp] theorem val_eq_zero {s : finset α} : s.1 = 0 ↔ s = ∅ := @val_inj _ s ∅
 
 theorem subset_empty {s : finset α} : s ⊆ ∅ ↔ s = ∅ := subset_zero.trans val_eq_zero
@@ -1298,6 +1301,9 @@ sort_eq _ _
 @[simp] theorem sort_to_finset [decidable_eq α] (s : finset α) : (sort r s).to_finset = s :=
 list.to_finset_eq (sort_nodup r s) ▸ eq_of_veq (sort_eq r s)
 
+@[simp] theorem mem_sort {s : finset α} {a : α} : a ∈ sort r s ↔ a ∈ s :=
+multiset.mem_sort _
+
 end sort
 
 section disjoint
@@ -1362,6 +1368,17 @@ theorem sort_sorted_lt [decidable_linear_order α] (s : finset α) :
 
 instance [has_repr α] : has_repr (finset α) := ⟨λ s, repr s.1⟩
 
+def attach_fin (s : finset ℕ) {n : ℕ} (h : ∀ m ∈ s, m < n) : finset (fin n) :=
+⟨s.1.pmap (λ a ha, ⟨a, ha⟩) h, multiset.nodup_pmap (λ _ _ _ _, fin.mk.inj) s.2⟩
+
+@[simp] lemma mem_attach_fin {n : ℕ} {s : finset ℕ} (h : ∀ m ∈ s, m < n) {a : fin n} :
+  a ∈ s.attach_fin h ↔ a.1 ∈ s :=
+⟨λ h, let ⟨b, hb₁, hb₂⟩ := multiset.mem_pmap.1 h in hb₂ ▸ hb₁,
+λ h, multiset.mem_pmap.2 ⟨a.1, h, fin.eta _ _⟩⟩
+
+@[simp] lemma card_attach_fin {n : ℕ} (s : finset ℕ) (h : ∀ m ∈ s, m < n) :
+  (s.attach_fin h).card = s.card := multiset.card_pmap _ _ _
+
 end finset
 
 namespace list

data/fintype.lean

@@ -179,6 +179,11 @@ instance : fintype bool := ⟨⟨tt::ff::0, by simp⟩, λ x, by cases x; simp
 
 @[simp] theorem fintype.univ_bool : @univ bool _ = {ff, tt} := rfl
 
+instance units_int.fintype : fintype (units ℤ) :=
+⟨{1, -1}, λ x, by cases int.units_eq_one_or x; simp *⟩
+
+@[simp] theorem fintype.card_units_int : fintype.card (units ℤ) = 2 := rfl
+
 @[simp] theorem fintype.card_bool : fintype.card bool = 2 := rfl
 
 def finset.insert_none (s : finset α) : finset (option α) :=

data/multiset.lean

@@ -2533,6 +2533,9 @@ quot.induction_on s $ λ l, sorted_merge_sort r _
 @[simp] theorem sort_eq (s : multiset α) : ↑(sort r s) = s :=
 quot.induction_on s $ λ l, quot.sound $ perm_merge_sort _ _
 
+@[simp] theorem mem_sort {s : multiset α} {a : α} : a ∈ sort r s ↔ a ∈ s :=
+by conv in (a ∈ s) {rw ← sort_eq r s}; simp [-sort_eq]
+
 end sort
 
 instance [has_repr α] : has_repr (multiset α) :=