From 038bbb8be3094244b0b2dd09fc72caef65e4efc4 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Thu, 13 Oct 2016 15:04:57 -0400 Subject: [PATCH] split group_constructions into several files --- algebra/direct_sum.hlean | 33 ++ algebra/free_commutative_group.hlean | 194 +++++++++ algebra/free_group.hlean | 179 ++++++++ algebra/group_constructions.hlean | 630 +-------------------------- algebra/product_group.hlean | 63 +++ algebra/quotient_group.hlean | 237 ++++++++++ 6 files changed, 707 insertions(+), 629 deletions(-) create mode 100644 algebra/direct_sum.hlean create mode 100644 algebra/free_commutative_group.hlean create mode 100644 algebra/free_group.hlean create mode 100644 algebra/product_group.hlean create mode 100644 algebra/quotient_group.hlean diff --git a/algebra/direct_sum.hlean b/algebra/direct_sum.hlean new file mode 100644 index 0000000..baf2e54 --- /dev/null +++ b/algebra/direct_sum.hlean @@ -0,0 +1,33 @@ +/- +Copyright (c) 2015 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Floris van Doorn, Egbert Rijke + +Constructions with groups +-/ + +import algebra.group_theory hit.set_quotient types.list types.sum .subgroup .quotient_group .product_group .free_group .free_commutative_group + +open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function + equiv +namespace group + + variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G} + {A B : CommGroup} + + variables (X : Set) {l l' : list (X ⊎ X)} + + section + + parameters {I : Set} (Y : I → CommGroup) + + definition dirsum_carrier : CommGroup := free_comm_group (trunctype.mk (Σi, Y i) _) + local abbreviation ι := @free_comm_group_inclusion + inductive dirsum_rel : dirsum_carrier → Type := + | rmk : Πi y₁ y₂, dirsum_rel (ι ⟨i, y₁⟩ * ι ⟨i, y₂⟩ * (ι ⟨i, y₁ * y₂⟩)⁻¹) + + definition direct_sum : CommGroup := quotient_comm_group_gen dirsum_carrier (λg, ∥dirsum_rel g∥) + + end + +end group diff --git a/algebra/free_commutative_group.hlean b/algebra/free_commutative_group.hlean new file mode 100644 index 0000000..0598918 --- /dev/null +++ b/algebra/free_commutative_group.hlean @@ -0,0 +1,194 @@ +/- +Copyright (c) 2015 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Floris van Doorn, Egbert Rijke + +Constructions with groups +-/ + +import algebra.group_theory hit.set_quotient types.list types.sum .subgroup .quotient_group .product_group .free_group + +open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function + equiv +namespace group + + variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G} + {A B : CommGroup} + + variables (X : Set) {l l' : list (X ⊎ X)} + + /- Free Commutative Group of a set -/ + namespace free_comm_group + + inductive fcg_rel : list (X ⊎ X) → list (X ⊎ X) → Type := + | rrefl : Πl, fcg_rel l l + | cancel1 : Πx, fcg_rel [inl x, inr x] [] + | cancel2 : Πx, fcg_rel [inr x, inl x] [] + | rflip : Πx y, fcg_rel [x, y] [y, x] + | resp_append : Π{l₁ l₂ l₃ l₄}, fcg_rel l₁ l₂ → fcg_rel l₃ l₄ → + fcg_rel (l₁ ++ l₃) (l₂ ++ l₄) + | rtrans : Π{l₁ l₂ l₃}, fcg_rel l₁ l₂ → fcg_rel l₂ l₃ → + fcg_rel l₁ l₃ + + open fcg_rel + local abbreviation R [reducible] := fcg_rel + attribute fcg_rel.rrefl [refl] + attribute fcg_rel.rtrans [trans] + + definition fcg_carrier [reducible] : Type := set_quotient (λx y, ∥R X x y∥) + local abbreviation FG := fcg_carrier + + definition is_reflexive_R : is_reflexive (λx y, ∥R X x y∥) := + begin constructor, intro s, apply tr, unfold R end + local attribute is_reflexive_R [instance] + + variable {X} + theorem rel_respect_flip (r : R X l l') : R X (map sum.flip l) (map sum.flip l') := + begin + induction r with l x x x y l₁ l₂ l₃ l₄ r₁ r₂ IH₁ IH₂ l₁ l₂ l₃ r₁ r₂ IH₁ IH₂, + { reflexivity}, + { repeat esimp [map], exact cancel2 x}, + { repeat esimp [map], exact cancel1 x}, + { repeat esimp [map], apply rflip}, + { rewrite [+map_append], exact resp_append IH₁ IH₂}, + { exact rtrans IH₁ IH₂} + end + + theorem rel_respect_reverse (r : R X l l') : R X (reverse l) (reverse l') := + begin + induction r with l x x x y l₁ l₂ l₃ l₄ r₁ r₂ IH₁ IH₂ l₁ l₂ l₃ r₁ r₂ IH₁ IH₂, + { reflexivity}, + { repeat esimp [map], exact cancel2 x}, + { repeat esimp [map], exact cancel1 x}, + { repeat esimp [map], apply rflip}, + { rewrite [+reverse_append], exact resp_append IH₂ IH₁}, + { exact rtrans IH₁ IH₂} + end + + theorem rel_cons_concat (l s) : R X (s :: l) (concat s l) := + begin + induction l with t l IH, + { reflexivity}, + { rewrite [concat_cons], transitivity (t :: s :: l), + { exact resp_append !rflip !rrefl}, + { exact resp_append (rrefl [t]) IH}} + end + + definition fcg_one [constructor] : FG X := class_of [] + definition fcg_inv [unfold 3] : FG X → FG X := + quotient_unary_map (reverse ∘ map sum.flip) + (λl l', trunc_functor -1 (rel_respect_reverse ∘ rel_respect_flip)) + definition fcg_mul [unfold 3 4] : FG X → FG X → FG X := + quotient_binary_map append (λl l', trunc.elim (λr m m', trunc.elim (λs, tr (resp_append r s)))) + + section + local notation 1 := fcg_one + local postfix ⁻¹ := fcg_inv + local infix * := fcg_mul + + theorem fcg_mul_assoc (g₁ g₂ g₃ : FG X) : g₁ * g₂ * g₃ = g₁ * (g₂ * g₃) := + begin + refine set_quotient.rec_prop _ g₁, + refine set_quotient.rec_prop _ g₂, + refine set_quotient.rec_prop _ g₃, + clear g₁ g₂ g₃, intro g₁ g₂ g₃, + exact ap class_of !append.assoc + end + + theorem fcg_one_mul (g : FG X) : 1 * g = g := + begin + refine set_quotient.rec_prop _ g, clear g, intro g, + exact ap class_of !append_nil_left + end + + theorem fcg_mul_one (g : FG X) : g * 1 = g := + begin + refine set_quotient.rec_prop _ g, clear g, intro g, + exact ap class_of !append_nil_right + end + + theorem fcg_mul_left_inv (g : FG X) : g⁻¹ * g = 1 := + begin + refine set_quotient.rec_prop _ g, clear g, intro g, + apply eq_of_rel, apply tr, + induction g with s l IH, + { reflexivity}, + { rewrite [▸*, map_cons, reverse_cons, concat_append], + refine rtrans _ IH, + apply resp_append, reflexivity, + change R X ([flip s, s] ++ l) ([] ++ l), + apply resp_append, + induction s, apply cancel2, apply cancel1, + reflexivity} + end + + theorem fcg_mul_comm (g h : FG X) : g * h = h * g := + begin + refine set_quotient.rec_prop _ g, clear g, intro g, + refine set_quotient.rec_prop _ h, clear h, intro h, + apply eq_of_rel, apply tr, + revert h, induction g with s l IH: intro h, + { rewrite [append_nil_left, append_nil_right]}, + { rewrite [append_cons,-concat_append], + transitivity concat s (l ++ h), apply rel_cons_concat, + rewrite [-append_concat], apply IH} + end + end + end free_comm_group open free_comm_group + + variables (X) + definition group_free_comm_group [constructor] : comm_group (fcg_carrier X) := + comm_group.mk fcg_mul _ fcg_mul_assoc fcg_one fcg_one_mul fcg_mul_one + fcg_inv fcg_mul_left_inv fcg_mul_comm + + definition free_comm_group [constructor] : CommGroup := + CommGroup.mk _ (group_free_comm_group X) + + /- The universal property of the free commutative group -/ + variables {X A} + definition free_comm_group_inclusion [constructor] (x : X) : free_comm_group X := + class_of [inl x] + + theorem fgh_helper_respect_comm_rel (f : X → A) (r : fcg_rel X l l') + : Π(g : A), foldl (fgh_helper f) g l = foldl (fgh_helper f) g l' := + begin + induction r with l x x x y l₁ l₂ l₃ l₄ r₁ r₂ IH₁ IH₂ l₁ l₂ l₃ r₁ r₂ IH₁ IH₂: intro g, + { reflexivity}, + { unfold [foldl], apply mul_inv_cancel_right}, + { unfold [foldl], apply inv_mul_cancel_right}, + { unfold [foldl, fgh_helper], apply mul.right_comm}, + { rewrite [+foldl_append, IH₁, IH₂]}, + { exact !IH₁ ⬝ !IH₂} + end + + definition free_comm_group_hom [constructor] (f : X → A) : free_comm_group X →g A := + begin + fapply homomorphism.mk, + { intro g, refine set_quotient.elim _ _ g, + { intro l, exact foldl (fgh_helper f) 1 l}, + { intro l l' r, esimp at *, refine trunc.rec _ r, clear r, intro r, + exact fgh_helper_respect_comm_rel f r 1}}, + { refine set_quotient.rec_prop _, intro l, refine set_quotient.rec_prop _, intro l', + esimp, refine !foldl_append ⬝ _, esimp, apply fgh_helper_mul} + end + + definition fn_of_free_comm_group_hom [unfold_full] (φ : free_comm_group X →g A) : X → A := + φ ∘ free_comm_group_inclusion + + variables (X A) + definition free_comm_group_hom_equiv_fn : (free_comm_group X →g A) ≃ (X → A) := + begin + fapply equiv.MK, + { exact fn_of_free_comm_group_hom}, + { exact free_comm_group_hom}, + { intro f, apply eq_of_homotopy, intro x, esimp, unfold [foldl], apply one_mul}, + { intro φ, apply homomorphism_eq, refine set_quotient.rec_prop _, intro l, esimp, + induction l with s l IH, + { esimp [foldl], symmetry, exact to_respect_one φ}, + { rewrite [foldl_cons, fgh_helper_mul], + refine _ ⬝ (to_respect_mul φ (class_of [s]) (class_of l))⁻¹, + rewrite [▸*,IH], induction s: rewrite [▸*, one_mul], apply ap (λx, x * _), + exact !to_respect_inv⁻¹}} + end + +end group diff --git a/algebra/free_group.hlean b/algebra/free_group.hlean new file mode 100644 index 0000000..ed2ca84 --- /dev/null +++ b/algebra/free_group.hlean @@ -0,0 +1,179 @@ +/- +Copyright (c) 2015 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Floris van Doorn, Egbert Rijke + +Constructions with groups +-/ + +import algebra.group_theory hit.set_quotient types.list types.sum .subgroup .quotient_group .product_group + +open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function + equiv +namespace group + + variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G} + {A B : CommGroup} + + /- Free Group of a set -/ + variables (X : Set) {l l' : list (X ⊎ X)} + namespace free_group + + inductive free_group_rel : list (X ⊎ X) → list (X ⊎ X) → Type := + | rrefl : Πl, free_group_rel l l + | cancel1 : Πx, free_group_rel [inl x, inr x] [] + | cancel2 : Πx, free_group_rel [inr x, inl x] [] + | resp_append : Π{l₁ l₂ l₃ l₄}, free_group_rel l₁ l₂ → free_group_rel l₃ l₄ → + free_group_rel (l₁ ++ l₃) (l₂ ++ l₄) + | rtrans : Π{l₁ l₂ l₃}, free_group_rel l₁ l₂ → free_group_rel l₂ l₃ → + free_group_rel l₁ l₃ + + open free_group_rel + local abbreviation R [reducible] := free_group_rel + attribute free_group_rel.rrefl [refl] + + definition free_group_carrier [reducible] : Type := set_quotient (λx y, ∥R X x y∥) + local abbreviation FG := free_group_carrier + + definition is_reflexive_R : is_reflexive (λx y, ∥R X x y∥) := + begin constructor, intro s, apply tr, unfold R end + local attribute is_reflexive_R [instance] + + variable {X} + theorem rel_respect_flip (r : R X l l') : R X (map sum.flip l) (map sum.flip l') := + begin + induction r with l x x l₁ l₂ l₃ l₄ r₁ r₂ IH₁ IH₂ l₁ l₂ l₃ r₁ r₂ IH₁ IH₂, + { reflexivity}, + { repeat esimp [map], exact cancel2 x}, + { repeat esimp [map], exact cancel1 x}, + { rewrite [+map_append], exact resp_append IH₁ IH₂}, + { exact rtrans IH₁ IH₂} + end + + theorem rel_respect_reverse (r : R X l l') : R X (reverse l) (reverse l') := + begin + induction r with l x x l₁ l₂ l₃ l₄ r₁ r₂ IH₁ IH₂ l₁ l₂ l₃ r₁ r₂ IH₁ IH₂, + { reflexivity}, + { repeat esimp [map], exact cancel2 x}, + { repeat esimp [map], exact cancel1 x}, + { rewrite [+reverse_append], exact resp_append IH₂ IH₁}, + { exact rtrans IH₁ IH₂} + end + + definition free_group_one [constructor] : FG X := class_of [] + definition free_group_inv [unfold 3] : FG X → FG X := + quotient_unary_map (reverse ∘ map sum.flip) + (λl l', trunc_functor -1 (rel_respect_reverse ∘ rel_respect_flip)) + definition free_group_mul [unfold 3 4] : FG X → FG X → FG X := + quotient_binary_map append (λl l', trunc.elim (λr m m', trunc.elim (λs, tr (resp_append r s)))) + + section + local notation 1 := free_group_one + local postfix ⁻¹ := free_group_inv + local infix * := free_group_mul + + theorem free_group_mul_assoc (g₁ g₂ g₃ : FG X) : g₁ * g₂ * g₃ = g₁ * (g₂ * g₃) := + begin + refine set_quotient.rec_prop _ g₁, + refine set_quotient.rec_prop _ g₂, + refine set_quotient.rec_prop _ g₃, + clear g₁ g₂ g₃, intro g₁ g₂ g₃, + exact ap class_of !append.assoc + end + + theorem free_group_one_mul (g : FG X) : 1 * g = g := + begin + refine set_quotient.rec_prop _ g, clear g, intro g, + exact ap class_of !append_nil_left + end + + theorem free_group_mul_one (g : FG X) : g * 1 = g := + begin + refine set_quotient.rec_prop _ g, clear g, intro g, + exact ap class_of !append_nil_right + end + + theorem free_group_mul_left_inv (g : FG X) : g⁻¹ * g = 1 := + begin + refine set_quotient.rec_prop _ g, clear g, intro g, + apply eq_of_rel, apply tr, + induction g with s l IH, + { reflexivity}, + { rewrite [▸*, map_cons, reverse_cons, concat_append], + refine rtrans _ IH, + apply resp_append, reflexivity, + change R X ([flip s, s] ++ l) ([] ++ l), + apply resp_append, + induction s, apply cancel2, apply cancel1, + reflexivity} + end + + end + end free_group open free_group +-- export [reduce_hints] free_group + variables (X) + definition group_free_group [constructor] : group (free_group_carrier X) := + group.mk free_group_mul _ free_group_mul_assoc free_group_one free_group_one_mul free_group_mul_one + free_group_inv free_group_mul_left_inv + + definition free_group [constructor] : Group := + Group.mk _ (group_free_group X) + + /- The universal property of the free group -/ + variables {X G} + definition free_group_inclusion [constructor] (x : X) : free_group X := + class_of [inl x] + + definition fgh_helper [unfold 5] (f : X → G) (g : G) (x : X + X) : G := + g * sum.rec (λx, f x) (λx, (f x)⁻¹) x + + theorem fgh_helper_respect_rel (f : X → G) (r : free_group_rel X l l') + : Π(g : G), foldl (fgh_helper f) g l = foldl (fgh_helper f) g l' := + begin + induction r with l x x l₁ l₂ l₃ l₄ r₁ r₂ IH₁ IH₂ l₁ l₂ l₃ r₁ r₂ IH₁ IH₂: intro g, + { reflexivity}, + { unfold [foldl], apply mul_inv_cancel_right}, + { unfold [foldl], apply inv_mul_cancel_right}, + { rewrite [+foldl_append, IH₁, IH₂]}, + { exact !IH₁ ⬝ !IH₂} + end + + theorem fgh_helper_mul (f : X → G) (l) + : Π(g : G), foldl (fgh_helper f) g l = g * foldl (fgh_helper f) 1 l := + begin + induction l with s l IH: intro g, + { unfold [foldl], exact !mul_one⁻¹}, + { rewrite [+foldl_cons, IH], refine _ ⬝ (ap (λx, g * x) !IH⁻¹), + rewrite [-mul.assoc, ↑fgh_helper, one_mul]} + end + + definition free_group_hom [constructor] (f : X → G) : free_group X →g G := + begin + fapply homomorphism.mk, + { intro g, refine set_quotient.elim _ _ g, + { intro l, exact foldl (fgh_helper f) 1 l}, + { intro l l' r, esimp at *, refine trunc.rec _ r, clear r, intro r, + exact fgh_helper_respect_rel f r 1}}, + { refine set_quotient.rec_prop _, intro l, refine set_quotient.rec_prop _, intro l', + esimp, refine !foldl_append ⬝ _, esimp, apply fgh_helper_mul} + end + + definition fn_of_free_group_hom [unfold_full] (φ : free_group X →g G) : X → G := + φ ∘ free_group_inclusion + + variables (X G) + definition free_group_hom_equiv_fn : (free_group X →g G) ≃ (X → G) := + begin + fapply equiv.MK, + { exact fn_of_free_group_hom}, + { exact free_group_hom}, + { intro f, apply eq_of_homotopy, intro x, esimp, unfold [foldl], apply one_mul}, + { intro φ, apply homomorphism_eq, refine set_quotient.rec_prop _, intro l, esimp, + induction l with s l IH, + { esimp [foldl], exact (respect_one φ)⁻¹}, + { rewrite [foldl_cons, fgh_helper_mul], + refine _ ⬝ (respect_mul φ (class_of [s]) (class_of l))⁻¹, + rewrite [IH], induction s: rewrite [▸*, one_mul], rewrite [-respect_inv φ]}} + end + + end group diff --git a/algebra/group_constructions.hlean b/algebra/group_constructions.hlean index 753cb99..371001d 100644 --- a/algebra/group_constructions.hlean +++ b/algebra/group_constructions.hlean @@ -6,644 +6,16 @@ Authors: Floris van Doorn, Egbert Rijke Constructions with groups -/ -import algebra.group_theory hit.set_quotient types.list types.sum .subgroup +import algebra.group_theory hit.set_quotient types.list types.sum .subgroup .quotient_group .product_group .free_group .free_commutative_group .direct_sum open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function equiv namespace group - definition aut.{u} (G : Group.{u}) : Group.{u} := - begin - fapply Group.mk, - exact (G ≃g G), - fapply group.mk, - { intros e f, fapply isomorphism.mk, exact f ∘g e, exact is_equiv.is_equiv_compose f e}, - { /-is_set G ≃g G-/ exact sorry}, - { /-associativity-/ intros e f g, exact sorry}, - { /-identity-/ fapply isomorphism.mk, exact sorry, exact sorry}, - { /-identity is left unit-/ exact sorry}, - { /-identity is right unit-/ exact sorry}, - { /-inverses-/ exact sorry}, - { /-inverse is right inverse?-/ exact sorry}, - end - - -- definition inner_aut (G : Group) : G →g (G ≃g G) := sorry /-- h ↦ h * g * h⁻¹ --/ - - variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G} {A B : CommGroup} - /- Quotient Group -/ - - definition quotient_rel (g h : G) : Prop := N (g * h⁻¹) - - variable {N} - - -- We prove that quotient_rel is an equivalence relation - theorem quotient_rel_refl (g : G) : quotient_rel N g g := - transport (λx, N x) !mul.right_inv⁻¹ (subgroup_has_one N) - - theorem quotient_rel_symm (r : quotient_rel N g h) : quotient_rel N h g := - transport (λx, N x) (!mul_inv ⬝ ap (λx, x * _) !inv_inv) (subgroup_respect_inv N r) - - theorem quotient_rel_trans (r : quotient_rel N g h) (s : quotient_rel N h k) - : quotient_rel N g k := - have H1 : N ((g * h⁻¹) * (h * k⁻¹)), from subgroup_respect_mul N 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 N (g * k⁻¹), from H2 ▸ H1 - - theorem is_equivalence_quotient_rel : is_equivalence (quotient_rel N) := - is_equivalence.mk quotient_rel_refl - (λg h, quotient_rel_symm) - (λg h k, quotient_rel_trans) - - -- We prove that quotient_rel respects inverses and multiplication, so - -- it is a congruence relation - theorem quotient_rel_resp_inv (r : quotient_rel N g h) : quotient_rel N g⁻¹ h⁻¹ := - have H1 : N (g⁻¹ * (h * g⁻¹) * g), from - is_normal_subgroup' N 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 N (g⁻¹ * h⁻¹⁻¹), from H2 ▸ H1 - - theorem quotient_rel_resp_mul (r : quotient_rel N g h) (r' : quotient_rel N g' h') - : quotient_rel N (g * g') (h * h') := - have H1 : N (g * ((g' * h'⁻¹) * h⁻¹)), from - normal_subgroup_insert N 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 N ((g * g') * (h * h')⁻¹), from transport (λx, N x) H2 H1 - - local attribute is_equivalence_quotient_rel [instance] - - variable (N) - - definition qg : Type := set_quotient (quotient_rel N) - - variable {N} - - local attribute qg [reducible] - - definition quotient_one [constructor] : qg N := class_of one - definition quotient_inv [unfold 3] : qg N → qg N := - quotient_unary_map has_inv.inv (λg g' r, quotient_rel_resp_inv r) - definition quotient_mul [unfold 3 4] : qg N → qg N → qg N := - 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 N) : g₁ * g₂ * g₃ = g₁ * (g₂ * g₃) := - begin - refine set_quotient.rec_prop _ g₁, - refine set_quotient.rec_prop _ g₂, - refine set_quotient.rec_prop _ g₃, - clear g₁ g₂ g₃, intro g₁ g₂ g₃, - exact ap class_of !mul.assoc - end - - theorem quotient_one_mul (g : qg N) : 1 * g = g := - begin - refine set_quotient.rec_prop _ g, clear g, intro g, - exact ap class_of !one_mul - end - - theorem quotient_mul_one (g : qg N) : g * 1 = g := - begin - refine set_quotient.rec_prop _ g, clear g, intro g, - exact ap class_of !mul_one - end - - theorem quotient_mul_left_inv (g : qg N) : g⁻¹ * g = 1 := - begin - refine set_quotient.rec_prop _ g, clear g, intro g, - exact ap class_of !mul.left_inv - end - - theorem quotient_mul_comm {G : CommGroup} {N : normal_subgroup_rel G} (g h : qg N) - : g * h = h * g := - begin - refine set_quotient.rec_prop _ g, clear g, intro g, - refine set_quotient.rec_prop _ h, clear h, intro h, - apply ap class_of, esimp, apply mul.comm - end - - end - - variable (N) - definition group_qg [constructor] : group (qg N) := - 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 N) - - definition comm_group_qg [constructor] {G : CommGroup} (N : normal_subgroup_rel G) - : comm_group (qg N) := - ⦃comm_group, group_qg N, mul_comm := quotient_mul_comm⦄ - - definition quotient_comm_group [constructor] {G : CommGroup} (N : subgroup_rel G) - : CommGroup := - CommGroup.mk _ (comm_group_qg (normal_subgroup_rel_comm N)) - - definition gq_map : G →g quotient_group N := - homomorphism.mk class_of (λ g h, idp) - - namespace quotient - notation `⟦`:max a `⟧`:0 := gq_map a _ - end quotient - - open quotient - variable {N} - - definition gq_map_eq_one (g : G) (H : N g) : gq_map N g = 1 := - begin - apply eq_of_rel, - have e : (g * 1⁻¹ = g), - from calc - g * 1⁻¹ = g * 1 : one_inv - ... = g : mul_one, - unfold quotient_rel, rewrite e, exact H - end - - definition rel_of_gq_map_eq_one (g : G) (H : gq_map N g = 1) : N g := - begin - have e : (g * 1⁻¹ = g), - from calc - g * 1⁻¹ = g * 1 : one_inv - ... = g : mul_one, - rewrite (inverse e), - apply rel_of_eq _ H - end - - definition quotient_group_elim (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : quotient_group N →g G' := - begin - fapply homomorphism.mk, - -- define function - { apply set_quotient.elim f, - intro g h K, - apply eq_of_mul_inv_eq_one, - have e : f (g * h⁻¹) = f g * (f h)⁻¹, - from calc - f (g * h⁻¹) = f g * (f h⁻¹) : to_respect_mul - ... = f g * (f h)⁻¹ : to_respect_inv, - rewrite (inverse e), - apply H, exact K}, - { intro g h, induction g using set_quotient.rec_prop with g, - induction h using set_quotient.rec_prop with h, - krewrite (inverse (to_respect_mul (gq_map N) g h)), - unfold gq_map, esimp, exact to_respect_mul f g h } - end - - definition quotient_group_compute (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : quotient_group_elim f H ∘g gq_map N ~ f := - begin - intro g, reflexivity - end - - definition glift_unique (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) (k : quotient_group N →g G') - : ( k ∘g gq_map N ~ f ) → k ~ quotient_group_elim f H := - begin - intro K cg, induction cg using set_quotient.rec_prop with g, - krewrite (quotient_group_compute f), - exact K g - end - - definition gq_universal_property (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : - is_contr (Σ(g : quotient_group N →g G'), g ∘g gq_map N = f) := - sorry - - /- Binary products (direct product) of Groups -/ - definition product_one [constructor] : G × G' := (one, one) - definition product_inv [unfold 3] : G × G' → G × G' := - λv, (v.1⁻¹, v.2⁻¹) - definition product_mul [unfold 3 4] : G × G' → G × G' → G × G' := - λv w, (v.1 * w.1, v.2 * w.2) - - section - local notation 1 := product_one - local postfix ⁻¹ := product_inv - local infix * := product_mul - - theorem product_mul_assoc (g₁ g₂ g₃ : G × G') : g₁ * g₂ * g₃ = g₁ * (g₂ * g₃) := - prod_eq !mul.assoc !mul.assoc - - theorem product_one_mul (g : G × G') : 1 * g = g := - prod_eq !one_mul !one_mul - - theorem product_mul_one (g : G × G') : g * 1 = g := - prod_eq !mul_one !mul_one - - theorem product_mul_left_inv (g : G × G') : g⁻¹ * g = 1 := - prod_eq !mul.left_inv !mul.left_inv - - theorem product_mul_comm {G G' : CommGroup} (g h : G × G') : g * h = h * g := - prod_eq !mul.comm !mul.comm - - end - - variables (G G') - definition group_prod [constructor] : group (G × G') := - group.mk product_mul _ product_mul_assoc product_one product_one_mul product_mul_one - product_inv product_mul_left_inv - - definition product [constructor] : Group := - Group.mk _ (group_prod G G') - - definition comm_group_prod [constructor] (G G' : CommGroup) : comm_group (G × G') := - ⦃comm_group, group_prod G G', mul_comm := product_mul_comm⦄ - - definition comm_product [constructor] (G G' : CommGroup) : CommGroup := - CommGroup.mk _ (comm_group_prod G G') - - infix ` ×g `:30 := group.product - - /- Free Group of a set -/ variables (X : Set) {l l' : list (X ⊎ X)} - namespace free_group - - inductive free_group_rel : list (X ⊎ X) → list (X ⊎ X) → Type := - | rrefl : Πl, free_group_rel l l - | cancel1 : Πx, free_group_rel [inl x, inr x] [] - | cancel2 : Πx, free_group_rel [inr x, inl x] [] - | resp_append : Π{l₁ l₂ l₃ l₄}, free_group_rel l₁ l₂ → free_group_rel l₃ l₄ → - free_group_rel (l₁ ++ l₃) (l₂ ++ l₄) - | rtrans : Π{l₁ l₂ l₃}, free_group_rel l₁ l₂ → free_group_rel l₂ l₃ → - free_group_rel l₁ l₃ - - open free_group_rel - local abbreviation R [reducible] := free_group_rel - attribute free_group_rel.rrefl [refl] - - definition free_group_carrier [reducible] : Type := set_quotient (λx y, ∥R X x y∥) - local abbreviation FG := free_group_carrier - - definition is_reflexive_R : is_reflexive (λx y, ∥R X x y∥) := - begin constructor, intro s, apply tr, unfold R end - local attribute is_reflexive_R [instance] - - variable {X} - theorem rel_respect_flip (r : R X l l') : R X (map sum.flip l) (map sum.flip l') := - begin - induction r with l x x l₁ l₂ l₃ l₄ r₁ r₂ IH₁ IH₂ l₁ l₂ l₃ r₁ r₂ IH₁ IH₂, - { reflexivity}, - { repeat esimp [map], exact cancel2 x}, - { repeat esimp [map], exact cancel1 x}, - { rewrite [+map_append], exact resp_append IH₁ IH₂}, - { exact rtrans IH₁ IH₂} - end - - theorem rel_respect_reverse (r : R X l l') : R X (reverse l) (reverse l') := - begin - induction r with l x x l₁ l₂ l₃ l₄ r₁ r₂ IH₁ IH₂ l₁ l₂ l₃ r₁ r₂ IH₁ IH₂, - { reflexivity}, - { repeat esimp [map], exact cancel2 x}, - { repeat esimp [map], exact cancel1 x}, - { rewrite [+reverse_append], exact resp_append IH₂ IH₁}, - { exact rtrans IH₁ IH₂} - end - - definition free_group_one [constructor] : FG X := class_of [] - definition free_group_inv [unfold 3] : FG X → FG X := - quotient_unary_map (reverse ∘ map sum.flip) - (λl l', trunc_functor -1 (rel_respect_reverse ∘ rel_respect_flip)) - definition free_group_mul [unfold 3 4] : FG X → FG X → FG X := - quotient_binary_map append (λl l', trunc.elim (λr m m', trunc.elim (λs, tr (resp_append r s)))) - - section - local notation 1 := free_group_one - local postfix ⁻¹ := free_group_inv - local infix * := free_group_mul - - theorem free_group_mul_assoc (g₁ g₂ g₃ : FG X) : g₁ * g₂ * g₃ = g₁ * (g₂ * g₃) := - begin - refine set_quotient.rec_prop _ g₁, - refine set_quotient.rec_prop _ g₂, - refine set_quotient.rec_prop _ g₃, - clear g₁ g₂ g₃, intro g₁ g₂ g₃, - exact ap class_of !append.assoc - end - - theorem free_group_one_mul (g : FG X) : 1 * g = g := - begin - refine set_quotient.rec_prop _ g, clear g, intro g, - exact ap class_of !append_nil_left - end - - theorem free_group_mul_one (g : FG X) : g * 1 = g := - begin - refine set_quotient.rec_prop _ g, clear g, intro g, - exact ap class_of !append_nil_right - end - - theorem free_group_mul_left_inv (g : FG X) : g⁻¹ * g = 1 := - begin - refine set_quotient.rec_prop _ g, clear g, intro g, - apply eq_of_rel, apply tr, - induction g with s l IH, - { reflexivity}, - { rewrite [▸*, map_cons, reverse_cons, concat_append], - refine rtrans _ IH, - apply resp_append, reflexivity, - change R X ([flip s, s] ++ l) ([] ++ l), - apply resp_append, - induction s, apply cancel2, apply cancel1, - reflexivity} - end - - end - end free_group open free_group --- export [reduce_hints] free_group - variables (X) - definition group_free_group [constructor] : group (free_group_carrier X) := - group.mk free_group_mul _ free_group_mul_assoc free_group_one free_group_one_mul free_group_mul_one - free_group_inv free_group_mul_left_inv - - definition free_group [constructor] : Group := - Group.mk _ (group_free_group X) - - /- The universal property of the free group -/ - variables {X G} - definition free_group_inclusion [constructor] (x : X) : free_group X := - class_of [inl x] - - definition fgh_helper [unfold 5] (f : X → G) (g : G) (x : X + X) : G := - g * sum.rec (λx, f x) (λx, (f x)⁻¹) x - - theorem fgh_helper_respect_rel (f : X → G) (r : free_group_rel X l l') - : Π(g : G), foldl (fgh_helper f) g l = foldl (fgh_helper f) g l' := - begin - induction r with l x x l₁ l₂ l₃ l₄ r₁ r₂ IH₁ IH₂ l₁ l₂ l₃ r₁ r₂ IH₁ IH₂: intro g, - { reflexivity}, - { unfold [foldl], apply mul_inv_cancel_right}, - { unfold [foldl], apply inv_mul_cancel_right}, - { rewrite [+foldl_append, IH₁, IH₂]}, - { exact !IH₁ ⬝ !IH₂} - end - - theorem fgh_helper_mul (f : X → G) (l) - : Π(g : G), foldl (fgh_helper f) g l = g * foldl (fgh_helper f) 1 l := - begin - induction l with s l IH: intro g, - { unfold [foldl], exact !mul_one⁻¹}, - { rewrite [+foldl_cons, IH], refine _ ⬝ (ap (λx, g * x) !IH⁻¹), - rewrite [-mul.assoc, ↑fgh_helper, one_mul]} - end - - definition free_group_hom [constructor] (f : X → G) : free_group X →g G := - begin - fapply homomorphism.mk, - { intro g, refine set_quotient.elim _ _ g, - { intro l, exact foldl (fgh_helper f) 1 l}, - { intro l l' r, esimp at *, refine trunc.rec _ r, clear r, intro r, - exact fgh_helper_respect_rel f r 1}}, - { refine set_quotient.rec_prop _, intro l, refine set_quotient.rec_prop _, intro l', - esimp, refine !foldl_append ⬝ _, esimp, apply fgh_helper_mul} - end - - definition fn_of_free_group_hom [unfold_full] (φ : free_group X →g G) : X → G := - φ ∘ free_group_inclusion - - variables (X G) - definition free_group_hom_equiv_fn : (free_group X →g G) ≃ (X → G) := - begin - fapply equiv.MK, - { exact fn_of_free_group_hom}, - { exact free_group_hom}, - { intro f, apply eq_of_homotopy, intro x, esimp, unfold [foldl], apply one_mul}, - { intro φ, apply homomorphism_eq, refine set_quotient.rec_prop _, intro l, esimp, - induction l with s l IH, - { esimp [foldl], exact (respect_one φ)⁻¹}, - { rewrite [foldl_cons, fgh_helper_mul], - refine _ ⬝ (respect_mul φ (class_of [s]) (class_of l))⁻¹, - rewrite [IH], induction s: rewrite [▸*, one_mul], rewrite [-respect_inv φ]}} - end - - /- Free Commutative Group of a set -/ - namespace free_comm_group - - inductive fcg_rel : list (X ⊎ X) → list (X ⊎ X) → Type := - | rrefl : Πl, fcg_rel l l - | cancel1 : Πx, fcg_rel [inl x, inr x] [] - | cancel2 : Πx, fcg_rel [inr x, inl x] [] - | rflip : Πx y, fcg_rel [x, y] [y, x] - | resp_append : Π{l₁ l₂ l₃ l₄}, fcg_rel l₁ l₂ → fcg_rel l₃ l₄ → - fcg_rel (l₁ ++ l₃) (l₂ ++ l₄) - | rtrans : Π{l₁ l₂ l₃}, fcg_rel l₁ l₂ → fcg_rel l₂ l₃ → - fcg_rel l₁ l₃ - - open fcg_rel - local abbreviation R [reducible] := fcg_rel - attribute fcg_rel.rrefl [refl] - attribute fcg_rel.rtrans [trans] - - definition fcg_carrier [reducible] : Type := set_quotient (λx y, ∥R X x y∥) - local abbreviation FG := fcg_carrier - - definition is_reflexive_R : is_reflexive (λx y, ∥R X x y∥) := - begin constructor, intro s, apply tr, unfold R end - local attribute is_reflexive_R [instance] - - variable {X} - theorem rel_respect_flip (r : R X l l') : R X (map sum.flip l) (map sum.flip l') := - begin - induction r with l x x x y l₁ l₂ l₃ l₄ r₁ r₂ IH₁ IH₂ l₁ l₂ l₃ r₁ r₂ IH₁ IH₂, - { reflexivity}, - { repeat esimp [map], exact cancel2 x}, - { repeat esimp [map], exact cancel1 x}, - { repeat esimp [map], apply rflip}, - { rewrite [+map_append], exact resp_append IH₁ IH₂}, - { exact rtrans IH₁ IH₂} - end - - theorem rel_respect_reverse (r : R X l l') : R X (reverse l) (reverse l') := - begin - induction r with l x x x y l₁ l₂ l₃ l₄ r₁ r₂ IH₁ IH₂ l₁ l₂ l₃ r₁ r₂ IH₁ IH₂, - { reflexivity}, - { repeat esimp [map], exact cancel2 x}, - { repeat esimp [map], exact cancel1 x}, - { repeat esimp [map], apply rflip}, - { rewrite [+reverse_append], exact resp_append IH₂ IH₁}, - { exact rtrans IH₁ IH₂} - end - - theorem rel_cons_concat (l s) : R X (s :: l) (concat s l) := - begin - induction l with t l IH, - { reflexivity}, - { rewrite [concat_cons], transitivity (t :: s :: l), - { exact resp_append !rflip !rrefl}, - { exact resp_append (rrefl [t]) IH}} - end - - definition fcg_one [constructor] : FG X := class_of [] - definition fcg_inv [unfold 3] : FG X → FG X := - quotient_unary_map (reverse ∘ map sum.flip) - (λl l', trunc_functor -1 (rel_respect_reverse ∘ rel_respect_flip)) - definition fcg_mul [unfold 3 4] : FG X → FG X → FG X := - quotient_binary_map append (λl l', trunc.elim (λr m m', trunc.elim (λs, tr (resp_append r s)))) - - section - local notation 1 := fcg_one - local postfix ⁻¹ := fcg_inv - local infix * := fcg_mul - - theorem fcg_mul_assoc (g₁ g₂ g₃ : FG X) : g₁ * g₂ * g₃ = g₁ * (g₂ * g₃) := - begin - refine set_quotient.rec_prop _ g₁, - refine set_quotient.rec_prop _ g₂, - refine set_quotient.rec_prop _ g₃, - clear g₁ g₂ g₃, intro g₁ g₂ g₃, - exact ap class_of !append.assoc - end - - theorem fcg_one_mul (g : FG X) : 1 * g = g := - begin - refine set_quotient.rec_prop _ g, clear g, intro g, - exact ap class_of !append_nil_left - end - - theorem fcg_mul_one (g : FG X) : g * 1 = g := - begin - refine set_quotient.rec_prop _ g, clear g, intro g, - exact ap class_of !append_nil_right - end - - theorem fcg_mul_left_inv (g : FG X) : g⁻¹ * g = 1 := - begin - refine set_quotient.rec_prop _ g, clear g, intro g, - apply eq_of_rel, apply tr, - induction g with s l IH, - { reflexivity}, - { rewrite [▸*, map_cons, reverse_cons, concat_append], - refine rtrans _ IH, - apply resp_append, reflexivity, - change R X ([flip s, s] ++ l) ([] ++ l), - apply resp_append, - induction s, apply cancel2, apply cancel1, - reflexivity} - end - - theorem fcg_mul_comm (g h : FG X) : g * h = h * g := - begin - refine set_quotient.rec_prop _ g, clear g, intro g, - refine set_quotient.rec_prop _ h, clear h, intro h, - apply eq_of_rel, apply tr, - revert h, induction g with s l IH: intro h, - { rewrite [append_nil_left, append_nil_right]}, - { rewrite [append_cons,-concat_append], - transitivity concat s (l ++ h), apply rel_cons_concat, - rewrite [-append_concat], apply IH} - end - end - end free_comm_group open free_comm_group - - variables (X) - definition group_free_comm_group [constructor] : comm_group (fcg_carrier X) := - comm_group.mk fcg_mul _ fcg_mul_assoc fcg_one fcg_one_mul fcg_mul_one - fcg_inv fcg_mul_left_inv fcg_mul_comm - - definition free_comm_group [constructor] : CommGroup := - CommGroup.mk _ (group_free_comm_group X) - - /- The universal property of the free commutative group -/ - variables {X A} - definition free_comm_group_inclusion [constructor] (x : X) : free_comm_group X := - class_of [inl x] - - theorem fgh_helper_respect_comm_rel (f : X → A) (r : fcg_rel X l l') - : Π(g : A), foldl (fgh_helper f) g l = foldl (fgh_helper f) g l' := - begin - induction r with l x x x y l₁ l₂ l₃ l₄ r₁ r₂ IH₁ IH₂ l₁ l₂ l₃ r₁ r₂ IH₁ IH₂: intro g, - { reflexivity}, - { unfold [foldl], apply mul_inv_cancel_right}, - { unfold [foldl], apply inv_mul_cancel_right}, - { unfold [foldl, fgh_helper], apply mul.right_comm}, - { rewrite [+foldl_append, IH₁, IH₂]}, - { exact !IH₁ ⬝ !IH₂} - end - - definition free_comm_group_hom [constructor] (f : X → A) : free_comm_group X →g A := - begin - fapply homomorphism.mk, - { intro g, refine set_quotient.elim _ _ g, - { intro l, exact foldl (fgh_helper f) 1 l}, - { intro l l' r, esimp at *, refine trunc.rec _ r, clear r, intro r, - exact fgh_helper_respect_comm_rel f r 1}}, - { refine set_quotient.rec_prop _, intro l, refine set_quotient.rec_prop _, intro l', - esimp, refine !foldl_append ⬝ _, esimp, apply fgh_helper_mul} - end - - definition fn_of_free_comm_group_hom [unfold_full] (φ : free_comm_group X →g A) : X → A := - φ ∘ free_comm_group_inclusion - - variables (X A) - definition free_comm_group_hom_equiv_fn : (free_comm_group X →g A) ≃ (X → A) := - begin - fapply equiv.MK, - { exact fn_of_free_comm_group_hom}, - { exact free_comm_group_hom}, - { intro f, apply eq_of_homotopy, intro x, esimp, unfold [foldl], apply one_mul}, - { intro φ, apply homomorphism_eq, refine set_quotient.rec_prop _, intro l, esimp, - induction l with s l IH, - { esimp [foldl], symmetry, exact to_respect_one φ}, - { rewrite [foldl_cons, fgh_helper_mul], - refine _ ⬝ (to_respect_mul φ (class_of [s]) (class_of l))⁻¹, - rewrite [▸*,IH], induction s: rewrite [▸*, one_mul], apply ap (λx, x * _), - exact !to_respect_inv⁻¹}} - end - - /- set generating normal subgroup -/ - - section - - parameters {GG : CommGroup} (S : GG → Prop) - - inductive generating_relation' : GG → Type := - | rincl : Π{g}, S g → generating_relation' g - | rmul : Π{g h}, generating_relation' g → generating_relation' h → generating_relation' (g * h) - | rinv : Π{g}, generating_relation' g → generating_relation' g⁻¹ - | rone : generating_relation' 1 - open generating_relation' - definition generating_relation (g : GG) : Prop := ∥ generating_relation' g ∥ - local abbreviation R := generating_relation - definition gr_one : R 1 := tr (rone S) - definition gr_inv (g : GG) : R g → R g⁻¹ := - trunc_functor -1 rinv - definition gr_mul (g h : GG) : R g → R h → R (g * h) := - trunc_functor2 rmul - - definition normal_generating_relation : subgroup_rel GG := - ⦃ subgroup_rel, - R := generating_relation, - Rone := gr_one, - Rinv := gr_inv, - Rmul := gr_mul⦄ - - parameter (GG) - definition quotient_comm_group_gen : CommGroup := quotient_comm_group normal_generating_relation - - end - - section - - parameters {I : Set} (Y : I → CommGroup) - - definition dirsum_carrier : CommGroup := free_comm_group (trunctype.mk (Σi, Y i) _) - local abbreviation ι := @free_comm_group_inclusion - inductive dirsum_rel : dirsum_carrier → Type := - | rmk : Πi y₁ y₂, dirsum_rel (ι ⟨i, y₁⟩ * ι ⟨i, y₂⟩ * (ι ⟨i, y₁ * y₂⟩)⁻¹) - - definition direct_sum : CommGroup := quotient_comm_group_gen dirsum_carrier (λg, ∥dirsum_rel g∥) - - end /- Tensor group (WIP) -/ diff --git a/algebra/product_group.hlean b/algebra/product_group.hlean new file mode 100644 index 0000000..c585007 --- /dev/null +++ b/algebra/product_group.hlean @@ -0,0 +1,63 @@ +/- +Copyright (c) 2015 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Floris van Doorn, Egbert Rijke + +Constructions with groups +-/ + +import algebra.group_theory hit.set_quotient types.list types.sum .subgroup .quotient_group + +open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function + equiv +namespace group + + variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G} + {A B : CommGroup} + + /- Binary products (direct product) of Groups -/ + definition product_one [constructor] : G × G' := (one, one) + definition product_inv [unfold 3] : G × G' → G × G' := + λv, (v.1⁻¹, v.2⁻¹) + definition product_mul [unfold 3 4] : G × G' → G × G' → G × G' := + λv w, (v.1 * w.1, v.2 * w.2) + + section + local notation 1 := product_one + local postfix ⁻¹ := product_inv + local infix * := product_mul + + theorem product_mul_assoc (g₁ g₂ g₃ : G × G') : g₁ * g₂ * g₃ = g₁ * (g₂ * g₃) := + prod_eq !mul.assoc !mul.assoc + + theorem product_one_mul (g : G × G') : 1 * g = g := + prod_eq !one_mul !one_mul + + theorem product_mul_one (g : G × G') : g * 1 = g := + prod_eq !mul_one !mul_one + + theorem product_mul_left_inv (g : G × G') : g⁻¹ * g = 1 := + prod_eq !mul.left_inv !mul.left_inv + + theorem product_mul_comm {G G' : CommGroup} (g h : G × G') : g * h = h * g := + prod_eq !mul.comm !mul.comm + + end + + variables (G G') + definition group_prod [constructor] : group (G × G') := + group.mk product_mul _ product_mul_assoc product_one product_one_mul product_mul_one + product_inv product_mul_left_inv + + definition product [constructor] : Group := + Group.mk _ (group_prod G G') + + definition comm_group_prod [constructor] (G G' : CommGroup) : comm_group (G × G') := + ⦃comm_group, group_prod G G', mul_comm := product_mul_comm⦄ + + definition comm_product [constructor] (G G' : CommGroup) : CommGroup := + CommGroup.mk _ (comm_group_prod G G') + + infix ` ×g `:30 := group.product + +end group diff --git a/algebra/quotient_group.hlean b/algebra/quotient_group.hlean new file mode 100644 index 0000000..e9cf99b --- /dev/null +++ b/algebra/quotient_group.hlean @@ -0,0 +1,237 @@ +/- +Copyright (c) 2015 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Floris van Doorn, Egbert Rijke + +Constructions with groups +-/ + +import algebra.group_theory hit.set_quotient types.list types.sum .subgroup + +open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function + equiv +namespace group + + variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G} + {A B : CommGroup} + + /- Quotient Group -/ + + definition quotient_rel (g h : G) : Prop := N (g * h⁻¹) + + variable {N} + + -- We prove that quotient_rel is an equivalence relation + theorem quotient_rel_refl (g : G) : quotient_rel N g g := + transport (λx, N x) !mul.right_inv⁻¹ (subgroup_has_one N) + + theorem quotient_rel_symm (r : quotient_rel N g h) : quotient_rel N h g := + transport (λx, N x) (!mul_inv ⬝ ap (λx, x * _) !inv_inv) (subgroup_respect_inv N r) + + theorem quotient_rel_trans (r : quotient_rel N g h) (s : quotient_rel N h k) + : quotient_rel N g k := + have H1 : N ((g * h⁻¹) * (h * k⁻¹)), from subgroup_respect_mul N 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 N (g * k⁻¹), from H2 ▸ H1 + + theorem is_equivalence_quotient_rel : is_equivalence (quotient_rel N) := + is_equivalence.mk quotient_rel_refl + (λg h, quotient_rel_symm) + (λg h k, quotient_rel_trans) + + -- We prove that quotient_rel respects inverses and multiplication, so + -- it is a congruence relation + theorem quotient_rel_resp_inv (r : quotient_rel N g h) : quotient_rel N g⁻¹ h⁻¹ := + have H1 : N (g⁻¹ * (h * g⁻¹) * g), from + is_normal_subgroup' N 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 N (g⁻¹ * h⁻¹⁻¹), from H2 ▸ H1 + + theorem quotient_rel_resp_mul (r : quotient_rel N g h) (r' : quotient_rel N g' h') + : quotient_rel N (g * g') (h * h') := + have H1 : N (g * ((g' * h'⁻¹) * h⁻¹)), from + normal_subgroup_insert N 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 N ((g * g') * (h * h')⁻¹), from transport (λx, N x) H2 H1 + + local attribute is_equivalence_quotient_rel [instance] + + variable (N) + + definition qg : Type := set_quotient (quotient_rel N) + + variable {N} + + local attribute qg [reducible] + + definition quotient_one [constructor] : qg N := class_of one + definition quotient_inv [unfold 3] : qg N → qg N := + quotient_unary_map has_inv.inv (λg g' r, quotient_rel_resp_inv r) + definition quotient_mul [unfold 3 4] : qg N → qg N → qg N := + 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 N) : g₁ * g₂ * g₃ = g₁ * (g₂ * g₃) := + begin + refine set_quotient.rec_prop _ g₁, + refine set_quotient.rec_prop _ g₂, + refine set_quotient.rec_prop _ g₃, + clear g₁ g₂ g₃, intro g₁ g₂ g₃, + exact ap class_of !mul.assoc + end + + theorem quotient_one_mul (g : qg N) : 1 * g = g := + begin + refine set_quotient.rec_prop _ g, clear g, intro g, + exact ap class_of !one_mul + end + + theorem quotient_mul_one (g : qg N) : g * 1 = g := + begin + refine set_quotient.rec_prop _ g, clear g, intro g, + exact ap class_of !mul_one + end + + theorem quotient_mul_left_inv (g : qg N) : g⁻¹ * g = 1 := + begin + refine set_quotient.rec_prop _ g, clear g, intro g, + exact ap class_of !mul.left_inv + end + + theorem quotient_mul_comm {G : CommGroup} {N : normal_subgroup_rel G} (g h : qg N) + : g * h = h * g := + begin + refine set_quotient.rec_prop _ g, clear g, intro g, + refine set_quotient.rec_prop _ h, clear h, intro h, + apply ap class_of, esimp, apply mul.comm + end + + end + + variable (N) + definition group_qg [constructor] : group (qg N) := + 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 N) + + definition comm_group_qg [constructor] {G : CommGroup} (N : normal_subgroup_rel G) + : comm_group (qg N) := + ⦃comm_group, group_qg N, mul_comm := quotient_mul_comm⦄ + + definition quotient_comm_group [constructor] {G : CommGroup} (N : subgroup_rel G) + : CommGroup := + CommGroup.mk _ (comm_group_qg (normal_subgroup_rel_comm N)) + + definition gq_map : G →g quotient_group N := + homomorphism.mk class_of (λ g h, idp) + + namespace quotient + notation `⟦`:max a `⟧`:0 := gq_map a _ + end quotient + + open quotient + variable {N} + + definition gq_map_eq_one (g : G) (H : N g) : gq_map N g = 1 := + begin + apply eq_of_rel, + have e : (g * 1⁻¹ = g), + from calc + g * 1⁻¹ = g * 1 : one_inv + ... = g : mul_one, + unfold quotient_rel, rewrite e, exact H + end + + definition rel_of_gq_map_eq_one (g : G) (H : gq_map N g = 1) : N g := + begin + have e : (g * 1⁻¹ = g), + from calc + g * 1⁻¹ = g * 1 : one_inv + ... = g : mul_one, + rewrite (inverse e), + apply rel_of_eq _ H + end + + definition quotient_group_elim (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : quotient_group N →g G' := + begin + fapply homomorphism.mk, + -- define function + { apply set_quotient.elim f, + intro g h K, + apply eq_of_mul_inv_eq_one, + have e : f (g * h⁻¹) = f g * (f h)⁻¹, + from calc + f (g * h⁻¹) = f g * (f h⁻¹) : to_respect_mul + ... = f g * (f h)⁻¹ : to_respect_inv, + rewrite (inverse e), + apply H, exact K}, + { intro g h, induction g using set_quotient.rec_prop with g, + induction h using set_quotient.rec_prop with h, + krewrite (inverse (to_respect_mul (gq_map N) g h)), + unfold gq_map, esimp, exact to_respect_mul f g h } + end + + definition quotient_group_compute (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : quotient_group_elim f H ∘g gq_map N ~ f := + begin + intro g, reflexivity + end + + definition glift_unique (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) (k : quotient_group N →g G') + : ( k ∘g gq_map N ~ f ) → k ~ quotient_group_elim f H := + begin + intro K cg, induction cg using set_quotient.rec_prop with g, + krewrite (quotient_group_compute f), + exact K g + end + + definition gq_universal_property (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : + is_contr (Σ(g : quotient_group N →g G'), g ∘g gq_map N = f) := + sorry + + /- set generating normal subgroup -/ + + section + + parameters {GG : CommGroup} (S : GG → Prop) + + inductive generating_relation' : GG → Type := + | rincl : Π{g}, S g → generating_relation' g + | rmul : Π{g h}, generating_relation' g → generating_relation' h → generating_relation' (g * h) + | rinv : Π{g}, generating_relation' g → generating_relation' g⁻¹ + | rone : generating_relation' 1 + open generating_relation' + definition generating_relation (g : GG) : Prop := ∥ generating_relation' g ∥ + local abbreviation R := generating_relation + definition gr_one : R 1 := tr (rone S) + definition gr_inv (g : GG) : R g → R g⁻¹ := + trunc_functor -1 rinv + definition gr_mul (g h : GG) : R g → R h → R (g * h) := + trunc_functor2 rmul + + definition normal_generating_relation : subgroup_rel GG := + ⦃ subgroup_rel, + R := generating_relation, + Rone := gr_one, + Rinv := gr_inv, + Rmul := gr_mul⦄ + + parameter (GG) + definition quotient_comm_group_gen : CommGroup := quotient_comm_group normal_generating_relation + + end + + end group