diff --git a/theories/Algebra/AbGroups/AbPushout.v b/theories/Algebra/AbGroups/AbPushout.v index 6654c549cc..f4e518fcf3 100644 --- a/theories/Algebra/AbGroups/AbPushout.v +++ b/theories/Algebra/AbGroups/AbPushout.v @@ -1,6 +1,6 @@ Require Import Basics Types Truncations.Core. Require Import WildCat.Core HSet. -Require Export Algebra.Groups.Image Algebra.Groups.QuotientGroup. +Require Export Algebra.Groups.QuotientGroup. Require Import AbGroups.AbelianGroup AbGroups.Biproduct. Local Open Scope mc_scope. diff --git a/theories/Algebra/Groups.v b/theories/Algebra/Groups.v index 89d347bd34..26efb965fc 100644 --- a/theories/Algebra/Groups.v +++ b/theories/Algebra/Groups.v @@ -2,8 +2,6 @@ Require Export HoTT.Algebra.Groups.Group. Require Export HoTT.Algebra.Groups.Subgroup. -Require Export HoTT.Algebra.Groups.Image. -Require Export HoTT.Algebra.Groups.Kernel. Require Export HoTT.Algebra.Groups.QuotientGroup. Require Export HoTT.Algebra.Groups.GrpPullback. diff --git a/theories/Algebra/Groups/Image.v b/theories/Algebra/Groups/Image.v deleted file mode 100644 index e5409faed0..0000000000 --- a/theories/Algebra/Groups/Image.v +++ /dev/null @@ -1,73 +0,0 @@ -Require Import Basics Types. -Require Import Truncations.Core. -Require Import Algebra.Groups.Group. -Require Import Algebra.Groups.Subgroup. -Require Import WildCat.Core. -Require Import HSet. - -(** Image of group homomorphisms *) - -Local Open Scope mc_scope. -Local Open Scope mc_mult_scope. - -(** The image of a group homomorphism between groups is a subgroup *) -Definition grp_image {A B : Group} (f : A $-> B) : Subgroup B. -Proof. - snrapply (Build_Subgroup' (fun b => hexists (fun a => f a = b))). - - exact _. - - apply tr. - exists mon_unit. - apply grp_homo_unit. - - intros x y p q; strip_truncations; apply tr. - destruct p as [a p], q as [b q]. - exists (a * b^). - lhs nrapply grp_homo_op; f_ap. - lhs nrapply grp_homo_inv; f_ap. -Defined. - -Definition grp_image_in {A B : Group} (f : A $-> B) : A $-> grp_image f. -Proof. - snrapply Build_GroupHomomorphism. - { intro x. - exists (f x). - srapply tr. - exists x. - reflexivity. } - cbn. grp_auto. -Defined. - -(** When the homomorphism is an embedding, we don't need to truncate. *) -Definition grp_image_embedding {A B : Group} (f : A $-> B) `{IsEmbedding f} : Subgroup B. -Proof. - snrapply (Build_Subgroup _ (hfiber f)). - repeat split. - - exact _. - - exact (mon_unit; grp_homo_unit f). - - intros x y [a []] [b []]. - exists (a * b). - apply grp_homo_op. - - intros b [a []]. - exists a^. - apply grp_homo_inv. -Defined. - -Definition grp_image_in_embedding {A B : Group} (f : A $-> B) `{IsEmbedding f} - : GroupIsomorphism A (grp_image_embedding f). -Proof. - snrapply Build_GroupIsomorphism. - - snrapply Build_GroupHomomorphism. - + intro x. - exists (f x). - exists x. - reflexivity. - + cbn; grp_auto. - - apply isequiv_surj_emb. - 2: apply (cancelL_isembedding (g:=pr1)). - intros [b [a p]]; cbn. - rapply contr_inhabited_hprop. - refine (tr (a; _)). - srapply path_sigma'. - 1: exact p. - refine (transport_sigma' _ _ @ _). - by apply path_sigma_hprop. -Defined. diff --git a/theories/Algebra/Groups/Kernel.v b/theories/Algebra/Groups/Kernel.v deleted file mode 100644 index 34f5977771..0000000000 --- a/theories/Algebra/Groups/Kernel.v +++ /dev/null @@ -1,94 +0,0 @@ -Require Import Basics Types. -Require Import Algebra.Groups.Group. -Require Import Algebra.Groups.Subgroup. -Require Import WildCat.Core. -Require Import Universes.HSet. - -(** * Kernels of group homomorphisms *) - -Local Open Scope mc_scope. -Local Open Scope mc_mult_scope. - -Definition grp_kernel {A B : Group} (f : GroupHomomorphism A B) : NormalSubgroup A. -Proof. - snrapply Build_NormalSubgroup. - - srapply (Build_Subgroup' (fun x => f x = 1)); cbn beta. - 1: apply grp_homo_unit. - intros x y p q. - apply (grp_homo_moveL_1M _ _ _)^-1. - exact (p @ q^). - - intros x y; cbn; intros p. - apply (grp_homo_moveL_1V _ _ _)^-1. - lhs_V nrapply grp_inv_inv. - nrapply (ap (-) _^). - by apply grp_homo_moveL_1V. -Defined. - -(** ** Corecursion principle for group kernels *) - -Proposition grp_kernel_corec {A B G : Group} {f : A $-> B} (g : G $-> A) - (h : f $o g == grp_homo_const) : G $-> grp_kernel f. -Proof. - snrapply Build_GroupHomomorphism. - - exact (fun x:G => (g x; h x)). - - intros x x'. - apply path_sigma_hprop; cbn. - apply grp_homo_op. -Defined. - -Theorem equiv_grp_kernel_corec `{Funext} {A B G : Group} {f : A $-> B} - : (G $-> grp_kernel f) <~> (exists g : G $-> A, f $o g == grp_homo_const). -Proof. - srapply equiv_adjointify. - - intro k. - srefine (_ $o k; _). - 1: apply subgroup_incl. - intro x; cbn. - exact (k x).2. - - intros [g p]. - exact (grp_kernel_corec _ p). - - intros [g p]. - apply path_sigma_hprop; unfold pr1. - apply equiv_path_grouphomomorphism; intro; reflexivity. - - intro k. - apply equiv_path_grouphomomorphism; intro x. - apply path_sigma_hprop; reflexivity. -Defined. - -(** The underlying map of a group homomorphism with a trivial kernel is an embedding. *) -Global Instance isembedding_istrivial_kernel {G H : Group} (f : G $-> H) - (triv : IsTrivialGroup (grp_kernel f)) - : IsEmbedding f. -Proof. - intros h. - apply hprop_allpath. - intros [x p] [y q]. - srapply path_sigma_hprop; unfold pr1. - apply grp_moveL_1M. - apply triv; simpl. - rhs_V nrapply (grp_inv_r h). - lhs nrapply grp_homo_op. - nrapply (ap011 (.*.) p). - lhs nrapply grp_homo_inv. - exact (ap (^) q). -Defined. - -(** If the underlying map of a group homomorphism is an embedding then the kernel is trivial. *) -Definition istrivial_kernel_isembedding {G H : Group} (f : G $-> H) - (emb : IsEmbedding f) - : IsTrivialGroup (grp_kernel f). -Proof. - intros g p. - rapply (isinj_embedding f). - exact (p @ (grp_homo_unit f)^). -Defined. -Global Hint Immediate istrivial_kernel_isembedding : typeclass_instances. - -(** Characterisation of group embeddings *) -Proposition equiv_istrivial_kernel_isembedding `{F : Funext} - {G H : Group} (f : G $-> H) - : IsTrivialGroup (grp_kernel f) <~> IsEmbedding f. -Proof. - apply equiv_iff_hprop_uncurried. - split; exact _. -Defined. diff --git a/theories/Algebra/Groups/QuotientGroup.v b/theories/Algebra/Groups/QuotientGroup.v index c19b207626..3ebf57fe1b 100644 --- a/theories/Algebra/Groups/QuotientGroup.v +++ b/theories/Algebra/Groups/QuotientGroup.v @@ -3,8 +3,6 @@ Require Import Truncations.Core. Require Import Algebra.Congruence. Require Import Algebra.Groups.Group. Require Import Algebra.Groups.Subgroup. -Require Export Algebra.Groups.Image. -Require Export Algebra.Groups.Kernel. Require Export Colimits.Quotient. Require Import HSet. Require Import Spaces.Finite.Finite. @@ -292,7 +290,7 @@ Section FirstIso. : A / grp_kernel phi $-> grp_image phi. Proof. srapply grp_quotient_rec. - + srapply grp_image_in. + + srapply grp_homo_image_in. + intros n x. by apply path_sigma_hprop. Defined. diff --git a/theories/Algebra/Groups/ShortExactSequence.v b/theories/Algebra/Groups/ShortExactSequence.v index 29973f191c..f86b8677b5 100644 --- a/theories/Algebra/Groups/ShortExactSequence.v +++ b/theories/Algebra/Groups/ShortExactSequence.v @@ -1,7 +1,7 @@ Require Import Basics Types. Require Import Truncations.Core. Require Import WildCat.Core Pointed. -Require Import Groups.Group Groups.Subgroup Groups.Kernel. +Require Import Groups.Group Groups.Subgroup. Require Import Homotopy.ExactSequence Modalities.Identity. (** * Complexes of groups *) diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v index 78a49bc07a..f65f1c4555 100644 --- a/theories/Algebra/Groups/Subgroup.v +++ b/theories/Algebra/Groups/Subgroup.v @@ -1,6 +1,7 @@ Require Import Basics Types HFiber WildCat.Core WildCat.Equiv. -Require Import Truncations.Core. -Require Import Algebra.Groups.Group TruncType. +Require Import Truncations.Core Modalities.Modality. +Require Export Modalities.Modality (conn_map_factor1_image). +Require Import Algebra.Groups.Group Universes.TruncType Universes.HSet. Local Open Scope mc_scope. Local Open Scope mc_mult_scope. @@ -9,6 +10,8 @@ Generalizable Variables G H A B C N f g. (** * Subgroups *) +(** ** Definition of being a subgroup *) + (** A subgroup H of a group G is a predicate (i.e. an hProp-valued type family) on G which is closed under the group operations. The group underlying H is given by the total space { g : G & H g }, defined in [subgroup_group] below. *) Class IsSubgroup {G : Group} (H : G -> Type) := { issubgroup_predicate : forall x, IsHProp (H x) ; @@ -19,6 +22,8 @@ Class IsSubgroup {G : Group} (H : G -> Type) := { Global Existing Instance issubgroup_predicate. +(** Basic properties of subgroups *) + (** Smart constructor for subgroups. *) Definition Build_IsSubgroup' {G : Group} (H : G -> Type) `{forall x, IsHProp (H x)} @@ -101,6 +106,8 @@ Proof. exact (istrunc_equiv_istrunc _ (issig_issubgroup H)). Defined. +(** ** Definition of subgroup *) + (** The type (set) of subgroups of a group G. *) Record Subgroup (G : Group) := { subgroup_pred : G -> Type ; @@ -110,6 +117,11 @@ Record Subgroup (G : Group) := { Coercion subgroup_pred : Subgroup >-> Funclass. Global Existing Instance subgroup_issubgroup. +Definition issig_subgroup {G : Group} : _ <~> Subgroup G + := ltac:(issig). + +(** ** Basics properties of subgroups *) + Definition Build_Subgroup' {G : Group} (H : G -> Type) `{forall x, IsHProp (H x)} (unit : H mon_unit) @@ -149,6 +161,38 @@ Proof. by rewrite grp_inv_op, grp_inv_inv. Defined. +(** Paths between subgroups correspond to homotopies between the underlying predicates. *) +Proposition equiv_path_subgroup `{F : Funext} {G : Group} (H K : Subgroup G) + : (H == K) <~> (H = K). +Proof. + refine ((equiv_ap' issig_subgroup^-1%equiv _ _)^-1%equiv oE _); cbn. + refine (equiv_path_sigma_hprop _ _ oE _); cbn. + apply equiv_path_arrow. +Defined. + +Proposition equiv_path_subgroup' `{U : Univalence} {G : Group} (H K : Subgroup G) + : (forall g:G, H g <-> K g) <~> (H = K). +Proof. + refine (equiv_path_subgroup _ _ oE _). + apply equiv_functor_forall_id; intro g. + exact equiv_path_iff_ishprop. +Defined. + +Global Instance ishset_subgroup `{Univalence} {G : Group} : IsHSet (Subgroup G). +Proof. + nrefine (istrunc_equiv_istrunc _ issig_subgroup). + nrefine (istrunc_equiv_istrunc _ (equiv_functor_sigma_id _)). + - intro P; apply issig_issubgroup. + - nrefine (istrunc_equiv_istrunc _ (equiv_sigma_assoc' _ _)^-1%equiv). + nrapply istrunc_sigma. + 2: intros []; apply istrunc_hprop. + nrefine (istrunc_equiv_istrunc + _ (equiv_sig_coind (fun g:G => Type) (fun g x => IsHProp x))^-1%equiv). + apply istrunc_forall. +Defined. + +(** ** Underlying group of a subgroup *) + (** The group given by a subgroup *) Definition subgroup_group {G : Group} (H : Subgroup G) : Group. Proof. @@ -169,6 +213,7 @@ Defined. Coercion subgroup_group : Subgroup >-> Group. +(** The underlying group of a subgroup of [G] has an inclusion map into [G]. *) Definition subgroup_incl {G : Group} (H : Subgroup G) : subgroup_group H $-> G. Proof. @@ -177,24 +222,52 @@ Proof. hnf; reflexivity. Defined. +(** The inclusion map is an embedding. *) Global Instance isembedding_subgroup_incl {G : Group} (H : Subgroup G) : IsEmbedding (subgroup_incl H) := fun _ => istrunc_equiv_istrunc _ (hfiber_fibration _ _). -Definition issig_subgroup {G : Group} : _ <~> Subgroup G - := ltac:(issig). +(** Restriction of a group homomorphism to a subgroup. *) +Definition grp_homo_restr {G H : Group} (f : G $-> H) (K : Subgroup G) + : subgroup_group K $-> H + := f $o subgroup_incl _. -Definition functor_subgroup_group {G H : Group} {J : Subgroup G} {K : Subgroup H} - (f : G $-> H) (g : forall x, J x -> K (f x)) - : subgroup_group J $-> subgroup_group K. +(** Corestriction of a group homomorphism to a subgroup. *) +Definition subgroup_corec {G H : Group} {K : Subgroup H} + (f : G $-> H) (g : forall x, K (f x)) + : G $-> subgroup_group K. Proof. snrapply Build_GroupHomomorphism. - - exact (functor_sigma f g). + - exact (fun x => (f x; g x)). - intros x y. rapply path_sigma_hprop. snrapply grp_homo_op. Defined. +(** Corestriction is an equivalence on group homomorphisms. *) +Definition equiv_subgroup_corec {F : Funext} + (G : Group) {H : Group} (K : Subgroup H) + : {f : G $-> H & forall x, K (f x)} <~> (G $-> subgroup_group K). +Proof. + snrapply equiv_adjointify. + - exact (sig_rec subgroup_corec). + - intros g. + exists (subgroup_incl _ $o g). + intros x. + exact (g x).2. + - intros g. + by snrapply equiv_path_grouphomomorphism. + - intros [f p]. + rapply path_sigma_hprop. + by snrapply equiv_path_grouphomomorphism. +Defined. + +(** Functoriality on subgroups. *) +Definition functor_subgroup_group {G H : Group} {J : Subgroup G} {K : Subgroup H} + (f : G $-> H) (g : forall x, J x -> K (f x)) + : subgroup_group J $-> subgroup_group K + := subgroup_corec (grp_homo_restr f J) (sig_ind _ g). + Definition grp_iso_subgroup_group {G H : Group@{i}} {J : Subgroup@{i i} G} (K : Subgroup@{i i} H) (e : G $<~> H) (f : forall x, J x <-> K (e x)) @@ -215,51 +288,7 @@ Proof. nrapply eissect. Defined. -(** The preimage of a subgroup under a group homomorphism is a subgroup. *) -Definition subgroup_preimage {G H : Group} (f : G $-> H) (S : Subgroup H) - : Subgroup G. -Proof. - snrapply Build_Subgroup'. - - exact (S o f). - - hnf; exact _. - - nrefine (transport S (grp_homo_unit f)^ _). - apply subgroup_in_unit. - - hnf; intros x y Sfx Sfy. - nrefine (transport S (grp_homo_op f _ _)^ _). - nrapply subgroup_in_op; only 1: assumption. - nrefine (transport S (grp_homo_inv f _)^ _). - by apply subgroup_in_inv. -Defined. - -(** Paths between subgroups correspond to homotopies between the underlying predicates. *) -Proposition equiv_path_subgroup `{F : Funext} {G : Group} (H K : Subgroup G) - : (H == K) <~> (H = K). -Proof. - refine ((equiv_ap' issig_subgroup^-1%equiv _ _)^-1%equiv oE _); cbn. - refine (equiv_path_sigma_hprop _ _ oE _); cbn. - apply equiv_path_arrow. -Defined. - -Proposition equiv_path_subgroup' `{U : Univalence} {G : Group} (H K : Subgroup G) - : (forall g:G, H g <-> K g) <~> (H = K). -Proof. - refine (equiv_path_subgroup _ _ oE _). - apply equiv_functor_forall_id; intro g. - exact equiv_path_iff_ishprop. -Defined. - -Global Instance ishset_subgroup `{Univalence} {G : Group} : IsHSet (Subgroup G). -Proof. - nrefine (istrunc_equiv_istrunc _ issig_subgroup). - nrefine (istrunc_equiv_istrunc _ (equiv_functor_sigma_id _)). - - intro P; apply issig_issubgroup. - - nrefine (istrunc_equiv_istrunc _ (equiv_sigma_assoc' _ _)^-1%equiv). - nrapply istrunc_sigma. - 2: intros []; apply istrunc_hprop. - nrefine (istrunc_equiv_istrunc - _ (equiv_sig_coind (fun g:G => Type) (fun g x => IsHProp x))^-1%equiv). - apply istrunc_forall. -Defined. +(** ** Cosets of subgroups *) Section Cosets. @@ -335,7 +364,7 @@ Section Cosets. End Cosets. -(** Identities related to the left and right cosets. *) +(** ** Properties of left and right cosets *) Definition in_cosetL_unit {G : Group} {N : Subgroup G} : forall x y, in_cosetL N (x^ * y) mon_unit <~> in_cosetL N x y. @@ -392,6 +421,8 @@ Proof. apply equiv_subgroup_op_inv. Defined. +(** ** Normal subgroups *) + (** A normal subgroup is a subgroup closed under conjugation. *) Class IsNormalSubgroup {G : Group} (N : Subgroup G) := isnormal : forall {x y}, N (x * y) -> N (y * x). @@ -507,7 +538,7 @@ Proof. exact p. Defined. -(** *** Trivial subgroup *) +(** ** Trivial subgroup *) (** The trivial subgroup of a group [G]. *) Definition trivial_subgroup G : Subgroup G. @@ -581,7 +612,7 @@ Proof. 1,2: apply istrivial_iff_grp_iso_trivial; exact _. Defined. -(** *** Maximal Subgroups *) +(** ** Maximal Subgroups *) (** Every group is a (maximal) subgroup of itself. *) Definition maximal_subgroup G : Subgroup G. @@ -623,7 +654,36 @@ Global Instance ismaximalsubgroup_maximalsubgroup {G : Group} : IsMaximalSubgroup (maximal_subgroup G) := fun g => tt. -(** *** Subgroup intersection *) +(** ** Preimage subgroup *) + +(** The preimage of a subgroup under a group homomorphism is a subgroup. *) +Definition subgroup_preimage {G H : Group} (f : G $-> H) (S : Subgroup H) + : Subgroup G. +Proof. + snrapply Build_Subgroup'. + - exact (S o f). + - hnf; exact _. + - nrefine (transport S (grp_homo_unit f)^ _). + apply subgroup_in_unit. + - hnf; intros x y Sfx Sfy. + nrefine (transport S (grp_homo_op f _ _)^ _). + nrapply subgroup_in_op; only 1: assumption. + nrefine (transport S (grp_homo_inv f _)^ _). + by apply subgroup_in_inv. +Defined. + +(** The preimage of a normal subgroup is again normal. *) +Global Instance isnormal_subgroup_preimage {G H : Group} (f : G $-> H) + (N : Subgroup H) `{!IsNormalSubgroup N} + : IsNormalSubgroup (subgroup_preimage f N). +Proof. + intros x y Nfxy; simpl. + nrefine (transport N (grp_homo_op _ _ _)^ _). + apply isnormal. + exact (transport N (grp_homo_op _ _ _) Nfxy). +Defined. + +(** ** Subgroup intersection *) (** Intersection of two subgroups *) Definition subgroup_intersection {G : Group} (H K : Subgroup G) : Subgroup G. @@ -636,13 +696,13 @@ Proof. split; by apply subgroup_in_op_inv. Defined. -(** *** Simple groups *) +(** ** Simple groups *) Class IsSimpleGroup (G : Group) := is_simple_group : forall (N : Subgroup G) `{IsNormalSubgroup G N}, IsTrivialGroup N + IsMaximalSubgroup N. -(** *** The subgroup generated by a subset *) +(** ** The subgroup generated by a subset *) (** Underlying type family of a subgroup generated by subset *) Inductive subgroup_generated_type {G : Group} (X : G -> Type) : G -> Type := @@ -777,9 +837,9 @@ Definition normalsubgroup_product {G : Group} (H K : NormalSubgroup G) : NormalSubgroup G := Build_NormalSubgroup G (subgroup_product H K) _. -(* **** Paths between generated subgroups *) +(** *** Paths between generated subgroups *) -(* This gets used twice in [path_subgroup_generated], so we factor it out here. *) +(** This gets used twice in [path_subgroup_generated], so we factor it out here. *) Local Lemma path_subgroup_generated_helper {G : Group} (X Y : G -> Type) (K : forall g, merely (X g) -> merely (Y g)) : forall g, Trunc (-1) (subgroup_generated_type X g) @@ -793,7 +853,7 @@ Proof. by apply tr, sgt_op. Defined. -(* If the predicates selecting the generators are merely equivalent, then the generated subgroups are equal. (One could probably prove that the generated subgroup are isomorphic without using univalence.) *) +(** If the predicates selecting the generators are merely equivalent, then the generated subgroups are equal. (One could probably prove that the generated subgroup are isomorphic without using univalence.) *) Definition path_subgroup_generated `{Univalence} {G : Group} (X Y : G -> Type) (K : forall g, Trunc (-1) (X g) <-> Trunc (-1) (Y g)) : subgroup_generated X = subgroup_generated Y. @@ -804,7 +864,197 @@ Proof. - apply path_subgroup_generated_helper, (fun x => snd (K x)). Defined. -(* Equal subgroups have isomorphic underlying groups. *) +(** Equal subgroups have isomorphic underlying groups. *) Definition equiv_subgroup_group {G : Group} (H1 H2 : Subgroup G) : H1 = H2 -> GroupIsomorphism H1 H2 := ltac:(intros []; exact grp_iso_id). + +(** ** Image of a group homomorphism *) + +(** The image of a group homomorphism between groups is a subgroup. *) +Definition grp_image {G H : Group} (f : G $-> H) : Subgroup H. +Proof. + srapply (Build_Subgroup' (fun y => hexists (fun x => f x = y))); cbn beta. + - apply tr. + exists 1. + apply grp_homo_unit. + - intros x y p q; strip_truncations; apply tr. + destruct p as [a p], q as [b q]. + exists (a * b^). + lhs nrapply grp_homo_op; f_ap. + lhs nrapply grp_homo_inv; f_ap. +Defined. + +Definition grp_image_in {G H : Group} (f : G $-> H) + : forall x, grp_image f (f x) + := fun x => tr (x; idpath). + +Definition grp_homo_image_in {G H : Group} (f : G $-> H) + : G $-> grp_image f + := subgroup_corec f (grp_image_in f). + +(** ** Image of a group embedding *) + +(** When the homomorphism is an embedding, we don't need to truncate. *) +Definition grp_image_embedding {G H : Group} (f : G $-> H) `{IsEmbedding f} + : Subgroup H. +Proof. + snrapply (Build_Subgroup _ (hfiber f)). + repeat split. + - exact _. + - exact (mon_unit; grp_homo_unit f). + - intros x y [a []] [b []]. + exists (a * b). + apply grp_homo_op. + - intros b [a []]. + exists a^. + apply grp_homo_inv. +Defined. + +Definition grp_image_in_embedding {G H : Group} (f : G $-> H) `{IsEmbedding f} + : GroupIsomorphism G (grp_image_embedding f). +Proof. + snrapply Build_GroupIsomorphism. + - snrapply (subgroup_corec f). + exact (fun x => (x; idpath)). + - apply isequiv_surj_emb. + 2: apply (cancelL_isembedding (g:=pr1)). + intros [b [a p]]; cbn. + rapply contr_inhabited_hprop. + refine (tr (a; _)). + srapply path_sigma'. + 1: exact p. + refine (transport_sigma' _ _ @ _). + by apply path_sigma_hprop. +Defined. + +(** The image of a surjective group homomorphism is the maximal subgroup. *) +Global Instance ismaximal_image_issurj {G H : Group} + (f : G $-> H) `{IsSurjection f} + : IsMaximalSubgroup (grp_image f). +Proof. + rapply conn_map_elim. + apply grp_image_in. +Defined. + +(** ** Image of a subgroup under a group homomoprhism *) + +(** The image of a subgroup under group homomorphism. *) +Definition subgroup_image {G H : Group} (f : G $-> H) + : Subgroup G -> Subgroup H + := fun K => grp_image (grp_homo_restr f K). + +(** By definition, values of [f x] where [x] is in a subgroup [J] are in the image of [J] under [f]. *) +Definition subgroup_image_in {G H : Group} (f : G $-> H) (J : Subgroup G) + : forall x, J x -> subgroup_image f J (f x) + := fun x Jx => tr ((x; Jx); idpath). + +(** Converting the subgroups to groups, we get the expected surjective (epi) restriction homomorphism. *) +Definition grp_homo_subgroup_image_in {G H : Group} + (f : G $-> H) (J : Subgroup G) + : subgroup_group J $-> subgroup_group (subgroup_image f J) + := functor_subgroup_group f (subgroup_image_in _ _). + +(** The restriction map from the subgroup to the image is surjective as expected, by [conn_map_factor1_image]. *) +Definition issurj_grp_homo_subgroup_image_in {G H : Group} + (f : G $-> H) (J : Subgroup G) + : IsSurjection (grp_homo_subgroup_image_in f J) + := _. + +(** An image of a subgroup [J] is included in a subgroup [K] if (and only if) [J] is included in the preimage of the subgroup [K]. *) +Definition subgroup_image_rec {G H : Group} + (f : G $-> H) {J : Subgroup G} {K : Subgroup H} + (g : forall x, J x -> K (f x)) + : forall x, subgroup_image f J x -> K x. +Proof. + intros x; apply Trunc_rec; intros [[j Jj] p]. + destruct p. + exact (g j Jj). +Defined. + +(** The image functor is adjoint to the preimage functor. *) +Definition iff_subgroup_image_rec {G H : Group} + (f : G $-> H) {J : Subgroup G} {K : Subgroup H} + : (forall x, subgroup_image f J x -> K x) + <-> (forall x, J x -> subgroup_preimage f K x). +Proof. + split. + - intros rec x Jx. + apply rec, tr. + by exists (x; Jx). + - snrapply subgroup_image_rec. +Defined. + +(** [subgroup_image] preserves normal subgroups when the group homomorphism is surjective. *) +Global Instance isnormal_subgroup_image {G H : Group} (f : G $-> H) + (J : Subgroup G) `{!IsNormalSubgroup J} `{!IsSurjection f} + : IsNormalSubgroup (subgroup_image f J). +Proof. + snrapply Build_IsNormalSubgroup'. + intros x y; revert x. + change (subgroup_image f J (y * ?x * y^)) + with (subgroup_preimage (grp_conj y) (subgroup_image f J) x). + snrapply subgroup_image_rec. + intros x Jx. + change (subgroup_image f J ((grp_conj y $o f) x)). + revert y; rapply (conn_map_elim (Tr (-1)) f); intros y. + rewrite <- grp_homo_conj. + nrapply subgroup_image_in. + by rapply isnormal_conj. +Defined. + +(** ** Kernels of group homomorphisms *) + +Definition grp_kernel {G H : Group} (f : G $-> H) + : NormalSubgroup G + := Build_NormalSubgroup G (subgroup_preimage f (trivial_subgroup _)) _. + +(** Corecursion principle for group kernels *) +Definition grp_kernel_corec {A B G : Group} {f : A $-> B} + (g : G $-> A) (h : f $o g == grp_homo_const) + : G $-> grp_kernel f. +Proof. + snrapply (subgroup_corec g); exact h. +Defined. + +Definition equiv_grp_kernel_corec `{Funext} {A B G : Group} {f : A $-> B} + : {g : G $-> A & f $o g == grp_homo_const} <~> (G $-> grp_kernel f) + := equiv_subgroup_corec G (grp_kernel f). + +(** The underlying map of a group homomorphism with a trivial kernel is an embedding. *) +Global Instance isembedding_istrivial_kernel {G H : Group} (f : G $-> H) + (triv : IsTrivialGroup (grp_kernel f)) + : IsEmbedding f. +Proof. + intros h. + apply hprop_allpath. + intros [x p] [y q]. + srapply path_sigma_hprop; unfold pr1. + apply grp_moveL_1M. + apply triv; simpl. + rhs_V nrapply (grp_inv_r h). + lhs nrapply grp_homo_op. + nrapply (ap011 (.*.) p). + lhs nrapply grp_homo_inv. + exact (ap (^) q). +Defined. + +(** If the underlying map of a group homomorphism is an embedding then the kernel is trivial. *) +Definition istrivial_kernel_isembedding {G H : Group} (f : G $-> H) + (emb : IsEmbedding f) + : IsTrivialGroup (grp_kernel f). +Proof. + intros g p. + rapply (isinj_embedding f). + exact (p @ (grp_homo_unit f)^). +Defined. +Global Hint Immediate istrivial_kernel_isembedding : typeclass_instances. + +(** Characterisation of group embeddings *) +Proposition equiv_istrivial_kernel_isembedding `{F : Funext} + {G H : Group} (f : G $-> H) + : IsTrivialGroup (grp_kernel f) <~> IsEmbedding f. +Proof. + apply equiv_iff_hprop_uncurried. + split; exact _. +Defined. diff --git a/theories/Algebra/Rings/Ideal.v b/theories/Algebra/Rings/Ideal.v index 3e19ae9f05..cb1ffb5307 100644 --- a/theories/Algebra/Rings/Ideal.v +++ b/theories/Algebra/Rings/Ideal.v @@ -2,7 +2,7 @@ Require Import Basics Types. Require Import Spaces.Finite.Fin. Require Import Classes.interfaces.canonical_names. Require Import Algebra.Rings.Ring. -Require Import Algebra.Groups.Subgroup Algebra.Groups.Kernel. +Require Import Algebra.Groups.Subgroup. Require Import Algebra.AbGroups.AbelianGroup. Require Import WildCat.Core. diff --git a/theories/Algebra/Rings/Module.v b/theories/Algebra/Rings/Module.v index a477adff3e..13a6c88849 100644 --- a/theories/Algebra/Rings/Module.v +++ b/theories/Algebra/Rings/Module.v @@ -2,7 +2,7 @@ Require Import WildCat. Require Import Spaces.Nat.Core. (* Some of the material in abstract_algebra and canonical names could be selectively exported to the user, as is done in Groups/Group.v. *) Require Import Classes.interfaces.canonical_names. -Require Import Algebra.Groups.Kernel Algebra.Groups.Image Algebra.Groups.QuotientGroup. +Require Import Algebra.Groups.QuotientGroup. Require Import Algebra.AbGroups.AbelianGroup Algebra.AbGroups.Biproduct. Require Import Rings.Ring. diff --git a/theories/Algebra/Rings/Ring.v b/theories/Algebra/Rings/Ring.v index 9384c9394d..d1746a20d0 100644 --- a/theories/Algebra/Rings/Ring.v +++ b/theories/Algebra/Rings/Ring.v @@ -2,7 +2,7 @@ Require Import WildCat. Require Import Spaces.Nat.Core Spaces.Nat.Arithmetic. (* Some of the material in abstract_algebra and canonical names could be selectively exported to the user, as is done in Groups/Group.v. *) Require Import Classes.interfaces.abstract_algebra. -Require Import Algebra.Groups.Group Algebra.Groups.Subgroup Algebra.Groups.Image. +Require Import Algebra.Groups.Group Algebra.Groups.Subgroup. Require Export Algebra.AbGroups.AbelianGroup Algebra.AbGroups.Biproduct Algebra.AbGroups.FiniteSum. Require Export Classes.theory.rings.