From 6da27d3121ed8e75ed219bb1a207ea500f32ff2d Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 20 Nov 2015 12:25:29 -0500 Subject: [PATCH] feat(group_theory): start on group theory, define quotient group --- group_theory.hlean | 168 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 168 insertions(+) create mode 100644 group_theory.hlean diff --git a/group_theory.hlean b/group_theory.hlean new file mode 100644 index 0000000..eaf63b2 --- /dev/null +++ b/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