Group morphisms (#30)

* feat(algebra/group): morphisms and antimorphisms

Definitions, image of one and inverses,
and computation on a product of more than two elements in big_operators.

Author: PatrickMassot

algebra/big_operators.lean

@@ -304,3 +304,37 @@ finset.induction_on s (by simp [abs_zero]) $
 end discrete_linear_ordered_field
 
 end finset
+
+section group
+
+open list
+variables [group α] [group β]
+
+lemma mph_prod (f : α → β) (hom : is_group_hom f) (l : list α) :
+f (prod l) = prod (map f l) :=
+begin
+  induction l,
+  case nil :
+  { simp[group_hom.one hom] },
+  case cons : hd tl IH
+  { simp,
+    rw hom,
+    simp[IH] }
+end
+
+lemma anti_mph_prod (f : α → β) (anti_mph : is_group_anti_hom f) (l : list α) :
+f (prod l) = prod (map f (reverse l)) :=
+begin
+  induction l,
+  case nil :
+  { simp [group_anti_hom.one anti_mph] },
+  case cons : hd tl IH
+  { simp,
+    rw anti_mph,
+    simp[IH] }
+end
+
+-- Following lemma could also be proved directly by "by induction l; simp *"
+lemma inv_prod (l : list α) : (prod l)⁻¹ = prod (map (λ x, x⁻¹) (reverse l)) := 
+anti_mph_prod (λ x, x⁻¹) group_anti_hom.inv_is_group_anti_hom l
+end group

algebra/group.lean

@@ -322,3 +322,50 @@ theorem sub_le_iff_le_add {a b c : α} : a - c ≤ b ↔ a ≤ b + c :=
 by rw [add_comm]; exact ⟨le_add_of_sub_left_le, sub_left_le_of_le_add⟩
 
 end ordered_comm_group
+
+
+variables { β : Type*} [group α] [group β] {a b : α}
+
+@[simp]
+def is_group_hom (f : α → β) : Prop :=
+∀ a b : α, f(a*b) = f(a)*f(b)
+
+namespace group_hom
+@[simp]
+lemma one { f : α → β } (H : is_group_hom f) : f 1 = 1 :=
+mul_self_iff_eq_one.1 (eq.symm (
+  calc f 1 = f (1*1)     : by simp
+       ... = (f 1)*(f 1) : by rw[H 1 1]))
+
+@[simp]
+lemma inv { f : α → β } (H : is_group_hom f) : (f a)⁻¹ = f (a⁻¹) :=
+inv_eq_of_mul_eq_one (
+  calc (f a) * (f a⁻¹) = f (a * a⁻¹) : by rw[H a a⁻¹]
+                  ...  = f 1 : by simp
+                  ...  = 1   : by rw[one H])
+
+end group_hom
+
+@[simp]
+def is_group_anti_hom (f : α → β) : Prop :=
+∀ a b : α, f(a*b) = f(b)*f(a)
+
+namespace group_anti_hom
+@[simp]
+lemma one { f : α → β } (H : is_group_anti_hom f) : f 1 = 1 :=
+mul_self_iff_eq_one.1 (eq.symm (
+  calc f 1 = f (1*1)     : by simp
+       ... = (f 1)*(f 1) : by rw[H 1 1]))
+
+@[simp]
+lemma inv { f : α → β } (H : is_group_anti_hom f) : (f a)⁻¹ = f (a⁻¹) :=
+inv_eq_of_mul_eq_one (
+  calc (f a) * (f a⁻¹) = f (a⁻¹ * a) : by rw[H a⁻¹ a]
+                  ...  = f 1 : by simp
+                  ...  = 1   : by rw[one H])
+
+
+lemma inv_is_group_anti_hom : is_group_anti_hom (λ x : α, x⁻¹) :=
+mul_inv_rev
+
+end group_anti_hom