From 345c45e07c7eec819c1ac44f2e30b0273e35e15a Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Fri, 30 Jun 2017 21:22:53 +0100 Subject: [PATCH] revise quotient_group --- algebra/quotient_group.hlean | 298 ++++++++++++++++++----------------- algebra/subgroup.hlean | 21 ++- property.hlean | 4 + 3 files changed, 178 insertions(+), 145 deletions(-) diff --git a/algebra/quotient_group.hlean b/algebra/quotient_group.hlean index 1b7e3e0..8958b9e 100644 --- a/algebra/quotient_group.hlean +++ b/algebra/quotient_group.hlean @@ -1,7 +1,7 @@ /- 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 +Authors: Floris van Doorn, Egbert Rijke, Jeremy Avigad Constructions with groups -/ @@ -9,11 +9,14 @@ Constructions with groups import hit.set_quotient .subgroup ..move_to_lib types.equiv open eq algebra is_trunc set_quotient relation sigma sigma.ops prod trunc function equiv is_equiv +open property namespace group - - variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G} - {N' : normal_subgroup_rel G'} + variables {G G' : Group} + (H : property G) [is_subgroup G H] + (N : property G) [is_normal_subgroup G N] + {g g' h h' k : G} + (N' : property G') [is_normal_subgroup G' N'] variables {A B : AbGroup} /- Quotient Group -/ @@ -21,20 +24,21 @@ namespace group definition homotopy_of_homomorphism_eq {f g : G →g G'}(p : f = g) : f ~ g := λx : G , ap010 group_fun p x - definition quotient_rel [constructor] (g h : G) : Prop := N (g * h⁻¹) + definition quotient_rel [constructor] (g h : G) : Prop := g * h⁻¹ ∈ N 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) + transport (λx, N x) !mul.right_inv⁻¹ (subgroup_one_mem 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) + transport (λx, N x) (!mul_inv ⬝ ap (λx, x * _) !inv_inv) + begin apply subgroup_inv_mem r end 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 H1 : N ((g * h⁻¹) * (h * k⁻¹)), from subgroup_mul_mem 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, @@ -48,18 +52,18 @@ namespace group -- 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 H1 : g⁻¹ * (h * g⁻¹) * g ∈ N, from + is_normal_subgroup' 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⁻¹⁻¹), by rewrite [-H2]; exact H1 + show g⁻¹ * h⁻¹⁻¹ ∈ N, by rewrite [-H2]; exact 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 H1 : g * ((g' * h'⁻¹) * h⁻¹) ∈ N, from + normal_subgroup_insert 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 @@ -114,7 +118,7 @@ namespace group exact ap class_of !mul.left_inv end - theorem quotient_mul_comm {G : AbGroup} {N : normal_subgroup_rel G} (g h : qg N) + theorem quotient_mul_comm {G : AbGroup} {N : property G} [is_normal_subgroup G N] (g h : qg N) : g * h = h * g := begin refine set_quotient.rec_prop _ g, clear g, intro g, @@ -132,21 +136,21 @@ namespace group definition quotient_group [constructor] : Group := Group.mk _ (group_qg N) - definition ab_group_qg [constructor] {G : AbGroup} (N : normal_subgroup_rel G) + definition ab_group_qg [constructor] {G : AbGroup} (N : property G) [is_normal_subgroup G N] : ab_group (qg N) := ⦃ab_group, group_qg N, mul_comm := quotient_mul_comm⦄ - definition quotient_ab_group [constructor] {G : AbGroup} (N : subgroup_rel G) + definition quotient_ab_group [constructor] {G : AbGroup} (N : property G) [is_subgroup G N] : AbGroup := - AbGroup.mk _ (ab_group_qg (normal_subgroup_rel_ab N)) + AbGroup.mk _ (@ab_group_qg G N (is_normal_subgroup_ab _)) definition qg_map [constructor] : G →g quotient_group N := homomorphism.mk class_of (λ g h, idp) - definition ab_qg_map {G : AbGroup} (N : subgroup_rel G) : G →g quotient_ab_group N := - qg_map _ + definition ab_qg_map {G : AbGroup} (N : property G) [is_subgroup G N] : G →g quotient_ab_group N := + @qg_map _ N (is_normal_subgroup_ab _) - definition is_surjective_ab_qg_map {A : AbGroup} (N : subgroup_rel A) : is_surjective (ab_qg_map N) := + definition is_surjective_ab_qg_map {A : AbGroup} (N : property A) [is_subgroup A N] : is_surjective (ab_qg_map N) := begin intro x, induction x, fapply image.mk, @@ -159,7 +163,7 @@ namespace group end quotient open quotient - variable {N} + variables {N N'} definition qg_map_eq_one (g : G) (H : N g) : qg_map N g = 1 := begin @@ -171,7 +175,7 @@ namespace group unfold quotient_rel, rewrite e, exact H end - definition ab_qg_map_eq_one {K : subgroup_rel A} (g :A) (H : K g) : ab_qg_map K g = 1 := + definition ab_qg_map_eq_one {K : property A} [is_subgroup A K] (g :A) (H : K g) : ab_qg_map K g = 1 := begin apply eq_of_rel, have e : (g * 1⁻¹ = g), @@ -182,7 +186,7 @@ namespace group end --- there should be a smarter way to do this!! Please have a look, Floris. - definition rel_of_qg_map_eq_one (g : G) (H : qg_map N g = 1) : N g := + definition rel_of_qg_map_eq_one (g : G) (H : qg_map N g = 1) : g ∈ N := begin have e : (g * 1⁻¹ = g), from calc @@ -192,14 +196,15 @@ namespace group apply rel_of_eq _ H end - definition rel_of_ab_qg_map_eq_one {K : subgroup_rel A} (a :A) (H : ab_qg_map K a = 1) : K a := + definition rel_of_ab_qg_map_eq_one {K : property A} [is_subgroup A K] (a :A) (H : ab_qg_map K a = 1) : a ∈ K := begin have e : (a * 1⁻¹ = a), from calc a * 1⁻¹ = a * 1 : one_inv ... = a : mul_one, rewrite (inverse e), - apply rel_of_eq _ H + have is_normal_subgroup A K, from is_normal_subgroup_ab _, + apply rel_of_eq (quotient_rel K) H end definition quotient_group_elim_fun [unfold 6] (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) @@ -216,7 +221,7 @@ namespace group apply H, exact K end - definition quotient_group_elim [constructor] (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : quotient_group N →g G' := + definition quotient_group_elim [constructor] (f : G →g G') (H : Π⦃g⦄, g ∈ N → f g = 1) : quotient_group N →g G' := begin fapply homomorphism.mk, -- define function @@ -227,24 +232,30 @@ namespace group unfold qg_map, esimp, exact to_respect_mul f g h } end + example {K : property A} [is_subgroup A K] : + quotient_ab_group K = @quotient_group A K (is_normal_subgroup_ab _) := rfl + + definition quotient_ab_group_elim [constructor] {K : property A} [is_subgroup A K] (f : A →g B) + (H : Π⦃g⦄, g ∈ K → f g = 1) : quotient_ab_group K →g B := + @quotient_group_elim A B K (is_normal_subgroup_ab _) f H + definition quotient_group_compute (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) (g : G) : quotient_group_elim f H (qg_map N g) = f g := begin reflexivity end - definition gelim_unique (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) (k : quotient_group N →g G') + definition gelim_unique (f : G →g G') (H : Π⦃g⦄, g ∈ N → f g = 1) (k : quotient_group N →g G') : ( k ∘g qg_map N ~ f ) → k ~ quotient_group_elim f H := begin intro K cg, induction cg using set_quotient.rec_prop with g, exact K g end - definition ab_gelim_unique {K : subgroup_rel A} (f : A →g B) (H : Π (a :A), K a → f a = 1) (k : quotient_ab_group K →g B) - : ( k ∘g ab_qg_map K ~ f) → k ~ quotient_group_elim f H := - begin - fapply gelim_unique, - end + definition ab_gelim_unique {K : property A} [is_subgroup A K] (f : A →g B) (H : Π (a :A), a ∈ K → f a = 1) (k : quotient_ab_group K →g B) + : ( k ∘g ab_qg_map K ~ f) → k ~ quotient_ab_group_elim f H := +--@quotient_group_elim A B K (is_normal_subgroup_ab _) f H := + @gelim_unique _ _ K (is_normal_subgroup_ab _) f H _ definition qg_universal_property (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : is_contr (Σ(g : quotient_group N →g G'), g ∘ qg_map N ~ f) := @@ -258,26 +269,27 @@ namespace group {fapply is_prop.elimo} } end - definition ab_qg_universal_property {K : subgroup_rel A} (f : A →g B) (H : Π (a :A), K a → f a = 1) : + definition ab_qg_universal_property {K : property A} [is_subgroup A K] (f : A →g B) (H : Π (a :A), K a → f a = 1) : is_contr ((Σ(g : quotient_ab_group K →g B), g ∘g ab_qg_map K ~ f) ) := begin - fapply qg_universal_property, + fapply @qg_universal_property _ _ K (is_normal_subgroup_ab _), exact H end - definition quotient_group_functor_contr {K L : subgroup_rel A} (H : Π (a : A), K a → L a) : + definition quotient_group_functor_contr {K L : property A} [is_subgroup A K] [is_subgroup A L] + (H : Π (a : A), K a → L a) : is_contr ((Σ(g : quotient_ab_group K →g quotient_ab_group L), g ∘g ab_qg_map K ~ ab_qg_map L) ) := begin fapply ab_qg_universal_property, intro a p, - fapply qg_map_eq_one, - exact H a p, + fapply ab_qg_map_eq_one, + exact H a p end - definition quotient_group_functor_id {K : subgroup_rel A} (H : Π (a : A), K a → K a) : - center' (@quotient_group_functor_contr _ K K H) = ⟨gid (quotient_ab_group K), λ x, rfl⟩ := + definition quotient_group_functor_id {K : property A} [is_subgroup A K] (H : Π (a : A), K a → K a) : + center' (@quotient_group_functor_contr _ K K _ _ H) = ⟨gid (quotient_ab_group K), λ x, rfl⟩ := begin - note p := @quotient_group_functor_contr _ K K H, + note p := @quotient_group_functor_contr _ K K _ _ H, fapply eq_of_is_contr, end @@ -285,10 +297,10 @@ namespace group set_option pp.universes true - definition subgroup_rel_eq' {K L : subgroup_rel A} (htpy : Π (a : A), K a ≃ L a) : K = L := + definition subgroup_rel_eq' {K L : property A} [HK : is_subgroup A K] [HL : is_subgroup A L] (htpy : Π (a : A), K a ≃ L a) : K = L := begin - induction K with K', induction L with L', esimp at *, - assert q : K' = L', + induction HK with Rone Rmul Rinv, induction HL with Rone' Rmul' Rinv', esimp at *, + assert q : K = L, begin fapply eq_of_homotopy, intro a, @@ -296,17 +308,17 @@ namespace group exact htpy a, end, induction q, - assert q : Rone = Rone_1, + assert q : Rone = Rone', begin fapply is_prop.elim, end, induction q, - assert q2 : @Rmul = @Rmul_1, + assert q2 : @Rmul = @Rmul', begin fapply is_prop.elim, end, induction q2, - assert q : @Rinv = @Rinv_1, + assert q : @Rinv = @Rinv', begin fapply is_prop.elim, end, @@ -314,21 +326,21 @@ namespace group reflexivity end - definition subgroup_rel_eq {K L : subgroup_rel A} (K_in_L : Π (a : A), K a → L a) (L_in_K : Π (a : A), L a → K a) : K = L := + definition subgroup_rel_eq {K L : property A} [is_subgroup A K] [is_subgroup A L] (K_in_L : Π (a : A), a ∈ K → a ∈ L) (L_in_K : Π (a : A), a ∈ L → a ∈ K) : K = L := begin have htpy : Π (a : A), K a ≃ L a, begin intro a, - fapply equiv_of_is_prop, - fapply K_in_L a, - fapply L_in_K a, + apply @equiv_of_is_prop (a ∈ K) (a ∈ L) _ _ (K_in_L a) (L_in_K a), end, exact subgroup_rel_eq' htpy, end - definition eq_of_ab_qg_group' {K L : subgroup_rel A} (p : K = L) : quotient_ab_group K = quotient_ab_group L := + definition eq_of_ab_qg_group' {K L : property A} [HK : is_subgroup A K] [HL : is_subgroup A L] (p : K = L) : quotient_ab_group K = quotient_ab_group L := begin - induction p, reflexivity + revert HK, revert HL, induction p, intros, + have HK = HL, begin apply @is_prop.elim _ _ HK HL end, + rewrite this end definition iso_of_eq {B : AbGroup} (p : A = B) : A ≃g B := @@ -336,29 +348,35 @@ namespace group induction p, fapply isomorphism.mk, exact gid A, fapply adjointify, exact id, intro a, reflexivity, intro a, reflexivity end - definition iso_of_ab_qg_group' {K L : subgroup_rel A} (p : K = L) : quotient_ab_group K ≃g quotient_ab_group L := + definition iso_of_ab_qg_group' {K L : property A} [is_subgroup A K] [is_subgroup A L] (p : K = L) : quotient_ab_group K ≃g quotient_ab_group L := iso_of_eq (eq_of_ab_qg_group' p) - definition htpy_of_ab_qg_group' {K L : subgroup_rel A} (p : K = L) : (iso_of_ab_qg_group' p) ∘g ab_qg_map K ~ ab_qg_map L := +/- + definition htpy_of_ab_qg_group' {K L : property A} [HK : is_subgroup A K] [HL : is_subgroup A L] (p : K = L) : (iso_of_ab_qg_group' p) ∘g ab_qg_map K ~ ab_qg_map L := begin - induction p, reflexivity + revert HK, revert HL, induction p, intros HK HL, unfold iso_of_ab_qg_group', unfold ab_qg_map +-- have HK = HL, begin apply @is_prop.elim _ _ HK HL end, +-- rewrite this +-- induction p, reflexivity end +-/ - definition eq_of_ab_qg_group {K L : subgroup_rel A} (K_in_L : Π (a : A), K a → L a) (L_in_K : Π (a : A), L a → K a) : quotient_ab_group K = quotient_ab_group L := + definition eq_of_ab_qg_group {K L : property A} [is_subgroup A K] [is_subgroup A L] (K_in_L : Π (a : A), K a → L a) (L_in_K : Π (a : A), L a → K a) : quotient_ab_group K = quotient_ab_group L := eq_of_ab_qg_group' (subgroup_rel_eq K_in_L L_in_K) - definition iso_of_ab_qg_group {K L : subgroup_rel A} (K_in_L : Π (a : A), K a → L a) (L_in_K : Π (a : A), L a → K a) : quotient_ab_group K ≃g quotient_ab_group L := + definition iso_of_ab_qg_group {K L : property A} [is_subgroup A K] [is_subgroup A L] (K_in_L : Π (a : A), K a → L a) (L_in_K : Π (a : A), L a → K a) : quotient_ab_group K ≃g quotient_ab_group L := iso_of_eq (eq_of_ab_qg_group K_in_L L_in_K) - definition htpy_of_ab_qg_group {K L : subgroup_rel A} (K_in_L : Π (a : A), K a → L a) (L_in_K : Π (a : A), L a → K a) : iso_of_ab_qg_group K_in_L L_in_K ∘g ab_qg_map K ~ ab_qg_map L := +/- + definition htpy_of_ab_qg_group {K L : property A} [is_subgroup A K] [is_subgroup A L] (K_in_L : Π (a : A), K a → L a) (L_in_K : Π (a : A), L a → K a) : iso_of_ab_qg_group K_in_L L_in_K ∘g ab_qg_map K ~ ab_qg_map L := begin fapply htpy_of_ab_qg_group' end - +-/ end quotient_group_iso_ua section quotient_group_iso - variables {K L : subgroup_rel A} (H1 : Π (a : A), K a → L a) (H2 : Π (a : A), L a → K a) + variables {K L : property A} [is_subgroup A K] [is_subgroup A L] (H1 : Π (a : A), K a → L a) (H2 : Π (a : A), L a → K a) include H1 include H2 @@ -372,15 +390,15 @@ namespace group definition quotient_group_iso_contr_KK : is_contr (Σ (g : quotient_ab_group K →g quotient_ab_group K), g ∘g ab_qg_map K ~ ab_qg_map K) := - @quotient_group_functor_contr A K K (λ a, H2 a ∘ H1 a) + @quotient_group_functor_contr A K K _ _ (λ a, H2 a ∘ H1 a) definition quotient_group_iso_contr_LK : quotient_ab_group L →g quotient_ab_group K := - pr1 (center' (@quotient_group_functor_contr A L K H2)) + pr1 (center' (@quotient_group_functor_contr A L K _ _ H2)) definition quotient_group_iso_contr_LL : quotient_ab_group L →g quotient_ab_group L := - pr1 (center' (@quotient_group_functor_contr A L L (λ a, H1 a ∘ H2 a))) + pr1 (center' (@quotient_group_functor_contr A L L _ _ (λ a, H1 a ∘ H2 a))) /- definition quotient_group_iso : quotient_ab_group K ≃g quotient_ab_group L := @@ -402,15 +420,15 @@ namespace group intro a, induction a with g h, fapply is_contr_of_inhabited_prop, fapply adjointify, - rexact group_fun (pr1 (center' (@quotient_group_functor_contr A L K H2))), - note htpy := homotopy_of_eq (ap group_fun (ap sigma.pr1 (@quotient_group_functor_id _ L (λ a, (H1 a) ∘ (H2 a))))), + rexact group_fun (pr1 (center' (@quotient_group_functor_contr A L K _ _ H2))), + note htpy := homotopy_of_eq (ap group_fun (ap sigma.pr1 (@quotient_group_functor_id _ L _ (λ a, (H1 a) ∘ (H2 a))))), have KK : is_contr ((Σ(g' : quotient_ab_group K →g quotient_ab_group K), g' ∘g ab_qg_map K ~ ab_qg_map K) ), from quotient_group_functor_contr (λ a, (H2 a) ∘ (H1 a)), -- have KK_path : ⟨g, h⟩ = ⟨id, λ a, refl (ab_qg_map K a)⟩, from eq_of_is_contr ⟨g, h⟩ ⟨id, λ a, refl (ab_qg_map K a)⟩, repeat exact sorry end /- - definition quotient_group_iso_contr {K L : subgroup_rel A} (H1 : Π (a : A), K a → L a) (H2 : Π (a : A), L a → K a) : + definition quotient_group_iso_contr {K L : property A} [is_subgroup A K] [is_subgroup A L] (H1 : Π (a : A), K a → L a) (H2 : Π (a : A), L a → K a) : is_contr (Σ (g : quotient_ab_group K ≃g quotient_ab_group L), g ∘g ab_qg_map K ~ ab_qg_map L) := begin refine @is_trunc_equiv_closed (Σ(gh : Σ (g : quotient_ab_group K →g quotient_ab_group L), g ∘g ab_qg_map K ~ ab_qg_map L), is_equiv (group_fun (pr1 gh))) (Σ (g : quotient_ab_group K ≃g quotient_ab_group L), g ∘g ab_qg_map K ~ ab_qg_map L) -2 _ (quotient_group_iso_contr_aux H1 H2), @@ -422,8 +440,7 @@ namespace group end quotient_group_iso - - definition quotient_group_functor [constructor] (φ : G →g G') (h : Πg, N g → N' (φ g)) : + definition quotient_group_functor [constructor] (φ : G →g G') (h : Πg, g ∈ N → φ g ∈ N') : quotient_group N →g quotient_group N' := begin apply quotient_group_elim (qg_map N' ∘g φ), @@ -435,17 +452,18 @@ namespace group -- FIRST ISOMORPHISM THEOREM ------------------------------------------------ - -definition kernel_quotient_extension {A B : AbGroup} (f : A →g B) : quotient_ab_group (kernel_subgroup f) →g B := +definition kernel_quotient_extension {A B : AbGroup} (f : A →g B) : quotient_ab_group (kernel f) →g B := begin - fapply quotient_group_elim f, intro a, intro p, exact p + unfold quotient_ab_group, + fapply @quotient_group_elim A B _ (@is_normal_subgroup_ab _ (kernel f) _) f, + intro a, intro p, exact p end definition kernel_quotient_extension_triangle {A B : AbGroup} (f : A →g B) : - kernel_quotient_extension f ∘ ab_qg_map (kernel_subgroup f) ~ f := + kernel_quotient_extension f ∘ ab_qg_map (kernel f) ~ f := begin intro a, - apply quotient_group_compute + apply @quotient_group_compute _ _ _ (@is_normal_subgroup_ab _ (kernel f) _) end definition is_embedding_kernel_quotient_extension {A B : AbGroup} (f : A →g B) : @@ -453,27 +471,27 @@ definition is_embedding_kernel_quotient_extension {A B : AbGroup} (f : A →g B) begin fapply is_embedding_of_is_mul_hom, intro x, - note H := is_surjective_ab_qg_map (kernel_subgroup f) x, + note H := is_surjective_ab_qg_map (kernel f) x, induction H, induction p, intro q, - apply qg_map_eq_one, + apply @qg_map_eq_one _ _ (@is_normal_subgroup_ab _ (kernel f) _), refine _ ⬝ q, symmetry, rexact kernel_quotient_extension_triangle f a end -definition ab_group_quotient_homomorphism (A B : AbGroup)(K : subgroup_rel A)(L : subgroup_rel B) (f : A →g B) - (p : Π(a:A), K(a) → L(f a)) : quotient_ab_group K →g quotient_ab_group L := +definition ab_group_quotient_homomorphism (A B : AbGroup)(K : property A)(L : property B) [is_subgroup A K] [is_subgroup B L] (f : A →g B) + (p : Π(a:A), a ∈ K → f a ∈ L) : quotient_ab_group K →g quotient_ab_group L := begin - fapply quotient_group_elim, + fapply @quotient_group_elim, exact (ab_qg_map L) ∘g f, intro a, intro k, - exact @ab_qg_map_eq_one B L (f a) (p a k), + exact @ab_qg_map_eq_one B L _ (f a) (p a k), end definition ab_group_kernel_factor {A B C: AbGroup} (f : A →g B)(g : A →g C){i : C →g B}(H : f = i ∘g g ) - : Π a:A , kernel_subgroup(g)(a) → kernel_subgroup(f)(a) := + : kernel g ⊆ kernel f := begin intro a, intro p, @@ -484,41 +502,36 @@ definition ab_group_kernel_factor {A B C: AbGroup} (f : A →g B)(g : A →g C){ end definition ab_group_triv_kernel_factor {A B C: AbGroup} (f : A →g B)(g : A →g C){i : C →g B}(H : f = i ∘g g ) : - is_trivial_subgroup _ (kernel_subgroup(f)) → is_trivial_subgroup _ (kernel_subgroup(g)) := - begin - intro p, - intro a, - intro q, - fapply p, - exact ab_group_kernel_factor f g H a q - end + kernel f ⊆ '{1} → kernel g ⊆ '{1} := +λ p, subproperty.trans (ab_group_kernel_factor f g H) p -definition triv_kern_is_embedding {A B : AbGroup} (f : A →g B): -is_trivial_subgroup _ (kernel_subgroup(f)) → is_embedding(f) := - begin - intro p, - fapply is_embedding_of_is_mul_hom, - intro a q, - apply p, - exact q - end +definition is_embedding_of_kernel_subproperty_one {A B : AbGroup} (f : A →g B) : + kernel f ⊆ '{1} → is_embedding f := +λ p, is_embedding_of_is_mul_hom _ + (take x, assume h : f x = 1, + show x = 1, from eq_of_mem_singleton (p _ h)) + +definition kernel_subproperty_one {A B : AbGroup} (f : A →g B) : + is_embedding f → kernel f ⊆ '{1} := +λ h x hx, + have x = 1, from eq_one_of_is_mul_hom hx, + show x ∈ '{1}, from mem_singleton_of_eq this definition ab_group_kernel_equivalent {A B : AbGroup} (C : AbGroup) (f : A →g B)(g : A →g C)(i : C →g B)(H : f = i ∘g g )(K : is_embedding i) - : Π a:A , kernel_subgroup(g)(a) ↔ kernel_subgroup(f)(a) := -begin - intro a, - fapply iff.intro, - exact ab_group_kernel_factor f g H a, - intro p, - apply @is_injective_of_is_embedding _ _ i _ (g a) 1, - exact calc - i (g a) = f a : (homotopy_of_eq (ap group_fun H) a)⁻¹ - ... = 1 : p - ... = i 1 : (respect_one i)⁻¹ -end + : Π a:A, a ∈ kernel g ↔ a ∈ kernel f := +exteq_of_subproperty_of_subproperty + (show kernel g ⊆ kernel f, from ab_group_kernel_factor f g H) + (show kernel f ⊆ kernel g, from + take a, + suppose f a = 1, + have i (g a) = i 1, from calc + i (g a) = f a : (homotopy_of_eq (ap group_fun H) a)⁻¹ + ... = 1 : this + ... = i 1 : (respect_one i)⁻¹, + is_injective_of_is_embedding this) definition ab_group_kernel_image_lift (A B : AbGroup) (f : A →g B) - : Π a : A, kernel_subgroup(image_lift(f))(a) ↔ kernel_subgroup(f)(a) := + : Π a : A, a ∈ kernel (image_lift f) ↔ a ∈ kernel f := begin fapply ab_group_kernel_equivalent (ab_image f) (f) (image_lift(f)) (image_incl(f)), exact image_factor f, @@ -526,14 +539,14 @@ definition ab_group_kernel_image_lift (A B : AbGroup) (f : A →g B) end definition ab_group_kernel_quotient_to_image {A B : AbGroup} (f : A →g B) - : quotient_ab_group (kernel_subgroup f) →g ab_image (f) := + : quotient_ab_group (kernel f) →g ab_image (f) := begin - fapply quotient_group_elim (image_lift f), intro a, intro p, + fapply quotient_ab_group_elim (image_lift f), intro a, intro p, apply iff.mpr (ab_group_kernel_image_lift _ _ f a) p end definition ab_group_kernel_quotient_to_image_domain_triangle {A B : AbGroup} (f : A →g B) - : ab_group_kernel_quotient_to_image (f) ∘g ab_qg_map (kernel_subgroup (f)) ~ image_lift(f) := + : ab_group_kernel_quotient_to_image (f) ∘g ab_qg_map (kernel f) ~ image_lift(f) := begin intros a, esimp, @@ -551,10 +564,10 @@ definition ab_group_kernel_quotient_to_image_codomain_triangle {A B : AbGroup} ( definition is_surjective_kernel_quotient_to_image {A B : AbGroup} (f : A →g B) : is_surjective (ab_group_kernel_quotient_to_image f) := begin - fapply is_surjective_factor (group_fun (ab_qg_map (kernel_subgroup f))), -exact image_lift f, -apply quotient_group_compute, -exact is_surjective_image_lift f + fapply is_surjective_factor (group_fun (ab_qg_map (kernel f))), + exact image_lift f, + apply @quotient_group_compute _ _ _ (@is_normal_subgroup_ab _ (kernel f) _), + exact is_surjective_image_lift f end definition is_embedding_kernel_quotient_to_image {A B : AbGroup} (f : A →g B) @@ -566,7 +579,7 @@ definition is_embedding_kernel_quotient_to_image {A B : AbGroup} (f : A →g B) end definition ab_group_first_iso_thm {A B : AbGroup} (f : A →g B) - : quotient_ab_group (kernel_subgroup f) ≃g ab_image f := + : quotient_ab_group (kernel f) ≃g ab_image f := begin fapply isomorphism.mk, exact ab_group_kernel_quotient_to_image f, @@ -576,13 +589,13 @@ definition ab_group_first_iso_thm {A B : AbGroup} (f : A →g B) end definition codomain_surjection_is_quotient {A B : AbGroup} (f : A →g B)( H : is_surjective f) - : quotient_ab_group (kernel_subgroup f) ≃g B := + : quotient_ab_group (kernel f) ≃g B := begin exact (ab_group_first_iso_thm f) ⬝g (iso_surjection_ab_image_incl f H) end definition codomain_surjection_is_quotient_triangle {A B : AbGroup} (f : A →g B)( H : is_surjective f) - : codomain_surjection_is_quotient (f)(H) ∘g ab_qg_map (kernel_subgroup f) ~ f := + : codomain_surjection_is_quotient (f)(H) ∘g ab_qg_map (kernel f) ~ f := begin intro a, esimp @@ -610,18 +623,17 @@ definition codomain_surjection_is_quotient_triangle {A B : AbGroup} (f : A →g definition gr_mul (g h : A₁) : R g → R h → R (g * h) := trunc_functor2 rmul - definition normal_generating_relation : subgroup_rel A₁ := - ⦃ subgroup_rel, - R := R, - Rone := gr_one, - Rinv := gr_inv, - Rmul := gr_mul⦄ + definition normal_generating_relation [instance] : is_subgroup A₁ generating_relation := + ⦃ is_subgroup, + one_mem := gr_one, + inv_mem := gr_inv, + mul_mem := gr_mul⦄ parameter (A₁) - definition quotient_ab_group_gen : AbGroup := quotient_ab_group normal_generating_relation + definition quotient_ab_group_gen : AbGroup := quotient_ab_group generating_relation definition gqg_map [constructor] : A₁ →g quotient_ab_group_gen := - qg_map _ + ab_qg_map _ parameter {A₁} definition gqg_eq_of_rel {g h : A₁} (H : S (g * h⁻¹)) : gqg_map g = gqg_map h := @@ -634,7 +646,7 @@ definition codomain_surjection_is_quotient_triangle {A B : AbGroup} (f : A →g definition gqg_elim [constructor] (f : A₁ →g A₂) (H : Π⦃g⦄, S g → f g = 1) : quotient_ab_group_gen →g A₂ := begin - apply quotient_group_elim f, + apply quotient_ab_group_elim f, intro g r, induction r with r, induction r with g s g h r r' IH1 IH2 g r IH, { exact H s }, @@ -651,7 +663,7 @@ definition codomain_surjection_is_quotient_triangle {A B : AbGroup} (f : A →g definition gqg_elim_unique (f : A₁ →g A₂) (H : Π⦃g⦄, S g → f g = 1) (k : quotient_ab_group_gen →g A₂) : ( k ∘g gqg_map ~ f ) → k ~ gqg_elim f H := - !gelim_unique + !ab_gelim_unique end @@ -659,16 +671,18 @@ end group namespace group - variables {G H K : Group} {R : normal_subgroup_rel G} {S : normal_subgroup_rel H} - {T : normal_subgroup_rel K} + variables {G H K : Group} {R : property G} [is_normal_subgroup G R] + {S : property H} [is_normal_subgroup H S] + {T : property K} [is_normal_subgroup K T] - definition quotient_ab_group_functor [constructor] {G H : AbGroup} {R : subgroup_rel G} - {S : subgroup_rel H} (φ : G →g H) - (h : Πg, R g → S (φ g)) : quotient_ab_group R →g quotient_ab_group S := - quotient_group_functor φ h + definition quotient_ab_group_functor [constructor] {G H : AbGroup} + {R : property G} [is_subgroup G R] + {S : property H} [is_subgroup H S] (φ : G →g H) + (h : Πg, g ∈ R → φ g ∈ S) : quotient_ab_group R →g quotient_ab_group S := + @quotient_group_functor G H R (is_normal_subgroup_ab _) S (is_normal_subgroup_ab _) φ h theorem quotient_group_functor_compose (ψ : H →g K) (φ : G →g H) - (hψ : Πg, S g → T (ψ g)) (hφ : Πg, R g → S (φ g)) : + (hψ : Πg, g ∈ S → ψ g ∈ T) (hφ : Πg, g ∈ R → φ g ∈ S) : quotient_group_functor ψ hψ ∘g quotient_group_functor φ hφ ~ quotient_group_functor (ψ ∘g φ) (λg, proof hψ (φ g) qed ∘ hφ g) := begin @@ -681,18 +695,18 @@ namespace group intro g, induction g using set_quotient.rec_prop with g hg, reflexivity end - definition quotient_group_functor_mul.{u₁ v₁ u₂ v₂} - {G H : AbGroup} {R : subgroup_rel.{u₁ v₁} G} {S : subgroup_rel.{u₂ v₂} H} - (ψ φ : G →g H) (hψ : Πg, R g → S (ψ g)) (hφ : Πg, R g → S (φ g)) : + definition quotient_group_functor_mul + {G H : AbGroup} {R : property G} [is_subgroup G R] {S : property H} [is_subgroup H S] + (ψ φ : G →g H) (hψ : Πg, g ∈ R → ψ g ∈ S) (hφ : Πg, g ∈ R → φ g ∈ S) : homomorphism_mul (quotient_ab_group_functor ψ hψ) (quotient_ab_group_functor φ hφ) ~ quotient_ab_group_functor (homomorphism_mul ψ φ) - (λg hg, subgroup_respect_mul S (hψ g hg) (hφ g hg)) := + (λg hg, is_subgroup.mul_mem (hψ g hg) (hφ g hg)) := begin intro g, induction g using set_quotient.rec_prop with g hg, reflexivity end definition quotient_group_functor_homotopy {ψ φ : G →g H} (hψ : Πg, R g → S (ψ g)) - (hφ : Πg, R g → S (φ g)) (p : φ ~ ψ) : + (hφ : Πg, g ∈ R → φ g ∈ S) (p : φ ~ ψ) : quotient_group_functor φ hφ ~ quotient_group_functor ψ hψ := begin intro g, induction g using set_quotient.rec_prop with g hg, diff --git a/algebra/subgroup.hlean b/algebra/subgroup.hlean index 44e3c42..934dad9 100644 --- a/algebra/subgroup.hlean +++ b/algebra/subgroup.hlean @@ -22,6 +22,19 @@ namespace group (mul_mem : Π{g h}, g ∈ H → h ∈ H → g * h ∈ H) (inv_mem : Π{g}, g ∈ H → g⁻¹ ∈ H) + definition is_prop_is_subgroup [instance] (G : Group) (H : property G) : is_prop (is_subgroup G H) := + proof -- this results in a simpler choice of universe metavariables + have 1 ∈ H × (Π{g h}, g ∈ H → h ∈ H → g * h ∈ H) × (Π{g}, g ∈ H → g⁻¹ ∈ H) ≃ is_subgroup G H, + begin + fapply equiv.MK, + { intro p, cases p with p1 p2, cases p2 with p2 p3, exact is_subgroup.mk p1 @p2 @p3 }, + { intro p, split, exact is_subgroup.one_mem H, split, apply @is_subgroup.mul_mem G H p, apply @is_subgroup.inv_mem G H p}, + { intro b, cases b, reflexivity }, + { intro a, cases a with a1 a2, cases a2, reflexivity } + end, + is_trunc_equiv_closed _ this + qed + /-- Every group G has at least two subgroups, the trivial subgroup containing only one, and the full subgroup. --/ definition trivial_subgroup [instance] (G : Group) : is_subgroup G '{1} := begin @@ -103,7 +116,7 @@ namespace group /-- Next, we formalize some aspects of normal subgroups. Recall that a normal subgroup H of a group G is a subgroup which is invariant under all inner automorophisms on G. --/ - definition is_normal [constructor] (G : Group) (N : property G) : Prop := + definition is_normal.{u v} [constructor] (G : Group) (N : property.{u v} G) : Prop := trunctype.mk (Π{g} h, g ∈ N → h * g * h⁻¹ ∈ N) _ structure is_normal_subgroup [class] (G : Group) (N : property G) extends is_subgroup G N := @@ -122,7 +135,7 @@ section theorem is_normal_subgroup' (h : G) (r : g ∈ N) : h⁻¹ * g * h ∈ N := inv_inv h ▸ subgroup_is_normal N h⁻¹ r - definition is_normal_subgroup_ab.{u} [constructor] {C : property A} (subgrpA : is_subgroup A C) + definition is_normal_subgroup_ab [constructor] {C : property A} (subgrpA : is_subgroup A C) : is_normal_subgroup A C := ⦃ is_normal_subgroup, subgrpA, is_normal := abstract begin @@ -219,6 +232,8 @@ section definition Kernel {G H : Group} (f : G →g H) : Group := subgroup (kernel f) +set_option trace.class_instances true + definition ab_kernel {G H : AbGroup} (f : G →g H) : AbGroup := ab_subgroup (kernel f) definition incl_of_subgroup [constructor] {G : Group} (H : property G) [is_subgroup G H] : @@ -249,7 +264,7 @@ section fapply is_embedding_incl_of_subgroup, end - definition is_subgroup_of_subgroup {G : Group} {H1 H2 : property G} [is_subgroup G H1] + definition is_subgroup_of_is_subgroup {G : Group} {H1 H2 : property G} [is_subgroup G H1] [is_subgroup G H2] (hyp : Π (g : G), g ∈ H1 → g ∈ H2) : is_subgroup (subgroup H2) {h | incl_of_subgroup H2 h ∈ H1} := is_subgroup.mk diff --git a/property.hlean b/property.hlean index 0b58c5d..b6a313a 100644 --- a/property.hlean +++ b/property.hlean @@ -44,6 +44,10 @@ theorem eq_of_subproperty_of_subproperty {a b : property X} (h₁ : a ⊆ b) (h subproperty.antisymm h₁ h₂ -/ +theorem exteq_of_subproperty_of_subproperty {a b : property X} (h₁ : a ⊆ b) (h₂ : b ⊆ a) : + ∀ ⦃x⦄, x ∈ a ↔ x ∈ b := +λ x, iff.intro (λ h, h₁ h) (λ h, h₂ h) + theorem mem_of_subproperty_of_mem {s₁ s₂ : property X} {a : X} : s₁ ⊆ s₂ → a ∈ s₁ → a ∈ s₂ := assume h₁ h₂, h₁ _ h₂