Skip to content
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

Improve mapping out of a generated subgroup #2180

Merged
merged 4 commits into from
Jan 4, 2025
Merged

Improve mapping out of a generated subgroup #2180

Changes from 1 commit
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
78860cb
better subgroup_generated_rec lemma
Alizter Jan 3, 2025
6b99b15
change x to g
Alizter Jan 3, 2025
10b911b
rename variables
Alizter Jan 3, 2025
88934ed
simplify subgroup_generated_rec further and add comment
Alizter Jan 3, 2025
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
26 changes: 17 additions & 9 deletions theories/Algebra/Groups/Subgroup.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -557,20 +557,28 @@ Definition subgroup_generated_gen_incl {G : Group} {X : G -> Type} (g : G) (H :
: subgroup_generated X
:= (g; tr (sgt_in H)).

Definition subgroup_generated_rec {G H : Group} (X : G -> Type) (S : Subgroup H)
(f : G $-> H) (i : forall x, X x -> S (f x))
: forall x, subgroup_generated X x -> S (f x).
Copy link
Collaborator

Choose a reason for hiding this comment

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

This result is really a combination of two things. First, consider the special case when f is the identity map. Then it says that subgroup_generated X is the smallest subgroup containing the generating set. I think this is something worth recording on its own.

And then this result follows from that special case, since S o f is again a subgroup of G (by subgroup_preimage).

I think separating this out into those two pieces would be useful and a bit shorter (since the current approach redoes subgroup_preimage).

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I simplified the lemma like you suggested and added a comment. I'll add the preimage version back in if it becomes useful.

Copy link
Collaborator

Choose a reason for hiding this comment

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

Sounds good. Do you think subgroup_generated_rec should be renamed to something like subgroup_generated_minimal?

Copy link
Collaborator

Choose a reason for hiding this comment

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

Did you see the previous comment?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I missed that. Whats wrong with subgroup_generated_rec?

Copy link
Collaborator

Choose a reason for hiding this comment

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

What the result is saying is that every subgroup containing the generators contains the generated subgroup, so the generated subgroup is the minimal subgroup containing the generators. So I thought a name in that direction might make more sense. subgroup_generated_rec would seem more appropriate for something that defines a function from the generated subgroup to an arbitrary group (or even an arbitrary type).

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

That's a good point. I think I'll hold off on that for now. At some point I should go around and start using inclusions like we do in Ideal.v for subgroups, that way it would make sense to call this a sg_incl or something to that effect.

Proof.
intros x; rapply Trunc_rec; intros p.
Alizter marked this conversation as resolved.
Show resolved Hide resolved
induction p as [g Xg | | g h p1 IHp1 p2 IHp2].
- by apply i.
- rewrite grp_homo_unit.
apply subgroup_in_unit.
- rewrite grp_homo_op, grp_homo_inv.
by apply subgroup_in_op_inv.
Defined.

(** If [f : G $-> H] is a group homomorphism and [X] and [Y] are subsets of [G] and [H] such that [f] maps [X] into [Y], then [f] sends the subgroup generated by [X] into the subgroup generated by [Y]. *)
Definition functor_subgroup_generated {G H : Group} (X : G -> Type) (Y : H -> Type)
(f : G $-> H) (preserves : forall g, X g -> Y (f g))
: forall g, subgroup_generated X g -> subgroup_generated Y (f g).
Proof.
intro g.
apply Trunc_functor.
intro p.
induction p as [g i | | g h p1 IHp1 p2 IHp2].
- apply sgt_in, preserves, i.
- rewrite grp_homo_unit.
apply sgt_unit.
- rewrite grp_homo_op, grp_homo_inv.
by apply sgt_op.
apply subgroup_generated_rec.
intros g x.
Alizter marked this conversation as resolved.
Show resolved Hide resolved
apply tr, sgt_in.
by apply preserves.
Defined.

(** The product of two subgroups. *)
Expand Down
Loading