From 392590bec8547644b6889bae82a8431024c4dbbb Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Fri, 16 Sep 2016 02:03:58 -0400 Subject: [PATCH] working with Ulrik on basic group theory --- algebra/group_constructions.hlean | 56 +++++++++++++++++++++++++------ 1 file changed, 46 insertions(+), 10 deletions(-) diff --git a/algebra/group_constructions.hlean b/algebra/group_constructions.hlean index fe40ead..fb233ac 100644 --- a/algebra/group_constructions.hlean +++ b/algebra/group_constructions.hlean @@ -155,7 +155,7 @@ namespace group CommGroup.mk _ (comm_group_qg (normal_subgroup_rel_comm N)) definition gq_map : G →g quotient_group N := - sorry + homomorphism.mk class_of (λ g h, idp) namespace quotient notation `⟦`:max a `⟧`:0 := gq_map a _ @@ -165,20 +165,56 @@ namespace group variable {N} definition gq_map_eq_one (g : G) (H : N g) : gq_map N g = 1 := - sorry + 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 := - sorry + 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 glift (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : quotient_group N →g G' := - sorry + 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 glift_gq_map (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : glift f H ∘g gq_map N ~ f := - sorry + 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) (g : quotient_group N →g G') : - g ~ glift f H := - sorry + 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) :=