From b91d3d2ab5707c10d73d9dd6c9288198697691df Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Fri, 3 Jan 2025 21:07:03 +0000 Subject: [PATCH 1/3] more on trivial groups Signed-off-by: Ali Caglayan --- theories/Algebra/Groups/Subgroup.v | 49 ++++++++++++++++++++++++------ 1 file changed, 40 insertions(+), 9 deletions(-) diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v index b97b088a92..a2cc95d58c 100644 --- a/theories/Algebra/Groups/Subgroup.v +++ b/theories/Algebra/Groups/Subgroup.v @@ -1,4 +1,4 @@ -Require Import Basics Types HFiber WildCat.Core. +Require Import Basics Types HFiber WildCat.Core WildCat.Equiv. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType. @@ -188,6 +188,13 @@ Proof. apply inverse_mon_unit. Defined. +Definition trivial_subgroup_rec {G : Group} (H : Subgroup G) + : forall x, trivial_subgroup G x -> H x. +Proof. + snrapply paths_ind_r; cbn beta. + apply issubgroup_in_unit. +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. @@ -488,14 +495,38 @@ Proof. exact p. Defined. -(** The property of being the trivial subgroup is useful. *) -Definition IsTrivialSubgroup {G : Group} (H : Subgroup G) : Type := - forall x, H x <-> trivial_subgroup G x. -Existing Class IsTrivialSubgroup. - -Global Instance istrivialsubgroup_trivial_subgroup {G : Group} - : IsTrivialSubgroup (@trivial_subgroup G) - := ltac:(hnf; reflexivity). +(** The property of being the trivial group is useful. Note that any group can be automatically coerced to its maximal subgroup, so it makes sense for this predicate to be applied to groups in general. *) +Definition IsTrivialGroup@{i} {G : Group@{i}} (H : Subgroup@{i i} G) := + forall x, H x -> trivial_subgroup G x. +Existing Class IsTrivialGroup. + +Global Instance istrivial_trivial_subgroup {G : Group} + : IsTrivialGroup (trivial_subgroup G) + := fun x => idmap. + +(** Trivial groups are isomorphic to the trivial group. *) +Definition istrivial_iff_grp_iso_trivial_subgroup {G : Group} (H : Subgroup G) + : IsTrivialGroup H <-> (H : Group) $<~> trivial_subgroup G. +Proof. + split. + - intros T. + snrapply Build_GroupIsomorphism'. + + snrapply equiv_functor_sigma_id. + intros x. + rapply equiv_iff_hprop_uncurried. + split; only 1: apply T. + apply trivial_subgroup_rec. + + intros [x Hx] [y Hy]. + by rapply path_sigma_hprop. + - unfold IsTrivialGroup. + intros e x h. + change ((x; h).1 = (1; idpath).1). + snrapply (pr1_path (u:=(_;_)) (v:=(_;_))). + 1: apply subgroup_in_unit. + rhs_V nrapply (grp_homo_unit e^-1$). + apply moveL_equiv_V. + apply path_contr. +Defined. (** Intersection of two subgroups *) Definition subgroup_intersection {G : Group} (H K : Subgroup G) : Subgroup G. From 54d7184d9470ed6c233077bde6bcf3b17bfde42d Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Fri, 3 Jan 2025 21:05:44 +0000 Subject: [PATCH 2/3] group unit lemmas Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/Centralizer.v | 8 +++----- theories/Algebra/Groups/Group.v | 11 ++++++++--- 2 files changed, 11 insertions(+), 8 deletions(-) diff --git a/theories/Algebra/AbGroups/Centralizer.v b/theories/Algebra/AbGroups/Centralizer.v index 8c3a8da8f7..6e0aceacd7 100644 --- a/theories/Algebra/AbGroups/Centralizer.v +++ b/theories/Algebra/AbGroups/Centralizer.v @@ -11,10 +11,8 @@ Local Open Scope mc_mult_scope. Definition centralizer {G : Group} (g : G) := fun h => g * h = h * g. -Definition centralizer_unit {G : Group} (g : G) : centralizer g mon_unit. -Proof. - exact (grp_unit_r _ @ (grp_unit_l _)^). -Defined. +Definition centralizer_unit {G : Group} (g : G) : centralizer g mon_unit + := grp_g1_1g _ _ idpath. Definition centralizer_sgop {G : Group} (g h k : G) (p : centralizer g h) (q : centralizer g k) @@ -33,7 +31,7 @@ Definition centralizer_inverse {G : Group} (g h : G) Proof. unfold centralizer in *. symmetry. - refine ((grp_unit_r _)^ @ _ @ grp_unit_l _). + apply grp_g1_1g. refine (ap ((_ * g) *.) (grp_inv_r h)^ @ _ @ ap (.* (g * _)) (grp_inv_l h)). refine (grp_assoc _ _ _ @ _ @ (grp_assoc _ _ _)^). refine (ap (.* h^) _). diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v index 2c489454e5..76d1d782d8 100644 --- a/theories/Algebra/Groups/Group.v +++ b/theories/Algebra/Groups/Group.v @@ -465,6 +465,12 @@ Section GroupEquations. Definition grp_inv_gV_g : (x * y^) * y = x := (grp_assoc _ _ _)^ @ ap (x *.) (grp_inv_l y) @ grp_unit_r x. + Definition grp_1g_g1 : x = y <~> 1 * x = y * 1 + := equiv_concat_r (grp_unit_r _)^ _ oE equiv_concat_l (grp_unit_l _) _. + + Definition grp_g1_1g : x = y <~> x * 1 = 1 * y + := equiv_concat_r (grp_unit_l _)^ _ oE equiv_concat_l (grp_unit_r _) _. + End GroupEquations. (** ** Cancelation lemmas *) @@ -678,7 +684,7 @@ Definition grp_pow_commutes {G : Group} (n : Int) (g h : G) : h * (grp_pow g n) = (grp_pow g n) * h. Proof. induction n. - - exact (grp_unit_r _ @ (grp_unit_l _)^). + - by apply grp_g1_1g. - rewrite grp_pow_succ. nrapply grp_commutes_op; assumption. - rewrite grp_pow_pred. @@ -1168,8 +1174,7 @@ Definition grp_conj_unit {G : Group} : grp_conj (G:=G) 1 $== Id _. Proof. intros x. apply grp_moveR_gV. - rhs nrapply grp_unit_r. - nrapply grp_unit_l. + by nrapply grp_1g_g1. Defined. (** Conjugation commutes with group homomorphisms. *) From ad43e040880af40f62f0fb724037e5dda9fe33cc Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sat, 4 Jan 2025 17:44:41 +0000 Subject: [PATCH 3/3] address review comments Signed-off-by: Ali Caglayan --- theories/Algebra/Groups/Subgroup.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v index a2cc95d58c..0878378979 100644 --- a/theories/Algebra/Groups/Subgroup.v +++ b/theories/Algebra/Groups/Subgroup.v @@ -496,9 +496,8 @@ Proof. Defined. (** The property of being the trivial group is useful. Note that any group can be automatically coerced to its maximal subgroup, so it makes sense for this predicate to be applied to groups in general. *) -Definition IsTrivialGroup@{i} {G : Group@{i}} (H : Subgroup@{i i} G) := - forall x, H x -> trivial_subgroup G x. -Existing Class IsTrivialGroup. +Class IsTrivialGroup@{i} {G : Group@{i}} (H : Subgroup@{i i} G) := + istrivialgroup : forall x, H x -> trivial_subgroup G x. Global Instance istrivial_trivial_subgroup {G : Group} : IsTrivialGroup (trivial_subgroup G) @@ -506,7 +505,8 @@ Global Instance istrivial_trivial_subgroup {G : Group} (** Trivial groups are isomorphic to the trivial group. *) Definition istrivial_iff_grp_iso_trivial_subgroup {G : Group} (H : Subgroup G) - : IsTrivialGroup H <-> (H : Group) $<~> trivial_subgroup G. + : IsTrivialGroup H + <-> (subgroup_group H $<~> subgroup_group (trivial_subgroup G)). Proof. split. - intros T.