From HoTT Require Import Basics Types.From HoTT Require Import Basics Types.
From HoTT.WildCat Require Import Core Opposite Bifunctor AbEnriched.
Require Import HSet Truncations.Core Modalities.ReflectiveSubuniverse.
Require Import Groups.Group 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.

(** ** 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; 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; 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.

(** ** [AbGroup] has a wild enrichment in wild abelian groups *)

(** Using arguments very similar to the above, but without using [Funext], we can show that [AbGroup] is enriched in the wild sense.  We could use this combined with [Funext] to deduce the results above, but we wouldn't get the extra generality where the domain group does not need to be abelian.  And conversely we don't want to use the above results here, since we don't need to rely on [Funext]. *)

Instance abenriched_abgroup : IsAbEnriched AbGroup.
IsAbEnriched AbGroup
Proof.
IsAbEnriched AbGroup
  snapply Build_IsAbEnriched.
forall a b : AbGroup, IsAbGroup_0gpd (a $-> b)
forall (a b c : AbGroup) (g : b $-> c), IsGroupHom_0gpd (cat_postcomp a g)
forall (a b c : AbGroup) (f : a $-> b), IsGroupHom_0gpd (cat_precomp c f)
  -
forall a b : AbGroup, IsAbGroup_0gpd (a $-> b) intros A B.
A, B: AbGroup
IsAbGroup_0gpd (A $-> B)
    snapply (Build_IsAbGroup_0gpd _ _ _ _ sgop_hom grp_homo_const inverse_hom).
A, B: AbGroup
Is0Bifunctor sgop_hom
A, B: AbGroup
Is0Functor inverse_hom
A, B: AbGroup
forall a b c : A $-> B, a + b + c $== a + (b + c)
A, B: AbGroup
forall a : A $-> B, 0 + a $== a
A, B: AbGroup
forall a : A $-> B, a + 0 $== a
A, B: AbGroup
forall a : A $-> B, - a + a $== 0
A, B: AbGroup
forall a : A $-> B, a - a $== 0
A, B: AbGroup
forall a b : A $-> B, a + b $== b + a
    3-8: hnf; intros; intro; cbn.
A, B: AbGroup
Is0Bifunctor sgop_hom
A, B: AbGroup
Is0Functor inverse_hom
A, B: AbGroup
a, b, c: A $-> B
x: A
a x + b x + c x = a x + (b x + c x)
A, B: AbGroup
a: A $-> B
x: A
group_unit + a x = a x
A, B: AbGroup
a: A $-> B
x: A
a x + group_unit = a x
A, B: AbGroup
a: A $-> B
x: A
- a x + a x = group_unit
A, B: AbGroup
a: A $-> B
x: A
a x - a x = group_unit
A, B: AbGroup
a, b: A $-> B
x: A
a x + b x = b x + a x
    +
A, B: AbGroup
Is0Bifunctor sgop_hom srapply Build_Is0Bifunctor'.
A, B: AbGroup
Is0Functor (uncurry sgop_hom)
      snapply Build_Is0Functor.
A, B: AbGroup
forall a b : (A $-> B) * (A $-> B),
(a $-> b) -> uncurry sgop_hom a $-> uncurry sgop_hom b
      intros [f f'] [g g'] [p p'] a; cbn in *.
A, B: AbGroup
f, f', g, g': GroupHomomorphism A B
p: f == g
p': f' == g'
a: A
f a + f' a = g a + g' a
      exact (ap011 _ (p a) (p' a)).
    +
A, B: AbGroup
Is0Functor inverse_hom snapply Build_Is0Functor.
A, B: AbGroup
forall a b : A $-> B, (a $-> b) -> inverse_hom a $-> inverse_hom b
      intros f g p a; cbn.
A, B: AbGroup
f, g: A $-> B
p: f $-> g
a: A
- f a = - g a
      apply (ap _ (p a)).
    +
A, B: AbGroup
a, b, c: A $-> B
x: A
a x + b x + c x = a x + (b x + c x) symmetry; apply associativity.
    +
A, B: AbGroup
a: A $-> B
x: A
group_unit + a x = a x apply left_identity.
    +
A, B: AbGroup
a: A $-> B
x: A
a x + group_unit = a x apply right_identity.
    +
A, B: AbGroup
a: A $-> B
x: A
- a x + a x = group_unit apply left_inverse.
    +
A, B: AbGroup
a: A $-> B
x: A
a x - a x = group_unit apply right_inverse.
    +
A, B: AbGroup
a, b: A $-> B
x: A
a x + b x = b x + a x apply commutativity.
  -
forall (a b c : AbGroup) (g : b $-> c), IsGroupHom_0gpd (cat_postcomp a g) intros A B C g f f' a; cbn.
A, B, C: AbGroup
g: B $-> C
f, f': A $-> B
a: A
g (f a + f' a) = g (f a) + g (f' a)
    apply grp_homo_op.
  -
forall (a b c : AbGroup) (f : a $-> b), IsGroupHom_0gpd (cat_precomp c f) intros A B C f g g' a; cbn.
A, B, C: AbGroup
f: A $-> B
g, g': B $-> C
a: A
g (f a) + g' (f a) = g (f a) + g' (f a) reflexivity.
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.