Library HoTT.Algebra.AbGroups.AbHom

Require Import Basics Types.
Require Import WildCat HSet Truncations.Core Modalities.ReflectiveSubuniverse.
Require Import Groups.Group Groups.QuotientGroup AbelianGroup Biproduct.

Homomorphisms from a group to an abelian group form an abelian group.

In this file, we use additive notation for the group operation, even though some of the groups we deal with are not assumed to be abelian.

Local Open Scope mc_add_scope.

The sum of group homomorphisms f and g is fun a ⇒ f(a) + g(a). While the group *laws* require Funext, the operations do not, so we make them instances.

Instance sgop_hom {A : Group} {B : AbGroup} : SgOp (A $-> B).
Proof.
intros f g.
exact (grp_homo_compose ab_codiagonal (grp_prod_corec f g)).
Defined.

We can negate a group homomorphism A → B by post-composing with ab_homo_negation : B → B.

Instance inverse_hom {A : Group} {B : AbGroup}
: Inverse (@Hom Group _ A B) := grp_homo_compose ab_homo_negation.

For A and B groups, with B abelian, homomorphisms A $-> B form an abelian group.

Definition grp_hom `{Funext} (A : Group) (B : AbGroup) : Group.
Proof.
  snapply (Build_Group' (GroupHomomorphism A B) sgop_hom grp_homo_const inverse_hom).
  1: exact _.
  all: hnf; intros; apply equiv_path_grouphomomorphism; intro; cbn.
  - apply associativity.
  - apply left_identity.
  - apply left_inverse.
Defined.

Definition ab_hom `{Funext} (A : Group) (B : AbGroup) : AbGroup.
Proof.
  snapply (Build_AbGroup (grp_hom A B)).
  intros f g; cbn.
  apply equiv_path_grouphomomorphism; intro x; cbn.
  apply commutativity.
Defined.

Coequalizers

Using the cokernel and addition and negation for the homs of abelian groups, we can define the coequalizer of two group homomorphisms as the cokernel of their difference.

Definition ab_coeq {A B : AbGroup} (f g : GroupHomomorphism A B)
  := ab_cokernel ((-f ) + g).

Definition ab_coeq_in {A B : AbGroup} {f g : A $-> B} : B $-> ab_coeq f g.
Proof.
  exact grp_quotient_map.
Defined.

Definition ab_coeq_glue {A B : AbGroup} {f g : A $-> B}
  : ab_coeq_in (f:=f) (g:=g) $o f $== ab_coeq_in $o g.
Proof.
  intros x.
  napply qglue.
  apply tr.
  by ∃ x.
Defined.

Definition ab_coeq_rec {A B : AbGroup} {f g : A $-> B}
  {C : AbGroup} (i : B $-> C) (p : i $o f $== i $o g)
  : ab_coeq f g $-> C.
Proof.
  snapply (grp_quotient_rec _ _ i).
  cbn.
  intros b H.
  strip_truncations.
  destruct H as [a q].
  destruct q; simpl.
  lhs napply grp_homo_op.
  lhs napply (ap (+ _)).
  1: apply grp_homo_inv.
  apply grp_moveL_M1 ^-1.
  exact (p a)^.
Defined.

Definition ab_coeq_rec_beta_in {A B : AbGroup} {f g : A $-> B}
  {C : AbGroup} (i : B $-> C) (p : i $o f $== i $o g)
  : ab_coeq_rec i p $o ab_coeq_in $== i
  := fun _ ⇒ idpath.

Definition ab_coeq_ind_hprop {A B f g} (P : @ab_coeq A B f g → Type)
  `{∀ x , IsHProp (P x )}
  (i : ∀ b , P (ab_coeq_in b))
  : ∀ x , P x.
Proof.
  rapply Quotient_ind_hprop.
  exact i.
Defined.

Definition ab_coeq_ind_homotopy {A B C f g}
  {l r : @ab_coeq A B f g $-> C}
  (p : l $o ab_coeq_in $== r $o ab_coeq_in)
  : l $== r.
Proof.
  srapply ab_coeq_ind_hprop.
  exact p.
Defined.

Definition functor_ab_coeq {A B : AbGroup} {f g : A $-> B} {A' B' : AbGroup} {f' g' : A' $-> B'}
  (a : A $-> A') (b : B $-> B') (p : f' $o a $== b $o f) (q : g' $o a $== b $o g)
  : ab_coeq f g $-> ab_coeq f' g'.
Proof.
  snapply ab_coeq_rec.
  1: exact (ab_coeq_in $o b).
  refine (cat_assoc _ _ _ $@ _ $@ cat_assoc_opp _ _ _).
  refine ((_ $@L p^$) $@ _ $@ (_ $@L q)).
  refine (cat_assoc_opp _ _ _ $@ (_ $@R a) $@ cat_assoc _ _ _).
  exact ab_coeq_glue.
Defined.

Definition functor2_ab_coeq {A B : AbGroup} {f g : A $-> B} {A' B' : AbGroup} {f' g' : A' $-> B'}
  {a a' : A $-> A'} {b b' : B $-> B'}
  (p : f' $o a $== b $o f) (q : g' $o a $== b $o g)
  (p' : f' $o a' $== b' $o f) (q' : g' $o a' $== b' $o g)
  (s : b $== b')
  : functor_ab_coeq a b p q $== functor_ab_coeq a' b' p' q'.
Proof.
  snapply ab_coeq_ind_homotopy.
  intros x.
  exact (ap ab_coeq_in (s x)).
Defined.

Definition functor_ab_coeq_compose {A B : AbGroup} {f g : A $-> B}
  {A' B' : AbGroup} {f' g' : A' $-> B'}
  (a : A $-> A') (b : B $-> B') (p : f' $o a $== b $o f) (q : g' $o a $== b $o g)
  {A'' B'' : AbGroup} {f'' g'' : A'' $-> B''}
  (a' : A' $-> A'') (b' : B' $-> B'')
  (p' : f'' $o a' $== b' $o f') (q' : g'' $o a' $== b' $o g')
  : functor_ab_coeq a' b' p' q' $o functor_ab_coeq a b p q
  $== functor_ab_coeq (a' $o a) (b' $o b) (hconcat p p') (hconcat q q').
Proof.
  snapply ab_coeq_ind_homotopy.
  simpl; reflexivity.
Defined.

Definition functor_ab_coeq_id {A B : AbGroup} (f g : A $-> B)
  : functor_ab_coeq (f:=f) (g:=g) (Id _) (Id _) (hrefl _) (hrefl _) $== Id _.
Proof.
  snapply ab_coeq_ind_homotopy.
  reflexivity.
Defined.

Definition grp_iso_ab_coeq {A B : AbGroup} {f g : A $-> B}
  {A' B' : AbGroup} {f' g' : A' $-> B'}
  (a : A $<~> A') (b : B $<~> B') (p : f' $o a $== b $o f) (q : g' $o a $== b $o g)
  : ab_coeq f g $<~> ab_coeq f' g'.
Proof.
  snapply cate_adjointify.
  - exact (functor_ab_coeq a b p q).
  - exact (functor_ab_coeq a^-1$ b^-1$ (hinverse _ _ p) (hinverse _ _ q)).
  - nrefine (functor_ab_coeq_compose _ _ _ _ _ _ _ _
      $@ functor2_ab_coeq _ _ _ _ _ $@ functor_ab_coeq_id _ _).
    tapply cate_isretr.
  - nrefine (functor_ab_coeq_compose _ _ _ _ _ _ _ _
      $@ functor2_ab_coeq _ _ _ _ _ $@ functor_ab_coeq_id _ _).
    tapply cate_issect.
Defined.

The bifunctor ab_hom

Instance is0functor_ab_hom01 `{Funext} {A : Group ^op}
  : Is0Functor (ab_hom A).
Proof.
  snapply (Build_Is0Functor _ AbGroup); intros B B' f.
  snapply Build_GroupHomomorphism.
  1: exact (fun g ⇒ grp_homo_compose f g).
  intros phi psi.
  apply equiv_path_grouphomomorphism; intro a; cbn.
  exact (grp_homo_op f _ _).
Defined.

Instance is0functor_ab_hom10 `{Funext} {B : AbGroup@{u }}
  : Is0Functor (flip (ab_hom : Group ^op → AbGroup → AbGroup) B).
Proof.
  snapply (Build_Is0Functor (Group ^op) AbGroup); intros A A' f.
  snapply Build_GroupHomomorphism.
  1: exact (fun g ⇒ grp_homo_compose g f).
  intros phi psi.
  by apply equiv_path_grouphomomorphism.
Defined.

Instance is1functor_ab_hom01 `{Funext} {A : Group ^op}
  : Is1Functor (ab_hom A).
Proof.
  napply Build_Is1Functor.
  - intros B B' f g p phi.
    apply equiv_path_grouphomomorphism; intro a; cbn.
    exact (p (phi a)).
  - intros B phi.
    by apply equiv_path_grouphomomorphism.
  - intros B C D f g phi.
    by apply equiv_path_grouphomomorphism.
Defined.

Instance is1functor_ab_hom10 `{Funext} {B : AbGroup@{u }}
  : Is1Functor (flip (ab_hom : Group ^op → AbGroup → AbGroup) B).
Proof.
  napply Build_Is1Functor.
  - intros A A' f g p phi.
    apply equiv_path_grouphomomorphism; intro a; cbn.
    exact (ap phi (p a)).
  - intros A phi.
    by apply equiv_path_grouphomomorphism.
  - intros A C D f g phi.
    by apply equiv_path_grouphomomorphism.
Defined.

Instance is0bifunctor_ab_hom `{Funext}
  : Is0Bifunctor (ab_hom : Group ^op → AbGroup → AbGroup).
Proof.
  rapply Build_Is0Bifunctor''.
Defined.

Instance is1bifunctor_ab_hom `{Funext}
  : Is1Bifunctor (ab_hom : Group ^op → AbGroup → AbGroup).
Proof.
  napply Build_Is1Bifunctor''.
  1,2: exact _.
  intros A A' f B B' g phi; cbn.
  by apply equiv_path_grouphomomorphism.
Defined.

Properties of ab_hom

Precomposition with a surjection is an embedding.

(* This could be deduced from isembedding_precompose_surjection_hset, but relating precomposition of homomorphisms with precomposition of the underlying maps is tedious, so we give a direct proof. *)
Instance isembedding_precompose_surjection_ab `{Funext} {A B C : AbGroup}
  (f : A $-> B) `{IsSurjection f}
  : IsEmbedding (fmap10 (A:=Group ^op) ab_hom f C).
Proof.
  apply isembedding_isinj_hset; intros g0 g1 p.
  apply equiv_path_grouphomomorphism.
  rapply (conn_map_elim (Tr (-1)) f).
  exact (equiv_path_grouphomomorphism ^-1 p).
Defined.