Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
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).
A: Group
B: AbGroup
SgOp (A $-> B)
Proof.
A: Group
B: AbGroup
SgOp (A $-> B)
  intros f g.
A: Group
B: AbGroup
f, g: A $-> B
A $-> B
  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.
H: Funext
A: Group
B: AbGroup
Group
Proof.
H: Funext
A: Group
B: AbGroup
Group
  snapply (Build_Group' (GroupHomomorphism A B) sgop_hom grp_homo_const inverse_hom).
H: Funext
A: Group
B: AbGroup
IsHSet (GroupHomomorphism A B)
H: Funext
A: Group
B: AbGroup
Associative sg_op
H: Funext
A: Group
B: AbGroup
LeftIdentity sg_op 0
H: Funext
A: Group
B: AbGroup
LeftInverse sg_op inv 0
  1: exact _.
H: Funext
A: Group
B: AbGroup
Associative sg_op
H: Funext
A: Group
B: AbGroup
LeftIdentity sg_op 0
H: Funext
A: Group
B: AbGroup
LeftInverse sg_op inv 0
  all: hnf; intros; apply equiv_path_grouphomomorphism; intro; cbn.
H: Funext
A: Group
B: AbGroup
x, y, z: GroupHomomorphism A B
x0: A
x x0 + (y x0 + z x0) = x x0 + y x0 + z x0
H: Funext
A: Group
B: AbGroup
y: GroupHomomorphism A B
x: A
group_unit + y x = y x
H: Funext
A: Group
B: AbGroup
x: GroupHomomorphism A B
x0: A
- x x0 + x x0 = group_unit
  -
H: Funext
A: Group
B: AbGroup
x, y, z: GroupHomomorphism A B
x0: A
x x0 + (y x0 + z x0) = x x0 + y x0 + z x0 apply associativity.
  -
H: Funext
A: Group
B: AbGroup
y: GroupHomomorphism A B
x: A
group_unit + y x = y x apply left_identity.
  -
H: Funext
A: Group
B: AbGroup
x: GroupHomomorphism A B
x0: A
- x x0 + x x0 = group_unit apply left_inverse.
Defined.

Definition ab_hom `{Funext} (A : Group) (B : AbGroup) : AbGroup.
H: Funext
A: Group
B: AbGroup
AbGroup
Proof.
H: Funext
A: Group
B: AbGroup
AbGroup
  snapply (Build_AbGroup (grp_hom A B)).
H: Funext
A: Group
B: AbGroup
Commutative sg_op
  intros f g; cbn.
H: Funext
A: Group
B: AbGroup
f, g: grp_hom A B
sgop_hom f g = sgop_hom g f
  apply equiv_path_grouphomomorphism; intro x; cbn.
H: Funext
A: Group
B: AbGroup
f, g: grp_hom A B
x: A
f x + g x = g x + f x
  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 : A $-> B)
  := ab_cokernel ((-f) + g).

Definition ab_coeq_in {A B : AbGroup} {f g : A $-> B} : B $-> ab_coeq f g.
A, B: AbGroup
f, g: A $-> B
B $-> ab_coeq f g
Proof.
A, B: AbGroup
f, g: A $-> B
B $-> ab_coeq f g
  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.
A, B: AbGroup
f, g: A $-> B
ab_coeq_in $o f $== ab_coeq_in $o g
Proof.
A, B: AbGroup
f, g: A $-> B
ab_coeq_in $o f $== ab_coeq_in $o g
  intros x.
A, B: AbGroup
f, g: A $-> B
x: A
(ab_coeq_in $o f) x = (ab_coeq_in $o g) x
  napply qglue.
A, B: AbGroup
f, g: A $-> B
x: A
in_cosetL
  {|
    normalsubgroup_subgroup := grp_image (- f + g);
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup B (grp_image (- f + g))
  |} (f x) (g x)
  apply tr.
A, B: AbGroup
f, g: A $-> B
x: A
{x0 : A & (- f + g) x0 = - f x + g x}
  by exists 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.
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.
A, B: AbGroup
f, g: A $-> B
C: AbGroup
i: B $-> C
p: i $o f $== i $o g
ab_coeq f g $-> C
  snapply (grp_quotient_rec _ _ i).
A, B: AbGroup
f, g: A $-> B
C: AbGroup
i: B $-> C
p: i $o f $== i $o g
forall n : B,
{|
  normalsubgroup_subgroup := grp_image (- f + g);
  normalsubgroup_isnormal :=
    isnormal_ab_subgroup B (grp_image (- f + g))
|} n -> i n = 0
  cbn.
A, B: AbGroup
f, g: A $-> B
C: AbGroup
i: B $-> C
p: i $o f $== i $o g
forall n : B,
Trunc (-1) {x : A & - f x + g x = n} -> i n = 0
  intros b H.
A, B: AbGroup
f, g: A $-> B
C: AbGroup
i: B $-> C
p: i $o f $== i $o g
b: B
H: Trunc (-1) {x : A & - f x + g x = b}
i b = 0
  strip_truncations.
A, B: AbGroup
f, g: A $-> B
C: AbGroup
i: B $-> C
p: i $o f $== i $o g
b: B
H: {x : A & - f x + g x = b}
i b = 0
  destruct H as [a q].
A, B: AbGroup
f, g: A $-> B
C: AbGroup
i: B $-> C
p: i $o f $== i $o g
b: B
a: A
q: - f a + g a = b
i b = 0
  destruct q; simpl.
A, B: AbGroup
f, g: A $-> B
C: AbGroup
i: B $-> C
p: i $o f $== i $o g
a: A
i (- f a + g a) = 0
  lhs napply grp_homo_op.
A, B: AbGroup
f, g: A $-> B
C: AbGroup
i: B $-> C
p: i $o f $== i $o g
a: A
i (- f a) + i (g a) = 0
  lhs napply (ap (+ _)).
A, B: AbGroup
f, g: A $-> B
C: AbGroup
i: B $-> C
p: i $o f $== i $o g
a: A
i (- f a) = ?Goal
A, B: AbGroup
f, g: A $-> B
C: AbGroup
i: B $-> C
p: i $o f $== i $o g
a: A
?Goal + i (g a) = 0
  1: apply grp_homo_inv.
A, B: AbGroup
f, g: A $-> B
C: AbGroup
i: B $-> C
p: i $o f $== i $o g
a: A
- i (f a) + i (g a) = 0
  apply grp_moveL_M1^-1.
A, B: AbGroup
f, g: A $-> B
C: AbGroup
i: B $-> C
p: i $o f $== i $o g
a: A
i (g a) = i (f a)
  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)
  `{forall x, IsHProp (P x)}
  (i : forall b, P (ab_coeq_in b))
  : forall x, P x.
A, B: AbGroup
f, g: A $-> B
P: ab_coeq f g -> Type
H: forall x : ab_coeq f g, IsHProp (P x)
i: forall b : B, P (ab_coeq_in b)
forall x : ab_coeq f g, P x
Proof.
A, B: AbGroup
f, g: A $-> B
P: ab_coeq f g -> Type
H: forall x : ab_coeq f g, IsHProp (P x)
i: forall b : B, P (ab_coeq_in b)
forall x : ab_coeq f g, P x
  rapply Quotient_ind_hprop.
A, B: AbGroup
f, g: A $-> B
P: ab_coeq f g -> Type
H: forall x : ab_coeq f g, IsHProp (P x)
i: forall b : B, P (ab_coeq_in b)
forall a : B,
P
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup :=
            grp_image (- f + g);
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup B
              (grp_image (- f + g))
        |}) a)
  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.
A, B, C: AbGroup
f, g: A $-> B
l, r: ab_coeq f g $-> C
p: l $o ab_coeq_in $== r $o ab_coeq_in
l $== r
Proof.
A, B, C: AbGroup
f, g: A $-> B
l, r: ab_coeq f g $-> C
p: l $o ab_coeq_in $== r $o ab_coeq_in
l $== r
  srapply ab_coeq_ind_hprop.
A, B, C: AbGroup
f, g: A $-> B
l, r: ab_coeq f g $-> C
p: l $o ab_coeq_in $== r $o ab_coeq_in
forall b : B,
(fun x : ab_coeq f g =>
 (grp_homo_map
  :
  GroupHomomorphism (ab_coeq f g) C ->
  ab_coeq f g $-> C) l x =
 (grp_homo_map
  :
  GroupHomomorphism (ab_coeq f g) C ->
  ab_coeq f g $-> C) r x) (ab_coeq_in b)
  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'.
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.
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'
  snapply ab_coeq_rec.
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
B $-> ab_coeq f' g'
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
?i $o f $== ?i $o g
  1: exact (ab_coeq_in $o b).
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_in $o b $o f $== ab_coeq_in $o b $o g
  refine (cat_assoc _ _ _ $@ _ $@ cat_assoc_opp _ _ _).
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_in $o (b $o f) $== ab_coeq_in $o (b $o g)
  refine ((_ $@L p^$) $@ _ $@ (_ $@L q)).
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_in $o (f' $o a) $== ab_coeq_in $o (g' $o a)
  refine (cat_assoc_opp _ _ _ $@ (_ $@R a) $@ cat_assoc _ _ _).
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_in $o f' $== ab_coeq_in $o g'
  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'.
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.
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'
  snapply ab_coeq_ind_homotopy.
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 $o ab_coeq_in $==
functor_ab_coeq a' b' p' q' $o ab_coeq_in
  intros x.
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'
x: B
(functor_ab_coeq a b p q $o ab_coeq_in) x =
(functor_ab_coeq a' b' p' q' $o ab_coeq_in) 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').
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) (p $@h p')
  (q $@h q')
Proof.
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) (p $@h p')
  (q $@h q')
  snapply ab_coeq_ind_homotopy.
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 $o
ab_coeq_in $==
functor_ab_coeq (a' $o a) (b' $o b) (p $@h p')
  (q $@h q') $o ab_coeq_in
  simpl; reflexivity.
Defined.

Definition functor_ab_coeq_id {A B : AbGroup} (f g : A $-> B)
  : functor_ab_coeq (Id _) (Id _) (hrefl f) (hrefl g) $== Id _.
A, B: AbGroup
f, g: A $-> B
functor_ab_coeq (Id A) (Id B) (hrefl f) (hrefl g) $==
Id (ab_coeq f g)
Proof.
A, B: AbGroup
f, g: A $-> B
functor_ab_coeq (Id A) (Id B) (hrefl f) (hrefl g) $==
Id (ab_coeq f g)
  snapply ab_coeq_ind_homotopy.
A, B: AbGroup
f, g: A $-> B
functor_ab_coeq (Id A) (Id B) (hrefl f) (hrefl g) $o
ab_coeq_in $== Id (ab_coeq f g) $o ab_coeq_in
  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'.
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.
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'
  snapply cate_adjointify.
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'
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
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
?f $o ?g $== Id (ab_coeq f' g')
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
?g $o ?f $== Id (ab_coeq f g)
  -
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' exact (functor_ab_coeq a b p q).
  -
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 exact (functor_ab_coeq a^-1$ b^-1$ (hinverse a _ p) (hinverse a _ q)).
  -
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
functor_ab_coeq a b p q $o
functor_ab_coeq a^-1$ b^-1$ p ^h$ q ^h$ $==
Id (ab_coeq f' g') nrefine (functor_ab_coeq_compose _ _ _ _ _ _ _ _
      $@ functor2_ab_coeq _ _ _ _ _ $@ functor_ab_coeq_id _ _).
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
b $o b^-1$ $== Id B'
    exact (cate_isretr b).
  -
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
functor_ab_coeq a^-1$ b^-1$ p ^h$ q ^h$ $o
functor_ab_coeq a b p q $== Id (ab_coeq f g) nrefine (functor_ab_coeq_compose _ _ _ _ _ _ _ _
      $@ functor2_ab_coeq _ _ _ _ _ $@ functor_ab_coeq_id _ _).
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
b^-1$ $o b $== Id B
    exact (cate_issect b).
Defined.

(** ** The bifunctor [ab_hom] *)

Instance is0functor_ab_hom01 `{Funext} {A : Group^op}
  : Is0Functor (ab_hom A).
H: Funext
A: Group^op
Is0Functor (ab_hom A)
Proof.
H: Funext
A: Group^op
Is0Functor (ab_hom A)
  snapply (Build_Is0Functor _ AbGroup); intros B B' f.
H: Funext
A: Group^op
B, B': AbGroup
f: B $-> B'
ab_hom A B $-> ab_hom A B'
  snapply Build_GroupHomomorphism.
H: Funext
A: Group^op
B, B': AbGroup
f: B $-> B'
ab_hom A B -> ab_hom A B'
H: Funext
A: Group^op
B, B': AbGroup
f: B $-> B'
IsSemiGroupPreserving ?grp_homo_map
  1: exact (fun g => grp_homo_compose f g).
H: Funext
A: Group^op
B, B': AbGroup
f: B $-> B'
IsSemiGroupPreserving
  (fun g : ab_hom A B => grp_homo_compose f g)
  intros phi psi.
H: Funext
A: Group^op
B, B': AbGroup
f: B $-> B'
phi, psi: ab_hom A B
grp_homo_compose f (phi + psi) =
grp_homo_compose f phi + grp_homo_compose f psi
  apply equiv_path_grouphomomorphism; intro a; cbn.
H: Funext
A: Group^op
B, B': AbGroup
f: B $-> B'
phi, psi: ab_hom A B
a: A
f (phi a + psi a) = f (phi a) + f (psi a)
  exact (grp_homo_op f _ _).
Defined.

Instance is0functor_ab_hom10 `{Funext} {B : AbGroup@{u}}
  : Is0Functor (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B).
H: Funext
B: AbGroup
Is0Functor
  (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B)
Proof.
H: Funext
B: AbGroup
Is0Functor
  (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B)
  snapply (Build_Is0Functor (Group^op) AbGroup); intros A A' f.
H: Funext
B: AbGroup
A, A': Group^op
f: A $-> A'
flip (ab_hom : Group^op -> AbGroup -> AbGroup) B A $->
flip (ab_hom : Group^op -> AbGroup -> AbGroup) B A'
  snapply Build_GroupHomomorphism.
H: Funext
B: AbGroup
A, A': Group^op
f: A $-> A'
flip (ab_hom : Group^op -> AbGroup -> AbGroup) B A ->
flip (ab_hom : Group^op -> AbGroup -> AbGroup) B A'
H: Funext
B: AbGroup
A, A': Group^op
f: A $-> A'
IsSemiGroupPreserving ?grp_homo_map
  1: exact (fun g => grp_homo_compose g f).
H: Funext
B: AbGroup
A, A': Group^op
f: A $-> A'
IsSemiGroupPreserving
  (fun
     g : flip
           (ab_hom : Group^op -> AbGroup -> AbGroup) B
           A => grp_homo_compose g f)
  intros phi psi.
H: Funext
B: AbGroup
A, A': Group^op
f: A $-> A'
phi, psi: flip ab_hom B A
grp_homo_compose (phi + psi) f =
grp_homo_compose phi f + grp_homo_compose psi f
  by apply equiv_path_grouphomomorphism.
Defined.

Instance is1functor_ab_hom01 `{Funext} {A : Group^op}
  : Is1Functor (ab_hom A).
H: Funext
A: Group^op
Is1Functor (ab_hom A)
Proof.
H: Funext
A: Group^op
Is1Functor (ab_hom A)
  napply Build_Is1Functor.
H: Funext
A: Group^op
forall (a b : AbGroup) (f g : a $-> b),
f $== g -> fmap (ab_hom A) f $== fmap (ab_hom A) g
H: Funext
A: Group^op
forall a : AbGroup,
fmap (ab_hom A) (Id a) $== Id (ab_hom A a)
H: Funext
A: Group^op
forall (a b c : AbGroup) (f : a $-> b) (g : b $-> c),
fmap (ab_hom A) (g $o f) $==
fmap (ab_hom A) g $o fmap (ab_hom A) f
  -
H: Funext
A: Group^op
forall (a b : AbGroup) (f g : a $-> b),
f $== g -> fmap (ab_hom A) f $== fmap (ab_hom A) g intros B B' f g p phi.
H: Funext
A: Group^op
B, B': AbGroup
f, g: B $-> B'
p: f $== g
phi: ab_hom A B
fmap (ab_hom A) f phi = fmap (ab_hom A) g phi
    apply equiv_path_grouphomomorphism; intro a; cbn.
H: Funext
A: Group^op
B, B': AbGroup
f, g: B $-> B'
p: f $== g
phi: ab_hom A B
a: A
f (phi a) = g (phi a)
    exact (p (phi a)).
  -
H: Funext
A: Group^op
forall a : AbGroup,
fmap (ab_hom A) (Id a) $== Id (ab_hom A a) intros B phi.
H: Funext
A: Group^op
B: AbGroup
phi: ab_hom A B
fmap (ab_hom A) (Id B) phi = Id (ab_hom A B) phi
    by apply equiv_path_grouphomomorphism.
  -
H: Funext
A: Group^op
forall (a b c : AbGroup) (f : a $-> b) (g : b $-> c),
fmap (ab_hom A) (g $o f) $==
fmap (ab_hom A) g $o fmap (ab_hom A) f intros B C D f g phi.
H: Funext
A: Group^op
B, C, D: AbGroup
f: B $-> C
g: C $-> D
phi: ab_hom A B
fmap (ab_hom A) (g $o f) phi =
(fmap (ab_hom A) g $o fmap (ab_hom A) f) phi
    by apply equiv_path_grouphomomorphism.
Defined.

Instance is1functor_ab_hom10 `{Funext} {B : AbGroup@{u}}
  : Is1Functor (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B).
H: Funext
B: AbGroup
Is1Functor
  (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B)
Proof.
H: Funext
B: AbGroup
Is1Functor
  (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B)
  napply Build_Is1Functor.
H: Funext
B: AbGroup
forall (a b : Group^op) (f g : a $-> b),
f $== g ->
fmap
  (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B) f $==
fmap
  (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B) g
H: Funext
B: AbGroup
forall a : Group^op,
fmap
  (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B)
  (Id a) $== Id (flip ab_hom B a)
H: Funext
B: AbGroup
forall (a b c : Group^op) (f : a $-> b) (g : b $-> c),
fmap
  (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B)
  (g $o f) $==
fmap
  (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B) g $o
fmap
  (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B) f
  -
H: Funext
B: AbGroup
forall (a b : Group^op) (f g : a $-> b),
f $== g ->
fmap
  (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B) f $==
fmap
  (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B) g intros A A' f g p phi.
H: Funext
B: AbGroup
A, A': Group^op
f, g: A $-> A'
p: f $== g
phi: flip ab_hom B A
fmap
  (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B) f
  phi =
fmap
  (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B) g
  phi
    apply equiv_path_grouphomomorphism; intro a; cbn.
H: Funext
B: AbGroup
A, A': Group^op
f, g: A $-> A'
p: f $== g
phi: flip ab_hom B A
a: A'
phi (f a) = phi (g a)
    exact (ap phi (p a)).
  -
H: Funext
B: AbGroup
forall a : Group^op,
fmap
  (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B)
  (Id a) $== Id (flip ab_hom B a) intros A phi.
H: Funext
B: AbGroup
A: Group^op
phi: flip ab_hom B A
fmap
  (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B)
  (Id A) phi = Id (flip ab_hom B A) phi
    by apply equiv_path_grouphomomorphism.
  -
H: Funext
B: AbGroup
forall (a b c : Group^op) (f : a $-> b) (g : b $-> c),
fmap
  (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B)
  (g $o f) $==
fmap
  (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B) g $o
fmap
  (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B) f intros A C D f g phi.
H: Funext
B: AbGroup
A, C, D: Group^op
f: A $-> C
g: C $-> D
phi: flip ab_hom B A
fmap
  (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B)
  (g $o f) phi =
(fmap
   (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B)
   g $o
 fmap
   (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B)
   f) phi
    by apply equiv_path_grouphomomorphism.
Defined.

Instance is0bifunctor_ab_hom `{Funext}
  : Is0Bifunctor (ab_hom : Group^op -> AbGroup -> AbGroup)
  := Build_Is0Bifunctor'' _.

Instance is1bifunctor_ab_hom `{Funext}
  : Is1Bifunctor (ab_hom : Group^op -> AbGroup -> AbGroup).
H: Funext
Is1Bifunctor (ab_hom : Group^op -> AbGroup -> AbGroup)
Proof.
H: Funext
Is1Bifunctor (ab_hom : Group^op -> AbGroup -> AbGroup)
  napply Build_Is1Bifunctor''.
H: Funext
forall a : Group^op, Is1Functor (ab_hom a)
H: Funext
forall b : AbGroup, Is1Functor (flip ab_hom b)
H: Funext
forall (a0 a1 : Group^op) (f : a0 $-> a1)
(b0 b1 : AbGroup) (g : b0 $-> b1),
fmap01 ab_hom a1 g $o fmap10 ab_hom f b0 $==
fmap10 ab_hom f b1 $o fmap01 ab_hom a0 g
  1,2: exact _.
H: Funext
forall (a0 a1 : Group^op) (f : a0 $-> a1)
(b0 b1 : AbGroup) (g : b0 $-> b1),
fmap01 ab_hom a1 g $o fmap10 ab_hom f b0 $==
fmap10 ab_hom f b1 $o fmap01 ab_hom a0 g
  intros A A' f B B' g phi; cbn.
H: Funext
A, A': Group^op
f: A $-> A'
B, B': AbGroup
g: B $-> B'
phi: ab_hom A B
grp_homo_compose g (grp_homo_compose phi f) =
grp_homo_compose (grp_homo_compose g phi) f
  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).
H: Funext
A, B, C: AbGroup
f: A $-> B
IsSurjection0: IsConnMap (Tr (-1)) f
IsEmbedding (fmap10 ab_hom f C)
Proof.
H: Funext
A, B, C: AbGroup
f: A $-> B
IsSurjection0: IsConnMap (Tr (-1)) f
IsEmbedding (fmap10 ab_hom f C)
  apply isembedding_isinj_hset; intros g0 g1 p.
H: Funext
A, B, C: AbGroup
f: A $-> B
IsSurjection0: IsConnMap (Tr (-1)) f
g0, g1: ab_hom B C
p: fmap10 ab_hom f C g0 = fmap10 ab_hom f C g1
g0 = g1
  apply equiv_path_grouphomomorphism.
H: Funext
A, B, C: AbGroup
f: A $-> B
IsSurjection0: IsConnMap (Tr (-1)) f
g0, g1: ab_hom B C
p: fmap10 ab_hom f C g0 = fmap10 ab_hom f C g1
g0 == g1
  rapply (conn_map_elim (Tr (-1)) f).
H: Funext
A, B, C: AbGroup
f: A $-> B
IsSurjection0: IsConnMap (Tr (-1)) f
g0, g1: ab_hom B C
p: fmap10 ab_hom f C g0 = fmap10 ab_hom f C g1
forall a : A, g0 (f a) = g1 (f a)
  exact (equiv_path_grouphomomorphism^-1 p).
Defined.