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

Jump to bottom

ind_homotopy lemma for FreeAbGroup #2113

Merged
merged 2 commits into from
Oct 13, 2024
Merged

ind_homotopy lemma for FreeAbGroup #2113

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
b519a42
ind_homotopy lemma for FreeAbGroup
Alizter Oct 10, 2024
a88bf22
remove Abel_rec_hprop
Alizter Oct 13, 2024
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
10 changes: 9 additions & 1 deletion theories/Algebra/AbGroups/Abelianization.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -149,7 +149,7 @@ Section Abel.
srapply Coeq_ind_hprop.
exact a.
Defined.

(** And its recursion version. *)
Definition Abel_rec_hprop (P : Type) `{IsHProp P}
Alizter marked this conversation as resolved.
Show resolved Hide resolved
(a : G -> P)
Expand Down Expand Up @@ -342,6 +342,14 @@ Proof.
apply grp_homo_op.
Defined.

Definition abel_ind_homotopy {G H : Group} {f g : Hom (A:=Group) (abel G) H}
(p : f $o abel_unit $== g $o abel_unit)
: f $== g.
Proof.
rapply Abel_ind_hprop.
rapply p.
Defined.

(** Finally we can prove that our construction abel is an abelianization. *)
Global Instance isabelianization_abel {G : Group}
: IsAbelianization (abel G) abel_unit.
Expand Down
10 changes: 10 additions & 0 deletions theories/Algebra/AbGroups/FreeAbelianGroup.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,16 @@ Definition FreeAbGroup_rec_beta_in {S : Type} {A : AbGroup} (f : S -> A)
: FreeAbGroup_rec f o freeabgroup_in == f
:= fun _ => idpath.

Definition FreeAbGroup_ind_homotopy {X : Type} {A : AbGroup}
{f f' : FreeAbGroup X $-> A}
(p : forall x, f (freeabgroup_in x) = f' (freeabgroup_in x))
: f $== f'.
Proof.
snrapply abel_ind_homotopy.
snrapply FreeGroup_ind_homotopy.
snrapply p.
Defined.

(** The abelianization of a free group on a set is a free abelian group on that set. *)
Global Instance isfreeabgroupon_isabelianization_isfreegroup `{Funext}
{S : Type} {G : Group} {A : AbGroup} (f : S -> G) (g : G $-> A)
Expand Down
Loading