Merge pull request #2079 from Alizter/ps/rr/tensor_product_distribute…

…s_over_direct_sum

tensor product distributes over direct sum

theories/Algebra/AbGroups/Biproduct.v

@@ -23,6 +23,46 @@ Definition ab_biprod_inr {A B : AbGroup} : B $-> ab_biprod A B := grp_prod_inr.
 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 : forall a, P (ab_biprod_inl a))
+  (Hinr : forall b, P (ab_biprod_inr b))
+  (Hop : forall x y, P x -> P y -> P (x + y))
+  : forall 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)
@@ -58,7 +98,7 @@ Proof.
   - exact (left_identity b).
 Defined.
 
-Proposition ab_biprod_rec_inl_beta {A B Y : AbGroup}
+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.
@@ -67,7 +107,7 @@ Proof.
   exact (right_identity (a x)).
 Defined.
 
-Proposition ab_biprod_rec_inr_beta {A B Y : AbGroup}
+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.
@@ -88,9 +128,9 @@ Proof.
   - intros [a b].
     apply path_prod.
     + apply equiv_path_grouphomomorphism.
-      apply ab_biprod_rec_inl_beta.
+      apply ab_biprod_rec_beta_inl.
     + apply equiv_path_grouphomomorphism.
-      apply ab_biprod_rec_inr_beta.
+      apply ab_biprod_rec_beta_inr.
 Defined.
 
 (** Corecursion principle, inherited from Groups/Group.v. *)
@@ -114,6 +154,25 @@ Definition ab_biprod_functor_beta {Z X Y A B : AbGroup} (f0 : Z $-> X) (f1 : Z $
                       $== 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).
@@ -175,37 +234,6 @@ Defined.
 
 (** *** Lemmas for working with biproducts *)
 
-Lemma ab_biprod_decompose {B A : AbGroup} (a : A) (b : B)
-  : (a, b) = ((a, group_unit) : ab_biprod A B) + (group_unit, b).
-Proof.
-  apply path_prod; cbn.
-  - exact (right_identity _)^.
-  - exact (left_identity _)^.
-Defined.
-
-Lemma ab_biprod_corec_eta' {A B X : AbGroup} (f g : ab_biprod A B $-> X)
-  : (f $o ab_biprod_inl $== g $o ab_biprod_inl)
-  -> (f $o ab_biprod_inr $== g $o ab_biprod_inr)
-  -> f $== g.
-Proof.
-  intros h k.
-  intros [a b].
-  refine (ap f (ab_biprod_decompose _ _) @ _ @ ap g (ab_biprod_decompose _ _)^).
-  exact (grp_homo_op_agree f g (h a) (k b)).
-Defined.
-
-(* Maps out of biproducts are determined on the two inclusions. *)
-Lemma equiv_path_biprod_corec `{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.
-  - intros [h k].
-    apply ab_biprod_corec_eta'; assumption.
-  - intro h.
-    exact (fun a => h _, fun b => h _).
-Defined.
-
 (** The swap isomorphism of the biproduct of two groups. *)
 Definition direct_sum_swap {A B : AbGroup}
   : ab_biprod A B $<~> ab_biprod B A.

theories/Algebra/AbGroups/TensorProduct.v

@@ -1,5 +1,5 @@
 Require Import Basics.Overture Basics.Tactics.
-Require Import Types.Forall Types.Sigma.
+Require Import Types.Forall Types.Sigma Types.Prod.
 Require Import WildCat.Core WildCat.Equiv WildCat.Monoidal WildCat.Bifunctor.
 Require Import WildCat.NatTrans.
 Require Import Algebra.Groups.Group Algebra.Groups.QuotientGroup.
@@ -807,4 +807,52 @@ Proof.
     reflexivity.
 Defined.
 
+(** ** Tensor products distribute over direct sums *)
+
+Definition ab_tensor_prod_dist_l {A B C : AbGroup}
+  : ab_tensor_prod A (ab_biprod B C)
+    $<~> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C).
+Proof.
+  srapply (let f := _ in let g := _ in cate_adjointify f g _ _).
+  - snrapply ab_tensor_prod_rec.
+    + intros a bc.
+      exact (tensor a (fst bc), tensor a (snd bc)).
+    + intros a bc bc'; cbn beta.
+      snrapply path_prod'; snrapply tensor_dist_l.
+    + intros a a' bc; cbn beta.
+      snrapply path_prod; snrapply tensor_dist_r.
+  - snrapply ab_biprod_rec.
+    + exact (fmap01 ab_tensor_prod A ab_biprod_inl).
+    + exact (fmap01 ab_tensor_prod A ab_biprod_inr).
+  - snrapply ab_biprod_ind_homotopy.
+    + refine (cat_assoc _ _ _ $@ (_ $@L _) $@ _). 
+      1: snrapply ab_biprod_rec_beta_inl.
+      snrapply ab_tensor_prod_ind_homotopy.
+      intros a b.
+      snrapply path_prod; simpl.
+      * reflexivity.
+      * snrapply tensor_zero_r.
+    + refine (cat_assoc _ _ _ $@ (_ $@L _) $@ _).
+      1: snrapply ab_biprod_rec_beta_inr.
+      snrapply ab_tensor_prod_ind_homotopy.
+      intros a b.
+      snrapply path_prod; simpl.
+      * snrapply tensor_zero_r.
+      * reflexivity.
+  - snrapply ab_tensor_prod_ind_homotopy.
+    intros a [b c].
+    lhs_V nrapply tensor_dist_l; simpl.
+    snrapply ap.
+    symmetry; apply grp_prod_decompose.
+Defined.
+
+Definition ab_tensor_prod_dist_r {A B C : AbGroup}
+  : ab_tensor_prod (ab_biprod A B) C
+    $<~> ab_biprod (ab_tensor_prod A C) (ab_tensor_prod B C).
+Proof.
+  refine (emap11 ab_biprod (braide _ _) (braide _ _)
+    $oE _ $oE braide _ _).
+  snrapply ab_tensor_prod_dist_l.
+Defined.
+
 (** TODO: Show that the category of abelian groups is symmetric closed and therefore we have adjoint pair with the tensor and internal hom. This should allow us to prove lemmas such as tensors distributing over coproducts. *)

theories/Algebra/AbSES/Core.v

@@ -471,11 +471,11 @@ Proof.
     apply path_sigma_hprop; cbn.
     rapply equiv_path_grouphomomorphism; intros [a b]; cbn.
     apply path_prod; cbn.
-    + rewrite (ab_biprod_decompose a b).
+    + rewrite (grp_prod_decompose a b).
       refine (_ @ (grp_homo_op (ab_biprod_pr1 $o phi) _ _)^).
       apply grp_cancelR; symmetry.
       exact (ap fst (p a)).
-    + rewrite (ab_biprod_decompose a b).
+    + rewrite (grp_prod_decompose a b).
       refine (_ @ (grp_homo_op (ab_biprod_pr2 $o phi) _ _)^); cbn; symmetry.
       exact (ap011 _ (ap snd (p a)) (q (group_unit, b))^).
 Defined.

theories/Algebra/AbSES/PullbackFiberSequence.v

@@ -266,7 +266,7 @@ Proof.
   refine (cat_assoc _ _ _ $@ _).
   apply gpd_moveR_Vh.
   apply gpd_moveL_hM.
-  apply equiv_path_biprod_corec.
+  apply equiv_ab_biprod_ind_homotopy.
   split; apply equiv_path_pullback_rec_hset; split; cbn.
   - intro a.
     exact (ap (class_of _ o pullback_pr1) (fst p^$.2 a)).

theories/Algebra/Groups/Group.v

@@ -907,6 +907,15 @@ Proof.
   intros ? ?; reflexivity.
 Defined.
 
+(** Pairs in direct products can be decomposed *)
+Definition grp_prod_decompose {G H : Group} (g : G) (h : H)
+  : (g, h) = ((g, group_unit) : grp_prod G H) * (group_unit, h).
+Proof.
+  snrapply path_prod; symmetry.
+  - snrapply grp_unit_r.
+  - snrapply grp_unit_l.
+Defined.
+
 (** The second projection is a surjection. *)
 Global Instance issurj_grp_prod_pr2 {G H : Group}
   : IsSurjection (@grp_prod_pr2 G H)