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

group of maximal subgroup of a group is iso to said group #2187

Merged
merged 2 commits into from
Jan 8, 2025
Merged

group of maximal subgroup of a group is iso to said group #2187

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
fb52541
sugroup_group of maximal_subgroup is iso to original group
Alizter Jan 3, 2025
3b5d305
clarify comment
Alizter Jan 7, 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
9 changes: 9 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 @@ -222,6 +222,15 @@ Defined.
Coercion maximal_subgroup : Group >-> Subgroup.
Add Printing Coercion maximal_subgroup.

(** The group associated to the maximal subgroup is the original group. *)
Definition grp_iso_subgroup_group_maximal (G : Group)
: subgroup_group (maximal_subgroup G) $<~> G.
Proof.
snrapply Build_GroupIsomorphism'.
- rapply equiv_sigma_contr.
- hnf; reflexivity.
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).
Expand Down
Loading