feat(group_theory): start on group theory, define quotient group

group_theory.hlean

@@ -0,0 +1,168 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Floris van Doorn
+
+Basic group theory
+-/
+
+import algebra.group hit.set_quotient
+
+open eq algebra is_trunc set_quotient relation
+
+namespace group
+
+  definition Group_of_CommGroup [coercion] [constructor] (G : CommGroup) : Group :=
+  Group.mk G _
+
+  structure subgroup (G : Group) :=
+    (R : G → hprop)
+    (Rone : R one)
+    (Rmul : Π{g h}, R g → R h → R (g * h))
+    (Rinv : Π{g}, R g → R (g⁻¹))
+
+  structure normal_subgroup (G : Group) extends subgroup G :=
+    (is_normal : Π{g} h, R g → R (h * g * h⁻¹))
+
+  attribute subgroup.R [coercion]
+  abbreviation subgroup_rel         [unfold 2] := @subgroup.R
+  abbreviation subgroup_has_one     [unfold 2] := @subgroup.Rone
+  abbreviation subgroup_respect_mul [unfold 2] := @subgroup.Rmul
+  abbreviation subgroup_respect_inv [unfold 2] := @subgroup.Rinv
+  abbreviation is_normal_subgroup   [unfold 2] := @normal_subgroup.is_normal
+
+  variables {G : Group} (R : normal_subgroup G) {g g' h h' k : G}
+
+  theorem is_normal_subgroup' (h : G) (r : R g) : R (h⁻¹ * g * h) :=
+  inv_inv h ▸ is_normal_subgroup R h⁻¹ r
+
+  theorem is_normal_subgroup_rev (h : G) (r : R (h * g * h⁻¹)) : R g :=
+  have H : h⁻¹ * (h * g * h⁻¹) * h = g, from calc
+    h⁻¹ * (h * g * h⁻¹) * h = h⁻¹ * (h * g) * h⁻¹ * h : by rewrite [-mul.assoc h⁻¹]
+                        ... = h⁻¹ * (h * g)           : by rewrite [inv_mul_cancel_right]
+                        ... = g                       : inv_mul_cancel_left,
+  H ▸ is_normal_subgroup' R h r
+
+  theorem is_normal_subgroup_rev' (h : G) (r : R (h⁻¹ * g * h)) : R g :=
+  is_normal_subgroup_rev R h⁻¹ ((inv_inv h)⁻¹ ▸ r)
+
+  theorem normal_subgroup_insert (r : R k) (r' : R (g * h)) : R (g * (k * h)) :=
+  have H1 : R ((g * h) * (h⁻¹ * k * h)), from
+    subgroup_respect_mul R r' (is_normal_subgroup' R h r),
+  have H2 : (g * h) * (h⁻¹ * k * h) = g * (k * h), from calc
+    (g * h) * (h⁻¹ * k * h) = g * (h * (h⁻¹ * k * h))   : mul.assoc
+                        ... = g * (h * (h⁻¹ * (k * h))) : by rewrite [mul.assoc h⁻¹]
+                        ... = g * (k * h)               : by rewrite [mul_inv_cancel_left],
+  show R (g * (k * h)), from H2 ▸ H1
+
+  definition quotient_rel (g h : G) : hprop := R (g * h⁻¹)
+
+  variable {R}
+  theorem quotient_rel_refl (g : G) : quotient_rel R g g :=
+  transport (λx, R x) !mul.right_inv⁻¹ (subgroup_has_one R)
+  theorem quotient_rel_symm (r : quotient_rel R g h) : quotient_rel R h g :=
+  transport (λx, R x) (!mul_inv ⬝ ap (λx, x * _) !inv_inv) (subgroup_respect_inv R r)
+
+  theorem quotient_rel_trans (r : quotient_rel R g h) (s : quotient_rel R h k)
+    : quotient_rel R g k :=
+  have H1 : R ((g * h⁻¹) * (h * k⁻¹)), from subgroup_respect_mul R r s,
+  have H2 : (g * h⁻¹) * (h * k⁻¹) = g * k⁻¹, from calc
+    (g * h⁻¹) * (h * k⁻¹) = ((g * h⁻¹) * h) * k⁻¹ : by rewrite [mul.assoc (g * h⁻¹)]
+                      ... = g * k⁻¹               : by rewrite inv_mul_cancel_right,
+  show R (g * k⁻¹), from H2 ▸ H1
+
+  theorem quotient_rel_resp_inv (r : quotient_rel R g h) : quotient_rel R g⁻¹ h⁻¹ :=
+  have H1 : R (g⁻¹ * (h * g⁻¹) * g), from
+    is_normal_subgroup' R g (quotient_rel_symm r),
+  have H2 : g⁻¹ * (h * g⁻¹) * g = g⁻¹ * h⁻¹⁻¹, from calc
+    g⁻¹ * (h * g⁻¹) * g = g⁻¹ * h * g⁻¹ * g : by rewrite -mul.assoc
+                    ... = g⁻¹ * h           : inv_mul_cancel_right
+                    ... = g⁻¹ * h⁻¹⁻¹       : by rewrite algebra.inv_inv,
+  show R (g⁻¹ * h⁻¹⁻¹), from H2 ▸ H1
+
+  theorem quotient_rel_resp_mul (r : quotient_rel R g h) (r' : quotient_rel R g' h')
+    : quotient_rel R (g * g') (h * h') :=
+  have H1 : R (g * ((g' * h'⁻¹) * h⁻¹)), from
+    normal_subgroup_insert R r' r,
+  have H2 : g * ((g' * h'⁻¹) * h⁻¹) = (g * g') * (h * h')⁻¹, from calc
+    g * ((g' * h'⁻¹) * h⁻¹) = g * (g' * (h'⁻¹ * h⁻¹)) : by rewrite [mul.assoc]
+                        ... = (g * g') * (h'⁻¹ * h⁻¹) : mul.assoc
+                        ... = (g * g') * (h * h')⁻¹ : by rewrite [mul_inv],
+  show R ((g * g') * (h * h')⁻¹), from H2 ▸ H1
+
+  theorem is_equivalence_quotient_rel : is_equivalence (quotient_rel R) :=
+  is_equivalence.mk quotient_rel_refl
+                    (λg h, quotient_rel_symm)
+                    (λg h k, quotient_rel_trans)
+
+  local attribute is_equivalence_quotient_rel [instance]
+  variable (R)
+  definition qg : Type := set_quotient (quotient_rel R)
+  variable {R}
+  local attribute qg [reducible]
+
+  definition quotient_one [constructor] : qg R := class_of one
+  definition quotient_inv [unfold 3] : qg R → qg R :=
+  quotient_unary_map has_inv.inv (λg g' r, quotient_rel_resp_inv r)
+  definition quotient_mul [unfold 3 4] : qg R → qg R → qg R :=
+  quotient_binary_map has_mul.mul (λg g' r h h' r', quotient_rel_resp_mul r r')
+
+  section
+  local notation 1 := quotient_one
+  local postfix ⁻¹ := quotient_inv
+  local infix * := quotient_mul
+
+  theorem quotient_mul_assoc (g₁ g₂ g₃ : qg R) : g₁ * g₂ * g₃ = g₁ * (g₂ * g₃) :=
+  begin
+    refine set_quotient.rec_hprop _ g₁,
+    refine set_quotient.rec_hprop _ g₂,
+    refine set_quotient.rec_hprop _ g₃,
+    clear g₁ g₂ g₃, intro g₁ g₂ g₃,
+    exact ap class_of !mul.assoc
+  end
+
+  theorem quotient_one_mul (g : qg R) : 1 * g = g :=
+  begin
+    refine set_quotient.rec_hprop _ g, clear g, intro g,
+    exact ap class_of !one_mul
+  end
+
+  theorem quotient_mul_one (g : qg R) : g * 1 = g :=
+  begin
+    refine set_quotient.rec_hprop _ g, clear g, intro g,
+    exact ap class_of !mul_one
+  end
+
+  theorem quotient_mul_left_inv (g : qg R) : g⁻¹ * g = 1 :=
+  begin
+    refine set_quotient.rec_hprop _ g, clear g, intro g,
+    exact ap class_of !mul.left_inv
+  end
+
+  theorem quotient_mul_comm {G : CommGroup} {R : normal_subgroup G} (g h : qg R)
+    : g * h = h * g :=
+  begin
+    refine set_quotient.rec_hprop _ g, clear g, intro g,
+    refine set_quotient.rec_hprop _ h, clear h, intro h,
+    apply ap class_of, esimp, apply mul.comm
+  end
+
+  end
+
+  variable (R)
+  definition group_qg [constructor] : group (qg R) :=
+  group.mk quotient_mul _ quotient_mul_assoc quotient_one quotient_one_mul quotient_mul_one
+           quotient_inv quotient_mul_left_inv
+
+  definition quotient_group [constructor] : Group :=
+  Group.mk _ (group_qg R)
+
+  definition comm_group_qg [constructor] {G : CommGroup} (R : normal_subgroup G)
+    : comm_group (qg R) :=
+  ⦃comm_group, group_qg R, mul_comm := quotient_mul_comm⦄
+
+  definition quotient_comm_group [constructor] {G : CommGroup} (R : normal_subgroup G)
+    : CommGroup :=
+  CommGroup.mk _ (comm_group_qg R)
+
+end group