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.

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

Elimination principles for GroupCoeq #2184

Merged
Next Next commit
constructors and functoriality for GroupCoeq
Signed-off-by: Ali Caglayan <alizter@gmail.com>

<!-- ps-id: 4ccb2a6c-3b11-4ba5-9be2-530334d3f40d -->
  • Loading branch information
Alizter authored and jdchristensen committed Mar 15, 2025
commit d7356e94ada739cc198374280a91f2ee0ead4af4
88 changes: 81 additions & 7 deletions theories/Algebra/Groups/GroupCoeq.v
Original file line number Diff line number Diff line change
Expand Up @@ -4,17 +4,51 @@ Require Import Truncations.Core.
Require Import Algebra.Groups.Group.
Require Import Colimits.Coeq.
Require Import Algebra.Groups.FreeProduct.
Require Import List.Core.

Local Open Scope mc_scope.
Local Open Scope mc_mult_scope.

(** Coequalizers of group homomorphisms *)

Definition GroupCoeq {A B : Group} (f g : A $-> B) : Group.
Proof.
rapply (AmalgamatedFreeProduct (FreeProduct A A) A B).
1,2: apply FreeProduct_rec.
+ exact grp_homo_id.
+ exact grp_homo_id.
+ exact f.
+ exact g.
nrapply (AmalgamatedFreeProduct (FreeProduct A A) A B).
- exact (FreeProduct_rec (Id _) (Id _)).
- exact (FreeProduct_rec f g).
Defined.

Definition groupcoeq_in {A B : Group} {f g : A $-> B}
: B $-> GroupCoeq f g
:= amal_inr.

Definition groupcoeq_glue {A B : Group} {f g : A $-> B}
: groupcoeq_in (f:=f) (g:=g) $o f $== groupcoeq_in $o g.
Proof.
intros x; simpl.
rewrite <- (right_identity (f x)).
rewrite <- (right_identity (g x)).
rhs_V nrapply (amal_glue (freeproduct_inr x)).
symmetry.
nrapply (amal_glue (freeproduct_inl x)).
Defined.

Definition groupcoeq_rec {A B C : Group} (f g : A $-> B)
(h : B $-> C) (p : h $o f $== h $o g)
: GroupCoeq f g $-> C.
Proof.
snrapply AmalgamatedFreeProduct_rec.
- exact (h $o f).
- exact h.
- snrapply freeproduct_ind_homotopy.
+ change (?f1 $o ?f2 $o ?f3 $o ?f4 $== ?f5 $o ?f6 $o ?f7)
with (f1 $o f2 $o (f3 $o f4) $== f5 $o (f6 $o f7)).
exact ((_ $@L freeproduct_rec_beta_inl _ _) $@ cat_idr _
$@ (_ $@L freeproduct_rec_beta_inl _ _)^$).
+ change (?f1 $o ?f2 $o ?f3 $o ?f4 $== ?f5 $o ?f6 $o ?f7)
with (f1 $o f2 $o (f3 $o f4) $== f5 $o (f6 $o f7)).
exact ((_ $@L freeproduct_rec_beta_inr _ _) $@ (cat_idr _ $@ p)
$@ (_ $@L freeproduct_rec_beta_inr _ _)^$).
Defined.

Definition equiv_groupcoeq_rec `{Funext} {A B C : Group} (f g : GroupHomomorphism A B)
Expand Down Expand Up @@ -55,6 +89,46 @@ Proof.
pose (q1 := p (freeproduct_inl y)).
simpl in q1.
rewrite 2 right_identity in q1.
exact q1^. }
symmetry.
exact q1. }
hnf; intros; apply path_ishprop.
Defined.

Definition groupcoeq_ind_hprop {G H : Group} {f g : G $-> H}
(P : GroupCoeq f g -> Type) `{forall x, IsHProp (P x)}
(c : forall h, P (groupcoeq_in h))
(Hop : forall x y, P x -> P y -> P (x * y))
: forall x, P x.
Comment on lines +77 to +81
Copy link
Collaborator

Choose a reason for hiding this comment

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

Since the map from H to the coequalizer is surjective, the Hop assumption shouldn't be needed. But I'm not sure how to show that this map is surjective using the current definition of coequalizer.

Proof.
srapply amalgamatedfreeproduct_ind_hprop.
- intros x.
rewrite <- (right_identity x).
refine ((amal_glue (freeproduct_inl x))^ #_).
simpl.
rewrite (right_identity (f x)).
exact (c (f x)).
- exact c.
- exact Hop.
Defined.

Definition groupcoeq_ind_homotopy {G H K : Group} {f g : G $-> H}
{h h' : GroupCoeq f g $-> K}
(r : h $o groupcoeq_in $== h' $o groupcoeq_in)
: h $== h'.
Proof.
rapply (groupcoeq_ind_hprop _ r).
intros x y p q; by nrapply grp_homo_op_agree.
Defined.

Definition functor_groupcoeq
{G H : Group} {f g : G $-> H} {G' H' : Group} {f' g' : G' $-> H'}
(h : G $-> G') (k : H $-> H')
(p : k $o f $== f' $o h) (q : k $o g $== g' $o h)
: GroupCoeq f g $-> GroupCoeq f' g'.
Proof.
refine (groupcoeq_rec f g (groupcoeq_in $o k) _).
refine (cat_assoc _ _ _ $@ _ $@ cat_assoc_opp _ _ _).
refine ((_ $@L p) $@ _ $@ (_ $@L q^$)).
refine (cat_assoc_opp _ _ _ $@ (_ $@R _) $@ cat_assoc _ _ _).
apply groupcoeq_glue.
Defined.