AbHom.v

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 AbelianGroup Biproduct.

(** * Homomorphisms from a group to an abelian group form an abelian group. *)

(** We can add group homomorphisms. *)
Definition ab_homo_add {A : Group} {B : AbGroup} (f g : A $-> B)
  : A $-> B.A: Group
B: AbGroup
f, g: A $-> B
A $-> B
Proof.A: Group
B: AbGroup
f, g: A $-> B
A $-> B
  refine (grp_homo_compose ab_codiagonal _).A: Group
B: AbGroup
f, g: A $-> B
GroupHomomorphism A (ab_biprod B B)
  (** [fun a => f(a) + g(a)] **)
  exact (grp_prod_corec f g).
Defined.

(** We can negate a group homomorphism by composing with [ab_homo_negation]. *)
Global Instance negate_hom {A : Group} {B : AbGroup}
  : Negate (@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
  nrefine (Build_Group (GroupHomomorphism A B)
             ab_homo_add grp_homo_const negate_hom _).H: Funext
A: Group
B: AbGroup
IsGroup (GroupHomomorphism A B)
  repeat split.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 mon_unit
H: Funext
A: Group
B: AbGroup
RightIdentity sg_op mon_unit
H: Funext
A: Group
B: AbGroup
LeftInverse sg_op negate mon_unit
H: Funext
A: Group
B: AbGroup
RightInverse sg_op negate mon_unit
  1: exact _.H: Funext
A: Group
B: AbGroup
Associative sg_op
H: Funext
A: Group
B: AbGroup
LeftIdentity sg_op mon_unit
H: Funext
A: Group
B: AbGroup
RightIdentity sg_op mon_unit
H: Funext
A: Group
B: AbGroup
LeftInverse sg_op negate mon_unit
H: Funext
A: Group
B: AbGroup
RightInverse sg_op negate mon_unit
  all: hnf; intros; apply equiv_path_grouphomomorphism; intro; cbn.H: Funext
A: Group
B: AbGroup
x, y, z: GroupHomomorphism A B
x0: A
sg_op (x x0) (sg_op (y x0) (z x0)) =
sg_op (sg_op (x x0) (y x0)) (z x0)
H: Funext
A: Group
B: AbGroup
y: GroupHomomorphism A B
x: A
sg_op group_unit (y x) = y x
H: Funext
A: Group
B: AbGroup
x: GroupHomomorphism A B
x0: A
sg_op (x x0) group_unit = x x0
H: Funext
A: Group
B: AbGroup
x: GroupHomomorphism A B
x0: A
sg_op (negate (x x0)) (x x0) = group_unit
H: Funext
A: Group
B: AbGroup
x: GroupHomomorphism A B
x0: A
sg_op (x x0) (negate (x x0)) = group_unit
  +H: Funext
A: Group
B: AbGroup
x, y, z: GroupHomomorphism A B
x0: A
sg_op (x x0) (sg_op (y x0) (z x0)) =
sg_op (sg_op (x x0) (y x0)) (z x0) apply associativity.
  +H: Funext
A: Group
B: AbGroup
y: GroupHomomorphism A B
x: A
sg_op group_unit (y x) = y x apply left_identity.
  +H: Funext
A: Group
B: AbGroup
x: GroupHomomorphism A B
x0: A
sg_op (x x0) group_unit = x x0 apply right_identity.
  +H: Funext
A: Group
B: AbGroup
x: GroupHomomorphism A B
x0: A
sg_op (negate (x x0)) (x x0) = group_unit apply left_inverse.
  +H: Funext
A: Group
B: AbGroup
x: GroupHomomorphism A B
x0: A
sg_op (x x0) (negate (x x0)) = group_unit apply right_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
  snrapply (Build_AbGroup (grp_hom A B)).H: Funext
A: Group
B: AbGroup
Commutative group_sgop
  intros f g; cbn.H: Funext
A: Group
B: AbGroup
f, g: grp_hom A B
ab_homo_add f g = ab_homo_add g f
  apply equiv_path_grouphomomorphism; intro x; cbn.H: Funext
A: Group
B: AbGroup
f, g: grp_hom A B
x: A
sg_op (f x) (g x) = sg_op (g x) (f x)
  apply commutativity.
Defined.

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

Global 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)
  snrapply (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'
  snrapply 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 ?f
  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 (sg_op phi psi) =
sg_op (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 (sg_op (phi a) (psi a)) =
sg_op (f (phi a)) (f (psi a))
  exact (grp_homo_op f _ _).
Defined.

Global 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)
  snrapply (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'
  snrapply 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 ?f
  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 (sg_op phi psi) f =
sg_op (grp_homo_compose phi f)
  (grp_homo_compose psi f)
  by apply equiv_path_grouphomomorphism.
Defined.

Global 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)
  nrapply 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.

Global 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)
  nrapply 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.

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

Global 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)
  nrapply 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. *)
Global 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.