Library HoTT.Algebra.AbGroups.Biproduct
Require Import Basics Types Truncations.Core.
Require Import WildCat.
Require Import HSet.
Require Import AbelianGroup.
Require Import Modalities.ReflectiveSubuniverse.
Local Open Scope mc_add_scope.
Require Import WildCat.
Require Import HSet.
Require Import AbelianGroup.
Require Import Modalities.ReflectiveSubuniverse.
Local Open Scope mc_add_scope.
Definition ab_biprod@{u} (A B : AbGroup@{u}) : AbGroup@{u}.
Proof.
rapply (Build_AbGroup (grp_prod A B)).
intros [a b] [a' b'].
apply path_prod; simpl; apply commutativity.
Defined.
These inherit IsEmbedding instances from their grp_prod versions.
Definition ab_biprod_inl {A B : AbGroup} : A $-> ab_biprod A B := grp_prod_inl.
Definition ab_biprod_inr {A B : AbGroup} : B $-> ab_biprod A B := grp_prod_inr.
Definition ab_biprod_inr {A B : AbGroup} : B $-> ab_biprod A B := grp_prod_inr.
These inherit IsSurjection instances from their grp_prod versions.
Definition ab_biprod_pr1 {A B : AbGroup} : ab_biprod A B $-> A := grp_prod_pr1.
Definition ab_biprod_pr2 {A B : AbGroup} : ab_biprod A B $-> B := grp_prod_pr2.
Definition ab_biprod_ind {A B : AbGroup}
(P : ab_biprod A B → Type)
(Hinl : ∀ a, P (ab_biprod_inl a))
(Hinr : ∀ b, P (ab_biprod_inr b))
(Hop : ∀ x y, P x → P y → P (x + y))
: ∀ x, P x.
Proof.
intros [a b].
snrapply ((grp_prod_decompose a b)^ # _).
apply Hop.
- exact (Hinl a).
- exact (Hinr b).
Defined.
Definition ab_biprod_ind_homotopy {A B C : AbGroup}
{f g : ab_biprod A B $-> C}
(Hinl : f $o ab_biprod_inl $== g $o ab_biprod_inl)
(Hinr : f $o ab_biprod_inr $== g $o ab_biprod_inr)
: f $== g.
Proof.
rapply ab_biprod_ind.
- exact Hinl.
- exact Hinr.
- intros x y p q.
lhs nrapply grp_homo_op.
rhs nrapply grp_homo_op.
f_ap.
Defined.
(* Maps out of biproducts are determined on the two inclusions. *)
Definition equiv_ab_biprod_ind_homotopy `{Funext} {A B X : AbGroup} (phi psi : ab_biprod A B $-> X)
: (phi $o ab_biprod_inl == psi $o ab_biprod_inl)
× (phi $o ab_biprod_inr == psi $o ab_biprod_inr)
<~> phi == psi.
Proof.
apply equiv_iff_hprop.
- exact (uncurry ab_biprod_ind_homotopy).
- exact (fun h ⇒ (fun a ⇒ h _, fun b ⇒ h _)).
Defined.
Definition ab_biprod_pr2 {A B : AbGroup} : ab_biprod A B $-> B := grp_prod_pr2.
Definition ab_biprod_ind {A B : AbGroup}
(P : ab_biprod A B → Type)
(Hinl : ∀ a, P (ab_biprod_inl a))
(Hinr : ∀ b, P (ab_biprod_inr b))
(Hop : ∀ x y, P x → P y → P (x + y))
: ∀ x, P x.
Proof.
intros [a b].
snrapply ((grp_prod_decompose a b)^ # _).
apply Hop.
- exact (Hinl a).
- exact (Hinr b).
Defined.
Definition ab_biprod_ind_homotopy {A B C : AbGroup}
{f g : ab_biprod A B $-> C}
(Hinl : f $o ab_biprod_inl $== g $o ab_biprod_inl)
(Hinr : f $o ab_biprod_inr $== g $o ab_biprod_inr)
: f $== g.
Proof.
rapply ab_biprod_ind.
- exact Hinl.
- exact Hinr.
- intros x y p q.
lhs nrapply grp_homo_op.
rhs nrapply grp_homo_op.
f_ap.
Defined.
(* Maps out of biproducts are determined on the two inclusions. *)
Definition equiv_ab_biprod_ind_homotopy `{Funext} {A B X : AbGroup} (phi psi : ab_biprod A B $-> X)
: (phi $o ab_biprod_inl == psi $o ab_biprod_inl)
× (phi $o ab_biprod_inr == psi $o ab_biprod_inr)
<~> phi == psi.
Proof.
apply equiv_iff_hprop.
- exact (uncurry ab_biprod_ind_homotopy).
- exact (fun h ⇒ (fun a ⇒ h _, fun b ⇒ h _)).
Defined.
Recursion principle
Proposition ab_biprod_rec {A B Y : AbGroup}
(f : A $-> Y) (g : B $-> Y)
: (ab_biprod A B) $-> Y.
Proof.
snrapply Build_GroupHomomorphism.
- intros [a b]; exact (f a + g b).
- intros [a b] [a' b']; simpl.
rewrite (grp_homo_op f).
rewrite (grp_homo_op g).
rewrite (associativity _ (g b) _).
rewrite <- (associativity _ (f a') _).
rewrite (commutativity (f a') _).
rewrite (associativity _ (g b) _).
exact (associativity _ (f a') _)^.
Defined.
Corollary ab_biprod_rec_uncurried {A B Y : AbGroup}
: (A $-> Y) × (B $-> Y)
→ (ab_biprod A B) $-> Y.
Proof.
intros [f g]. exact (ab_biprod_rec f g).
Defined.
Proposition ab_biprod_rec_eta {A B Y : AbGroup}
(u : ab_biprod A B $-> Y)
: ab_biprod_rec (u $o ab_biprod_inl) (u $o ab_biprod_inr) == u.
Proof.
intros [a b]; simpl.
refine ((grp_homo_op u _ _)^ @ ap u _).
apply path_prod.
- exact (right_identity a).
- exact (left_identity b).
Defined.
Proposition ab_biprod_rec_beta_inl {A B Y : AbGroup}
(a : A $-> Y) (b : B $-> Y)
: (ab_biprod_rec a b) $o ab_biprod_inl == a.
Proof.
intro x; simpl.
rewrite (grp_homo_unit b).
exact (right_identity (a x)).
Defined.
Proposition ab_biprod_rec_beta_inr {A B Y : AbGroup}
(a : A $-> Y) (b : B $-> Y)
: (ab_biprod_rec a b) $o ab_biprod_inr == b.
Proof.
intro y; simpl.
rewrite (grp_homo_unit a).
exact (left_identity (b y)).
Defined.
Theorem isequiv_ab_biprod_rec `{Funext} {A B Y : AbGroup}
: IsEquiv (@ab_biprod_rec_uncurried A B Y).
Proof.
srapply isequiv_adjointify.
- intro phi.
exact (phi $o ab_biprod_inl, phi $o ab_biprod_inr).
- intro phi.
apply equiv_path_grouphomomorphism.
exact (ab_biprod_rec_eta phi).
- intros [a b].
apply path_prod.
+ apply equiv_path_grouphomomorphism.
apply ab_biprod_rec_beta_inl.
+ apply equiv_path_grouphomomorphism.
apply ab_biprod_rec_beta_inr.
Defined.
(f : A $-> Y) (g : B $-> Y)
: (ab_biprod A B) $-> Y.
Proof.
snrapply Build_GroupHomomorphism.
- intros [a b]; exact (f a + g b).
- intros [a b] [a' b']; simpl.
rewrite (grp_homo_op f).
rewrite (grp_homo_op g).
rewrite (associativity _ (g b) _).
rewrite <- (associativity _ (f a') _).
rewrite (commutativity (f a') _).
rewrite (associativity _ (g b) _).
exact (associativity _ (f a') _)^.
Defined.
Corollary ab_biprod_rec_uncurried {A B Y : AbGroup}
: (A $-> Y) × (B $-> Y)
→ (ab_biprod A B) $-> Y.
Proof.
intros [f g]. exact (ab_biprod_rec f g).
Defined.
Proposition ab_biprod_rec_eta {A B Y : AbGroup}
(u : ab_biprod A B $-> Y)
: ab_biprod_rec (u $o ab_biprod_inl) (u $o ab_biprod_inr) == u.
Proof.
intros [a b]; simpl.
refine ((grp_homo_op u _ _)^ @ ap u _).
apply path_prod.
- exact (right_identity a).
- exact (left_identity b).
Defined.
Proposition ab_biprod_rec_beta_inl {A B Y : AbGroup}
(a : A $-> Y) (b : B $-> Y)
: (ab_biprod_rec a b) $o ab_biprod_inl == a.
Proof.
intro x; simpl.
rewrite (grp_homo_unit b).
exact (right_identity (a x)).
Defined.
Proposition ab_biprod_rec_beta_inr {A B Y : AbGroup}
(a : A $-> Y) (b : B $-> Y)
: (ab_biprod_rec a b) $o ab_biprod_inr == b.
Proof.
intro y; simpl.
rewrite (grp_homo_unit a).
exact (left_identity (b y)).
Defined.
Theorem isequiv_ab_biprod_rec `{Funext} {A B Y : AbGroup}
: IsEquiv (@ab_biprod_rec_uncurried A B Y).
Proof.
srapply isequiv_adjointify.
- intro phi.
exact (phi $o ab_biprod_inl, phi $o ab_biprod_inr).
- intro phi.
apply equiv_path_grouphomomorphism.
exact (ab_biprod_rec_eta phi).
- intros [a b].
apply path_prod.
+ apply equiv_path_grouphomomorphism.
apply ab_biprod_rec_beta_inl.
+ apply equiv_path_grouphomomorphism.
apply ab_biprod_rec_beta_inr.
Defined.
Corecursion principle, inherited from Groups/Group.v.
Definition ab_biprod_corec {A B X : AbGroup} (f : X $-> A) (g : X $-> B)
: X $-> ab_biprod A B
:= grp_prod_corec f g.
: X $-> ab_biprod A B
:= grp_prod_corec f g.
Functoriality of ab_biprod
Definition functor_ab_biprod {A A' B B' : AbGroup} (f : A $-> A') (g: B $-> B')
: ab_biprod A B $-> ab_biprod A' B'
:= (ab_biprod_corec (f $o ab_biprod_pr1) (g $o ab_biprod_pr2)).
Definition ab_biprod_functor_beta {Z X Y A B : AbGroup} (f0 : Z $-> X) (f1 : Z $-> Y)
(g0 : X $-> A) (g1 : Y $-> B)
: functor_ab_biprod g0 g1 $o ab_biprod_corec f0 f1
$== ab_biprod_corec (g0 $o f0) (g1 $o f1)
:= fun _ ⇒ idpath.
Global Instance is0bifunctor_ab_biprod : Is0Bifunctor ab_biprod.
Proof.
srapply Build_Is0Bifunctor'.
snrapply Build_Is0Functor.
intros [A B] [A' B'] [f g].
exact (functor_ab_biprod f g).
Defined.
Global Instance is1bifunctor_ab_biprod : Is1Bifunctor ab_biprod.
Proof.
snrapply Build_Is1Bifunctor'.
snrapply Build_Is1Functor.
- intros [A B] [A' B'] [f g] [f' g'] [p q] [a b].
snrapply equiv_path_prod.
exact (p a, q b).
- reflexivity.
- cbn; reflexivity.
Defined.
Definition isequiv_functor_ab_biprod {A A' B B' : AbGroup}
(f : A $-> A') (g : B $-> B') `{IsEquiv _ _ f} `{IsEquiv _ _ g}
: IsEquiv (functor_ab_biprod f g).
Proof.
srapply isequiv_adjointify.
1: { rapply functor_ab_biprod;
apply grp_iso_inverse.
+ exact (Build_GroupIsomorphism _ _ f _).
+ exact (Build_GroupIsomorphism _ _ g _). }
all: intros [a b]; simpl.
all: apply path_prod'.
1,2: apply eisretr.
all: apply eissect.
Defined.
Definition equiv_functor_ab_biprod {A A' B B' : AbGroup}
(f : A $-> A') (g : B $-> B') `{IsEquiv _ _ f} `{IsEquiv _ _ g}
: GroupIsomorphism (ab_biprod A B) (ab_biprod A' B')
:= Build_GroupIsomorphism _ _ _ (isequiv_functor_ab_biprod f g).
Biproducts preserve embeddings.
Definition functor_ab_biprod_embedding {A A' B B' : AbGroup}
(i : A $-> B) (i' : A' $-> B')
`{IsEmbedding i} `{IsEmbedding i'}
: IsEmbedding (functor_ab_biprod i i').
Proof.
intros [b b'].
apply hprop_allpath.
intros [[a0 a0'] p] [[a1 a1'] p']; cbn in p, p'.
rapply path_sigma_hprop; cbn.
pose (q := (equiv_path_prod _ _)^-1 p); cbn in q.
pose (q' := (equiv_path_prod _ _)^-1 p'); cbn in q'.
destruct q as [q0 q1], q' as [q0' q1'].
apply path_prod; rapply isinj_embedding; cbn.
- exact (q0 @ q0'^).
- exact (q1 @ q1'^).
Defined.
(i : A $-> B) (i' : A' $-> B')
`{IsEmbedding i} `{IsEmbedding i'}
: IsEmbedding (functor_ab_biprod i i').
Proof.
intros [b b'].
apply hprop_allpath.
intros [[a0 a0'] p] [[a1 a1'] p']; cbn in p, p'.
rapply path_sigma_hprop; cbn.
pose (q := (equiv_path_prod _ _)^-1 p); cbn in q.
pose (q' := (equiv_path_prod _ _)^-1 p'); cbn in q'.
destruct q as [q0 q1], q' as [q0' q1'].
apply path_prod; rapply isinj_embedding; cbn.
- exact (q0 @ q0'^).
- exact (q1 @ q1'^).
Defined.
Products preserve surjections.
Definition functor_ab_biprod_surjection `{Funext} {A A' B B' : AbGroup}
(p : A $-> B) (p' : A' $-> B')
`{S : IsSurjection p} `{S' : IsSurjection p'}
: IsSurjection (functor_ab_biprod p p').
Proof.
intros [b b'].
pose proof (a := S b); pose proof (a' := S' b').
apply center in a, a'.
strip_truncations.
rapply contr_inhabited_hprop.
apply tr.
∃ (ab_biprod_inl a.1 + ab_biprod_inr a'.1); cbn.
apply path_prod;
refine (grp_homo_op _ _ _ @ _);
rewrite (grp_homo_unit _);
cbn.
- exact (right_identity _ @ a.2).
- exact (left_identity _ @ a'.2).
Defined.
(p : A $-> B) (p' : A' $-> B')
`{S : IsSurjection p} `{S' : IsSurjection p'}
: IsSurjection (functor_ab_biprod p p').
Proof.
intros [b b'].
pose proof (a := S b); pose proof (a' := S' b').
apply center in a, a'.
strip_truncations.
rapply contr_inhabited_hprop.
apply tr.
∃ (ab_biprod_inl a.1 + ab_biprod_inr a'.1); cbn.
apply path_prod;
refine (grp_homo_op _ _ _ @ _);
rewrite (grp_homo_unit _);
cbn.
- exact (right_identity _ @ a.2).
- exact (left_identity _ @ a'.2).
Defined.
Definition direct_sum_swap {A B : AbGroup}
: ab_biprod A B $<~> ab_biprod B A.
Proof.
snrapply Build_GroupIsomorphism'.
- apply equiv_prod_symm.
- intro; reflexivity.
Defined.
: ab_biprod A B $<~> ab_biprod B A.
Proof.
snrapply Build_GroupIsomorphism'.
- apply equiv_prod_symm.
- intro; reflexivity.
Defined.
Definition ab_codiagonal {A : AbGroup} : ab_biprod A A $-> A
:= ab_biprod_rec grp_homo_id grp_homo_id.
Definition ab_codiagonal_natural {A B : AbGroup} (f : A $-> B)
: f $o ab_codiagonal $== ab_codiagonal $o functor_ab_biprod f f
:= fun a ⇒ grp_homo_op f _ _.
Definition ab_diagonal {A : AbGroup} : A $-> ab_biprod A A
:= ab_biprod_corec grp_homo_id grp_homo_id.
:= ab_biprod_rec grp_homo_id grp_homo_id.
Definition ab_codiagonal_natural {A B : AbGroup} (f : A $-> B)
: f $o ab_codiagonal $== ab_codiagonal $o functor_ab_biprod f f
:= fun a ⇒ grp_homo_op f _ _.
Definition ab_diagonal {A : AbGroup} : A $-> ab_biprod A A
:= ab_biprod_corec grp_homo_id grp_homo_id.
Given two abelian group homomorphisms f and g, their pairing (f, g) : B → A + A can be written as a composite. Note that ab_biprod_corec is an alias for grp_prod_corec.
Lemma ab_biprod_corec_diagonal `{Funext} {A B : AbGroup} (f g : B $-> A)
: ab_biprod_corec f g = (functor_ab_biprod f g) $o ab_diagonal.
Proof.
apply equiv_path_grouphomomorphism; reflexivity.
Defined.
: ab_biprod_corec f g = (functor_ab_biprod f g) $o ab_diagonal.
Proof.
apply equiv_path_grouphomomorphism; reflexivity.
Defined.
Precomposing the codiagonal with the swap map has no effect.
Lemma ab_codiagonal_swap `{Funext} {A : AbGroup}
: (@ab_codiagonal A) $o direct_sum_swap = ab_codiagonal.
Proof.
apply equiv_path_grouphomomorphism.
intro a; cbn.
exact (abgroup_commutative _ _ _).
Defined.
: (@ab_codiagonal A) $o direct_sum_swap = ab_codiagonal.
Proof.
apply equiv_path_grouphomomorphism.
intro a; cbn.
exact (abgroup_commutative _ _ _).
Defined.
The corresponding result for the diagonal is true definitionally, so it isn't strictly necessary to state it, but we record it anyways.
Definition ab_diagonal_swap {A : AbGroup}
: direct_sum_swap $o (@ab_diagonal A) = ab_diagonal
:= idpath.
: direct_sum_swap $o (@ab_diagonal A) = ab_diagonal
:= idpath.
The biproduct is associative.
Lemma ab_biprod_assoc {A B C : AbGroup}
: ab_biprod A (ab_biprod B C) $<~> ab_biprod (ab_biprod A B) C.
Proof.
snrapply Build_GroupIsomorphism'.
- apply equiv_prod_assoc.
- unfold IsSemiGroupPreserving; reflexivity.
Defined.
: ab_biprod A (ab_biprod B C) $<~> ab_biprod (ab_biprod A B) C.
Proof.
snrapply Build_GroupIsomorphism'.
- apply equiv_prod_assoc.
- unfold IsSemiGroupPreserving; reflexivity.
Defined.
The iterated diagonals (ab_diagonal + id) o ab_diagonal and (id + ab_diagonal) o ab_diagonal agree, after reassociating the direct sum.
Definition ab_commute_id_diagonal {A : AbGroup}
: (functor_ab_biprod (@ab_diagonal A) grp_homo_id) $o ab_diagonal
= ab_biprod_assoc $o (functor_ab_biprod grp_homo_id ab_diagonal) $o ab_diagonal
:= idpath.
: (functor_ab_biprod (@ab_diagonal A) grp_homo_id) $o ab_diagonal
= ab_biprod_assoc $o (functor_ab_biprod grp_homo_id ab_diagonal) $o ab_diagonal
:= idpath.
A similar result for the codiagonal.
Lemma ab_commute_id_codiagonal `{Funext} {A : AbGroup}
: (@ab_codiagonal A) $o (functor_ab_biprod ab_codiagonal grp_homo_id) $o ab_biprod_assoc
= ab_codiagonal $o (functor_ab_biprod grp_homo_id ab_codiagonal).
Proof.
apply equiv_path_grouphomomorphism.
intro a; cbn.
exact (grp_assoc _ _ _)^.
Defined.
: (@ab_codiagonal A) $o (functor_ab_biprod ab_codiagonal grp_homo_id) $o ab_biprod_assoc
= ab_codiagonal $o (functor_ab_biprod grp_homo_id ab_codiagonal).
Proof.
apply equiv_path_grouphomomorphism.
intro a; cbn.
exact (grp_assoc _ _ _)^.
Defined.
The next few results are used to prove associativity of the Baer sum.
A "twist" isomorphism (A + B) + C <~> (C + B) + A.
Lemma ab_biprod_twist {A B C : AbGroup@{u}}
: ab_biprod (ab_biprod A B) C $<~> ab_biprod (ab_biprod C B) A.
Proof.
snrapply Build_GroupIsomorphism.
- snrapply Build_GroupHomomorphism.
+ intros [[a b] c].
exact ((c,b),a).
+ unfold IsSemiGroupPreserving. reflexivity.
- snrapply isequiv_adjointify.
+ intros [[c b] a].
exact ((a,b),c).
+ reflexivity.
+ reflexivity.
Defined.
: ab_biprod (ab_biprod A B) C $<~> ab_biprod (ab_biprod C B) A.
Proof.
snrapply Build_GroupIsomorphism.
- snrapply Build_GroupHomomorphism.
+ intros [[a b] c].
exact ((c,b),a).
+ unfold IsSemiGroupPreserving. reflexivity.
- snrapply isequiv_adjointify.
+ intros [[c b] a].
exact ((a,b),c).
+ reflexivity.
+ reflexivity.
Defined.
The triagonal and cotriagonal homomorphisms.
Definition ab_triagonal {A : AbGroup} : A $-> ab_biprod (ab_biprod A A) A
:= (functor_ab_biprod ab_diagonal grp_homo_id) $o ab_diagonal.
Definition ab_cotriagonal {A : AbGroup} : ab_biprod (ab_biprod A A) A $-> A
:= ab_codiagonal $o (functor_ab_biprod ab_codiagonal grp_homo_id).
:= (functor_ab_biprod ab_diagonal grp_homo_id) $o ab_diagonal.
Definition ab_cotriagonal {A : AbGroup} : ab_biprod (ab_biprod A A) A $-> A
:= ab_codiagonal $o (functor_ab_biprod ab_codiagonal grp_homo_id).
Definition ab_triagonal_twist {A : AbGroup}
: ab_biprod_twist $o @ab_triagonal A = ab_triagonal
:= idpath.
: ab_biprod_twist $o @ab_triagonal A = ab_triagonal
:= idpath.
A similar result for the cotriagonal.
Definition ab_cotriagonal_twist `{Funext} {A : AbGroup}
: @ab_cotriagonal A $o ab_biprod_twist = ab_cotriagonal.
Proof.
apply equiv_path_grouphomomorphism.
intro x. cbn.
refine ((grp_assoc _ _ _)^ @ _).
refine (abgroup_commutative _ _ _ @ _).
exact (ap (fun a ⇒ a + snd x) (abgroup_commutative _ _ _)).
Defined.
: @ab_cotriagonal A $o ab_biprod_twist = ab_cotriagonal.
Proof.
apply equiv_path_grouphomomorphism.
intro x. cbn.
refine ((grp_assoc _ _ _)^ @ _).
refine (abgroup_commutative _ _ _ @ _).
exact (ap (fun a ⇒ a + snd x) (abgroup_commutative _ _ _)).
Defined.