Skip to content

subgroups of direct products #2233

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Alizter wants to merge 1 commit into
base: master
Choose a base branch
from
Open

subgroups of direct products #2233

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
43 changes: 43 additions & 0 deletions theories/Algebra/Groups/Subgroup.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1183,3 +1183,46 @@ Proof.
apply equiv_iff_hprop_uncurried.
split; exact _.
Defined.

(** ** Subgroups of direct products *)

Definition subgroup_grp_prod_l {G H : Group} (K : Subgroup G)
: Subgroup (grp_prod G H)
:= subgroup_image grp_prod_inl K.
Comment on lines +1189 to +1191
Copy link
Collaborator

@jdchristensen jdchristensen Mar 23, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This definition of the induced subgroup of G x H is concise, but in some ways is more complicated than necessary. First, subgroup_image is defined in terms of grp_image, which adds a truncation, but because grp_prod_inl is an embedding, the truncation is not needed. So maybe we should have a subgroup_image_embedding that uses grp_image_embedding, and then use that here?

Second, grp_image_embedding adds a sigma type (via hfiber), but in this case even that is not necessary. The predicate for the induced subgroup can be defined to send (g, h) to K g * (h = 1). But then we'd have to prove that this does define a subgroup, which probably makes it not worthwhile.

Neither of these are very important, but I thought I'd mention them.


Definition subgroup_grp_prod_r {G H : Group} (K : Subgroup H)
: Subgroup (grp_prod G H)
:= subgroup_image grp_prod_inr K.

(** These two subgroups have trivial intersection. *)
Instance istrivial_intersection_subgroup_grp_prod {G H : Group}
(J : Subgroup G) (K : Subgroup H)
: IsTrivialGroup
(subgroup_intersection (subgroup_grp_prod_l J) (subgroup_grp_prod_r K)).
Proof.
intros [x y] [Jx Ky].
strip_truncations.
destruct Jx as [j p], Ky as [k q].
apply path_prod.
- exact (ap fst q^).
- exact (ap snd p^).
Defined.

(** TODO: use [pred_eq] *)
Copy link
Collaborator

@jdchristensen jdchristensen Mar 23, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What is pred_eq? Is this referring to something we discussed earlier?

Copy link
Collaborator Author

@Alizter Alizter Mar 23, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Predicate equality which is introduced in #2121 addressing #2202.

Copy link
Collaborator

@jdchristensen jdchristensen Mar 23, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, great. I'll try to get to 2121 soon.

(** The maximal subgroup of a direct product may be decomposed as the subgroup product of the factor subgroups. *)
Definition subgroup_eq_grp_prod_maximal {G H : Group}
: forall x, maximal_subgroup (grp_prod G H) x
<-> subgroup_product
(subgroup_grp_prod_l (maximal_subgroup G))
(subgroup_grp_prod_r (maximal_subgroup H)) x.
Comment on lines +1214 to +1217
Copy link
Collaborator

@jdchristensen jdchristensen Mar 23, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Another way to state the conclusion is

forall x, subgroup_product
            (subgroup_grp_prod_l (maximal_subgroup G))
            (subgroup_grp_prod_r (maximal_subgroup H)) x.

but maybe your way is better?

Independently, the two groups on the right can be simplified to (grp_image_embedding grp_prod_inl) and (grp_image_embedding grp_prod_inr), which avoids mentioning maximal groups, avoids subgroup_grp_prod_l and _r, and avoids the truncations. If your goal was this result, then using these versions of these groups would be a shorter way to get here.

Proof.
intros x; split.
- intros _; destruct x as [x y].
rewrite grp_prod_decompose.
apply subgroup_in_op.
+ apply subgroup_product_incl_l.
by rapply subgroup_image_in.
+ apply subgroup_product_incl_r.
by rapply subgroup_image_in.
- intros; exact tt.
Defined.
Loading