From 3c6ad573c72c1950125ee8e2b8b3ff336cfcfe43 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 8 Jul 2024 16:20:48 +0200 Subject: [PATCH 01/44] grp_pow_commutes Signed-off-by: Ali Caglayan --- theories/Algebra/Groups/Group.v | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v index 39eca032333..90d7d037e5c 100644 --- a/theories/Algebra/Groups/Group.v +++ b/theories/Algebra/Groups/Group.v @@ -535,6 +535,35 @@ Proof. - reflexivity. Defined. +(** [grp_pow g n] commutes with [h] if [g] commutes with [h]. *) +Definition grp_pow_commutes {G : Group} (n : Int) (g h : G) + (p : g * h = h * g) + : (grp_pow g n) * h = h * (grp_pow g n). +Proof. + induction n. + - exact (grp_unit_l _ @ (grp_unit_r _)^). + - rewrite grp_pow_succ. + rewrite <- simple_associativity. + rewrite IHn. + rewrite 2 simple_associativity. + f_ap. + - rewrite grp_pow_pred. + rewrite <- simple_associativity. + rewrite IHn. + rewrite 2 simple_associativity. + f_ap. + apply grp_moveL_gV. + rewrite <- simple_associativity. + by apply grp_moveR_Vg. +Defined. + +(** [grp_pow g n] commutes with [g]. *) +Definition grp_pow_commutes' {G : Group} (n : Int) (g : G) + : grp_pow g n * g = g * grp_pow g n. +Proof. + by apply grp_pow_commutes. +Defined. + (** ** The category of Groups *) (** ** Groups together with homomorphisms form a 1-category whose equivalences are the group isomorphisms. *) From d58355b1e13a4115965286380fc30de779b6db8a Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Tue, 9 Jul 2024 14:12:29 +0200 Subject: [PATCH 02/44] tensor products of abelian groups Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/AbelianGroup.v | 6 + theories/Algebra/AbGroups/Abelianization.v | 13 + theories/Algebra/AbGroups/FreeAbelianGroup.v | 4 + theories/Algebra/AbGroups/TensorProduct.v | 672 +++++++++++++++++++ theories/Algebra/AbGroups/Z.v | 39 ++ theories/Algebra/Groups/FreeGroup.v | 32 + theories/Algebra/Groups/QuotientGroup.v | 1 - 7 files changed, 766 insertions(+), 1 deletion(-) create mode 100644 theories/Algebra/AbGroups/TensorProduct.v diff --git a/theories/Algebra/AbGroups/AbelianGroup.v b/theories/Algebra/AbGroups/AbelianGroup.v index 7c9a818bbed..3b9cc0bd8e8 100644 --- a/theories/Algebra/AbGroups/AbelianGroup.v +++ b/theories/Algebra/AbGroups/AbelianGroup.v @@ -100,6 +100,12 @@ Defined. Definition QuotientAbGroup (G : AbGroup) (H : Subgroup G) : AbGroup := (Build_AbGroup (QuotientGroup' G H (isnormal_ab_subgroup G H)) _). +Definition quotient_abgroup_map (G : AbGroup) (H : Subgroup G) + : GroupHomomorphism G (QuotientAbGroup G H). +Proof. + snrapply grp_quotient_map. +Defined. + Definition quotient_abgroup_rec {G : AbGroup} (N : Subgroup G) (H : AbGroup) (f : GroupHomomorphism G H) (h : forall n : G, N n -> f n = mon_unit) diff --git a/theories/Algebra/AbGroups/Abelianization.v b/theories/Algebra/AbGroups/Abelianization.v index 55fe3b10441..4446e0d5b72 100644 --- a/theories/Algebra/AbGroups/Abelianization.v +++ b/theories/Algebra/AbGroups/Abelianization.v @@ -275,6 +275,19 @@ Section AbelGroup. Proof. by unfold IsSemiGroupPreserving. Defined. + + Global Instance ismonoidpreserving_ab : IsMonoidPreserving ab. + Proof. + split. + 1: exact _. + reflexivity. + Defined. + + (** [ab] preserves negation *) + Definition ab_negate x : ab (-x) = - ab x. + Proof. + exact (preserves_negate (f:=ab) x). + Defined. End AbelGroup. diff --git a/theories/Algebra/AbGroups/FreeAbelianGroup.v b/theories/Algebra/AbGroups/FreeAbelianGroup.v index 0c897818627..76267f0d2a7 100644 --- a/theories/Algebra/AbGroups/FreeAbelianGroup.v +++ b/theories/Algebra/AbGroups/FreeAbelianGroup.v @@ -3,6 +3,7 @@ Require Import Types.Sigma Types.Forall Types.Paths. Require Import WildCat.Core WildCat.EquivGpd. Require Import Algebra.AbGroups.AbelianGroup Algebra.AbGroups.Abelianization. Require Import Algebra.Groups.FreeGroup. +Require Import Spaces.List.Core. (** * Free Abelian Groups *) @@ -29,6 +30,9 @@ Global Instance isfreeabgroup_isfreeabgroupon (S : Type) (F_S : AbGroup) (i : S Definition FreeAbGroup (S : Type) : AbGroup := abel (FreeGroup S). +Definition freeabgroup_in {S : Type} : S -> FreeAbGroup S + := abel_unit _ o freegroup_in. + (** The abelianization of a free group on a set is a free abelian group on that set. *) Global Instance isfreeabgroupon_isabelianization_isfreegroup `{Funext} {S : Type} {G : Group} {A : AbGroup} (f : S -> G) (g : G $-> A) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v new file mode 100644 index 00000000000..a611cfea3de --- /dev/null +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -0,0 +1,672 @@ +Require Import Basics.Overture Basics.Tactics. +Require Import Types.Forall. +Require Import WildCat.Core WildCat.Equiv WildCat.Monoidal WildCat.Bifunctor. +Require Import WildCat.NatTrans. +Require Import Algebra.Groups.Group Algebra.Groups.QuotientGroup. +Require Import Algebra.AbGroups.AbelianGroup Algebra.AbGroups.Biproduct. +Require Import Algebra.AbGroups.AbHom Algebra.AbGroups.FreeAbelianGroup. +Require Import Algebra.AbGroups.Abelianization Algebra Algebra.Groups.FreeGroup. +Require Import Colimits.Quotient. +Require Import Spaces.List.Core. +Require Import Truncations. + +Local Open Scope mc_scope. +Local Open Scope mc_add_scope. + +(** * Tensor Product of Abelian Groups *) + +(** ** Construction *) + +(** We define the tensor product of abelian groups as a quotient of the free abelian group on pairs of elements of the two groups by the subgroup generated by the bilinear pairs. *) + +(** Here we define the subgroup of bilinear pairs *) +Definition subgroup_bilinear_pairs {A B : AbGroup} + : Subgroup (FreeAbGroup (A * B)). +Proof. + snrapply subgroup_generated. + intros x. + refine ((exists (a1 a2 : A) (b : B), _) + exists (a : A) (b1 b2 : B), _)%type. + - refine (_ - _ - _ = x). + 1-3: apply freeabgroup_in. + + exact (a1 + a2, b). + + exact (a1, b). + + exact (a2, b). + - refine (_ - _ - _ = x). + 1-3: apply freeabgroup_in. + + exact (a, b1 + b2). + + exact (a, b1). + + exact (a, b2). +Defined. + +Definition ab_tensor_prod (A B : AbGroup) : AbGroup + := QuotientAbGroup (FreeAbGroup (A * B)) subgroup_bilinear_pairs. + +Definition tensor {A B : AbGroup} : A -> B -> ab_tensor_prod A B + := fun a b => grp_quotient_map (freeabgroup_in (a, b)). + +Definition tensor_dist_l {A B : AbGroup} (a : A) (b b' : B) + : tensor a (b + b') = tensor a b + tensor a b'. +Proof. + apply qglue, tr. + rewrite <- grp_inv_inv. + apply sgt_inv. + rewrite 2 grp_inv_op. + rewrite grp_inv_inv. + rewrite (commutativity (- _)). + rewrite commutativity. + rewrite simple_associativity. + apply sgt_in. + right. + by exists a, b, b'. +Defined. + +Definition tensor_dist_r {A B : AbGroup} (a a' : A) (b : B) + : tensor (a + a') b = tensor a b + tensor a' b. +Proof. + apply qglue, tr. + rewrite <- grp_inv_inv. + apply sgt_inv. + rewrite 2 grp_inv_op. + rewrite grp_inv_inv. + rewrite (commutativity (- _)). + rewrite commutativity. + rewrite simple_associativity. + apply sgt_in. + left. + by exists a, a', b. +Defined. + +Definition grp_homo_tensor_l {A B : AbGroup} (b : B) + : A $-> ab_tensor_prod A B. +Proof. + snrapply Build_GroupHomomorphism. + - exact (fun a => tensor a b). + - intros a a'. + nrapply tensor_dist_r. +Defined. + +Definition grp_homo_tensor_r {A B : AbGroup} (a : A) + : B $-> ab_tensor_prod A B. +Proof. + snrapply Build_GroupHomomorphism. + - exact (fun b => tensor a b). + - intros b b'. + nrapply tensor_dist_l. +Defined. + +Definition tensor_neg_l {A B : AbGroup} (a : A) (b : B) + : tensor (-a) b = - tensor a b. +Proof. + change (grp_homo_tensor_l b (-a) = - tensor a b). + by rewrite grp_homo_inv. +Defined. + +Definition tensor_neg_r {A B : AbGroup} (a : A) (b : B) + : tensor a (-b) = - tensor a b. +Proof. + change (grp_homo_tensor_r a (-b) = - tensor a b). + by rewrite grp_homo_inv. +Defined. + +Definition tensor_zero_l {A B : AbGroup} (b : B) + : tensor (A:=A) 0 b = 0. +Proof. + change (grp_homo_tensor_l (A:=A) b 0 = 0). + nrapply grp_homo_unit. +Defined. + +Definition tensor_zero_r {A B : AbGroup} (a : A) + : tensor (B:=B) a 0 = 0. +Proof. + change (grp_homo_tensor_r (B:=B) a 0 = 0). + nrapply grp_homo_unit. +Defined. + +Definition tensor_zero {A B : AbGroup} + : @tensor A B 0 0 = 0. +Proof. + apply tensor_zero_l. +Defined. + +Definition grp_homo_tensor `{Funext} {A B : AbGroup} + : A $-> ab_hom B (ab_tensor_prod A B). +Proof. + snrapply Build_GroupHomomorphism. + - intros a. + snrapply Build_GroupHomomorphism. + + exact (tensor a). + + nrapply tensor_dist_l. + - intros a a'. + apply equiv_path_grouphomomorphism. + intros b. + nrapply tensor_dist_r. +Defined. + +Definition ab_tensor_prod_rec {A B C : AbGroup} + (f : A * B -> C) + (l : forall a b b', f (a, b + b') = f (a, b) + f (a, b')) + (r : forall a a' b, f (a + a', b) = f (a, b) + f (a', b)) + : ab_tensor_prod A B $-> C. +Proof. + unfold ab_tensor_prod. + snrapply grp_quotient_rec. + - snrapply grp_homo_abel_rec. + snrapply FreeGroup_rec. + exact f. + - intros x H. + strip_truncations. + induction H as + [ x [ [ a [ a' [ b p ] ] ] | [ a [ b [ b' p ] ] ] ] + | + | ? ? ? H1 ? H2 ]. + + destruct p. + rewrite 2 grp_homo_op. + rewrite 2 grp_homo_inv. + apply grp_moveL_1M^-1%equiv. + apply grp_moveL_gM^-1%equiv. + unfold freeabgroup_in. + change (grp_homo_abel_rec ?f (abel_unit ?G ?x)) with (f x). + simpl. + rewrite 3 grp_unit_r. + rhs rapply abgroup_commutative. + apply r. + + destruct p. + rewrite 2 grp_homo_op. + rewrite 2 grp_homo_inv. + apply grp_moveL_1M^-1%equiv. + apply grp_moveL_gM^-1%equiv. + unfold freeabgroup_in. + change (grp_homo_abel_rec ?f (abel_unit ?G ?x)) with (f x). + simpl. + rewrite 3 grp_unit_r. + rhs rapply abgroup_commutative. + apply l. + + nrapply grp_homo_unit. + + rewrite grp_homo_op, grp_homo_inv. + apply grp_moveL_1M^-1. + exact(H1 @ H2^). +Defined. + +Definition ab_tensor_prod_rec_beta_tensor {A B C : AbGroup} + (f : A * B -> C) + (l : forall a b b', f (a, b + b') = f (a, b) + f (a, b')) + (r : forall a a' b, f (a + a', b) = f (a, b) + f (a', b)) + (a : A) (b : B) + : ab_tensor_prod_rec f l r (tensor a b) = f (a, b). +Proof. + change (f (a, b) + mon_unit = f (a, b)). + apply grp_unit_r. +Defined. + +Definition ab_tensor_prod_ind_hprop {A B : AbGroup} + (P : ab_tensor_prod A B -> Type) + {H : forall x, IsHProp (P x)} + (H1 : P 0) + (H2 : forall a b, P (tensor a b)) + (H3 : forall x, P x -> P (-x)) + (H4 : forall x y, P x -> P y -> P (x + y)) + : forall x, P x. +Proof. + unfold ab_tensor_prod. + srapply Quotient_ind_hprop. + srapply Abel_ind_hprop. + srapply FreeGroup_ind_hprop. + - exact H1. + - intros [a b]. + apply H2. + - cbn beta. + intros w H5. + rewrite ab_negate. + change (P (quotient_abgroup_map _ subgroup_bilinear_pairs (- ab w))). + rewrite grp_homo_inv. + apply H3. + exact H5. + - cbn beta. + intros x y Hx Hy. + change (P (quotient_abgroup_map _ subgroup_bilinear_pairs (ab (x + y)))). + rewrite issemigrouppreserving_ab. + rewrite grp_homo_op. + by apply H4. +Defined. + +Definition ab_tensor_prod_ind_homotopy {A B G : AbGroup} + {f f' : ab_tensor_prod A B $-> G} + (H : forall a b, f (tensor a b) = f' (tensor a b)) + : f $== f'. +Proof. + rapply (ab_tensor_prod_ind_hprop (fun _ => _)). + - by rewrite 2 grp_homo_unit. + - exact H. + - intros x p. + rewrite 2 grp_homo_inv. + exact (ap (-) p). + - intros x y p q. + rewrite 2 grp_homo_op. + exact (ap011 (+) p q). +Defined. + +Definition ab_tensor_prod_ind_homotopy_plus {A B G : AbGroup} + {f f' f'' : ab_tensor_prod A B $-> G} + (H : forall a b, f (tensor a b) = f' (tensor a b) + f'' (tensor a b)) + : forall x, f x = f' x + f'' x + := ab_tensor_prod_ind_homotopy (f':=ab_homo_add f' f'') H. + +Definition ab_tensor_prod_ind_hprop_triple {A B C : AbGroup} + (P : ab_tensor_prod A (ab_tensor_prod B C) -> Type) + (H : forall x, IsHProp (P x)) + (H1 : P 0) + (H2 : forall a b c, P (tensor a (tensor b c))) + (H3 : forall x, P x -> P (-x)) + (H4 : forall x y, P x -> P y -> P (x + y)) + : forall x, P x. +Proof. + rapply (ab_tensor_prod_ind_hprop P H1). + - intros a. + rapply (ab_tensor_prod_ind_hprop (fun x => P (tensor _ x))). + + rewrite tensor_zero_r. + exact H1. + + nrapply H2. + + intros x Hx. + rewrite tensor_neg_r. + by apply H3. + + intros x y Hx Hy. + rewrite tensor_dist_l. + by apply H4. + - exact H3. + - exact H4. +Defined. + +Definition ab_tensor_prod_ind_homotopy_triple {A B C G : AbGroup} + {f f' : ab_tensor_prod A (ab_tensor_prod B C) $-> G} + (H : forall a b c, f (tensor a (tensor b c)) = f' (tensor a (tensor b c))) + : f $== f'. +Proof. + rapply (ab_tensor_prod_ind_hprop_triple (fun _ => _)). + - by rewrite 2 grp_homo_unit. + - exact H. + - intros x p. + rewrite 2 grp_homo_inv. + exact (ap (-) p). + - intros x y p q. + rewrite 2 grp_homo_op. + exact (ap011 (+) p q). +Defined. + +Definition ab_tensor_prod_ind_hprop_quad {A B C D : AbGroup} + (P : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) -> Type) + (H : forall x, IsHProp (P x)) + (H1 : P 0) + (H2 : forall a b c d, P (tensor a (tensor b (tensor c d)))) + (H3 : forall x, P x -> P (-x)) + (H4 : forall x y, P x -> P y -> P (x + y)) + : forall x, P x. +Proof. + rapply (ab_tensor_prod_ind_hprop P H1). + - intros a. + rapply (ab_tensor_prod_ind_hprop_triple (fun x => P (tensor _ x))). + + rewrite tensor_zero_r. + exact H1. + + nrapply H2. + + intros x Hx. + rewrite tensor_neg_r. + by apply H3. + + intros x y Hx Hy. + rewrite tensor_dist_l. + by apply H4. + - exact H3. + - exact H4. +Defined. + +Definition ab_tensor_prod_ind_homotopy_quad {A B C D G : AbGroup} + {f f' : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) $-> G} + (H : forall a b c d, f (tensor a (tensor b (tensor c d))) + = f' (tensor a (tensor b (tensor c d)))) + : f $== f'. +Proof. + rapply (ab_tensor_prod_ind_hprop_quad (fun _ => _)). + - by rewrite 2 grp_homo_unit. + - exact H. + - intros x p. + rewrite 2 grp_homo_inv. + exact (ap (-) p). + - intros x y p q. + rewrite 2 grp_homo_op. + exact (ap011 (+) p q). +Defined. + +Definition functor_ab_tensor_prod {A B A' B' : AbGroup} + (f : A $-> A') (g : B $-> B') + : ab_tensor_prod A B $-> ab_tensor_prod A' B'. +Proof. + snrapply ab_tensor_prod_rec. + - intros [a b]. + exact (tensor (f a) (g b)). + - intros a b b'; hnf. + rewrite grp_homo_op. + by rewrite tensor_dist_l. + - intros a a' b; hnf. + rewrite grp_homo_op. + by rewrite tensor_dist_r. +Defined. + +Definition functor_ab_tensor_prod_beta_tensor {A B A' B' : AbGroup} + (f : A $-> A') (g : B $-> B') (a : A) (b : B) + : functor_ab_tensor_prod f g (tensor a b) = tensor (f a) (g b). +Proof. + nrapply ab_tensor_prod_rec_beta_tensor. +Defined. + +Definition functor2_ab_tensor_prod {A B A' B' : AbGroup} + {f f' : A $-> A'} (p : f $== f') {g g' : B $-> B'} (q : g $== g') + : functor_ab_tensor_prod f g $== functor_ab_tensor_prod f' g'. +Proof. + snrapply ab_tensor_prod_ind_homotopy. + intros a b. + rewrite 2 functor_ab_tensor_prod_beta_tensor. + exact (ap011 tensor (p _) (q _)). +Defined. + +Definition functor_ab_tensor_prod_id (A B : AbGroup) + : functor_ab_tensor_prod (Id A) (Id B) $== Id (ab_tensor_prod A B). +Proof. + snrapply ab_tensor_prod_ind_homotopy. + intros a b. + apply functor_ab_tensor_prod_beta_tensor. +Defined. + +Definition functor_ab_tensor_prod_compose {A B C A' B' C' : AbGroup} + (f : A $-> B) (g : B $-> C) (f' : A' $-> B') (g' : B' $-> C') + : functor_ab_tensor_prod (g $o f) (g' $o f') + $== functor_ab_tensor_prod g g' $o functor_ab_tensor_prod f f'. +Proof. + snrapply ab_tensor_prod_ind_homotopy. + intros a b; hnf. + lhs nrapply functor_ab_tensor_prod_beta_tensor. + change (tensor (g (f a)) (g' (f' b)) + = functor_ab_tensor_prod g g' (functor_ab_tensor_prod f f' (tensor a b))). + by rewrite 2 functor_ab_tensor_prod_beta_tensor. +Defined. + +Global Instance is0bifunctor_ab_tensor_prod : Is0Bifunctor ab_tensor_prod. +Proof. + rapply Build_Is0Bifunctor'. + snrapply Build_Is0Functor. + intros [A B] [A' B'] [f g]. + exact (functor_ab_tensor_prod f g). +Defined. + +Global Instance is1bifunctor_ab_tensor_prod : Is1Bifunctor ab_tensor_prod. +Proof. + rapply Build_Is1Bifunctor'. + snrapply Build_Is1Functor. + - intros AB A'B' fg f'g' [p q]. + exact (functor2_ab_tensor_prod p q). + - intros [A B]. + exact (functor_ab_tensor_prod_id A B). + - intros AA' BB' CC' [f g] [f' g']. + exact (functor_ab_tensor_prod_compose f f' g g'). +Defined. + +Definition ab_tensor_swap {A B} : ab_tensor_prod A B $-> ab_tensor_prod B A. +Proof. + snrapply ab_tensor_prod_rec. + - exact (uncurry (flip tensor)). + - intros a b b'. + apply tensor_dist_r. + - intros a a' b. + apply tensor_dist_l. +Defined. + +Definition ab_tensor_swap_beta_tensor {A B} a b + : @ab_tensor_swap A B (tensor a b) = tensor b a. +Proof. + apply ab_tensor_prod_rec_beta_tensor. +Defined. + +Definition ab_tensor_swap_swap {A B} + : ab_tensor_swap $o @ab_tensor_swap A B $== Id _. +Proof. + snrapply ab_tensor_prod_ind_homotopy. + intros a b; hnf. + change (ab_tensor_swap (ab_tensor_swap (tensor a b)) = tensor a b). + by rewrite 2 ab_tensor_swap_beta_tensor. +Defined. + +Definition ab_tensor_swap_natural {A B A' B'} (f : A $-> A') (g : B $-> B') + : ab_tensor_swap $o functor_ab_tensor_prod f g + $== functor_ab_tensor_prod g f $o ab_tensor_swap. +Proof. + snrapply ab_tensor_prod_ind_homotopy. + intros a b. + change (ab_tensor_swap (functor_ab_tensor_prod f g (tensor a b)) + = functor_ab_tensor_prod g f (ab_tensor_swap (tensor a b))). + rewrite functor_ab_tensor_prod_beta_tensor. + rewrite 2 ab_tensor_swap_beta_tensor. + by rewrite functor_ab_tensor_prod_beta_tensor. +Defined. + +Global Instance symmetricbraiding_ab_tensor_prod : SymmetricBraiding ab_tensor_prod. +Proof. + snrapply Build_SymmetricBraiding. + - snrapply Build_NatTrans. + + intro; exact ab_tensor_swap. + + snrapply Build_Is1Natural. + intros; nrapply ab_tensor_swap_natural. + - intros; nrapply ab_tensor_swap_swap. +Defined. + +Definition ab_tensor_prod_twist {A B C} + : ab_tensor_prod A (ab_tensor_prod B C) $-> ab_tensor_prod B (ab_tensor_prod A C). +Proof. + snrapply ab_tensor_prod_rec. + - apply prod_ind. + intros a. + snrapply ab_tensor_prod_rec. + + intros [b c]. + exact (tensor b (tensor a c)). + + intros b c c'; hnf. + lhs nrapply ap. + 1: nrapply tensor_dist_l. + nrapply tensor_dist_l. + + intros b b' c; hnf. + nrapply tensor_dist_r. + - intros; nrapply grp_homo_op. + - intros a a'; unfold prod_ind; hnf. + nrapply ab_tensor_prod_ind_homotopy_plus. + intros b c. + rewrite 3 ab_tensor_prod_rec_beta_tensor. + by rewrite tensor_dist_r, tensor_dist_l. +Defined. + +Definition ab_tensor_prod_twist_beta_tensor_tensor {A B C} a b c + : @ab_tensor_prod_twist A B C (tensor a (tensor b c)) = tensor b (tensor a c). +Proof. + rapply ab_tensor_swap_beta_tensor. +Defined. + +Definition ab_tensor_prod_twist_twist {A B C} + : ab_tensor_prod_twist $o @ab_tensor_prod_twist A B C $== Id _. +Proof. + snrapply ab_tensor_prod_ind_homotopy_triple. + intros a b c. + change (ab_tensor_prod_twist (ab_tensor_prod_twist (tensor a (tensor b c))) + = tensor a (tensor b c)). + by rewrite 2 ab_tensor_prod_twist_beta_tensor_tensor. +Defined. + +Definition ab_tensor_prod_twist_natural {A B C A' B' C'} + (f : A $-> A') (g : B $-> B') (h : C $-> C') + : ab_tensor_prod_twist $o fmap11 ab_tensor_prod f (fmap11 ab_tensor_prod g h) + $== fmap11 ab_tensor_prod g (fmap11 ab_tensor_prod f h) $o ab_tensor_prod_twist. +Proof. + snrapply ab_tensor_prod_ind_homotopy_triple. + intros a b c. + change (ab_tensor_prod_twist (functor_ab_tensor_prod f (functor_ab_tensor_prod g h) (tensor a (tensor b c))) + = functor_ab_tensor_prod g (functor_ab_tensor_prod f h) (ab_tensor_prod_twist (tensor a (tensor b c)))). + rewrite 2 functor_ab_tensor_prod_beta_tensor. + rewrite 2 ab_tensor_prod_twist_beta_tensor_tensor. + by rewrite 2 functor_ab_tensor_prod_beta_tensor. +Defined. + +Require Import Spaces.Int. +Require Import AbGroups.Z. + +Definition tensor_grp_pow {A B : AbGroup} (z : Int) (a : A) (b : B) + : tensor (grp_pow a z) b = tensor a (grp_pow b z). +Proof. + induction z. + - rhs nrapply tensor_zero_r. + nrapply tensor_zero_l. + - rewrite 2 grp_pow_succ. + rewrite tensor_dist_r, tensor_dist_l. + nrapply ap. + exact IHz. + - rewrite 2 grp_pow_pred. + rewrite tensor_dist_r, tensor_dist_l. + snrapply ap011. + + rhs nrapply tensor_neg_r. + apply tensor_neg_l. + + exact IHz. +Defined. + +Definition ab_tensor_prod_Z_r {A} + : ab_tensor_prod A abgroup_Z $<~> A. +Proof. + symmetry. + snrapply Build_GroupIsomorphism. + - nrapply grp_homo_tensor_l. + exact 1%int. + - snrapply isequiv_adjointify. + + snrapply ab_tensor_prod_rec. + * exact (uncurry grp_pow_homo). + * intros a z z'; cbn beta; unfold uncurry, fst, snd. + nrapply grp_homo_op. + * intros a a' z; cbn beta; unfold uncurry, fst, snd. + nrapply grp_pow_plus. + + hnf. + change (forall x : ?A, (grp_homo_map _ _ ?f) ((grp_homo_map _ _ ?g) x) = x) + with (f $o g $== Id _). + snrapply ab_tensor_prod_ind_homotopy. + intros a z. + lhs nrapply (ap (grp_homo_tensor_l _)). + 1: apply ab_tensor_prod_rec_beta_tensor. + change (tensor (B:=abgroup_Z) (grp_pow a z) 1%int = tensor a z). + lhs nrapply tensor_grp_pow. + nrapply ap. + apply abgroup_Z_grp_pow_1. + + hnf. + intros x. + lhs nrapply ab_tensor_prod_rec_beta_tensor. + apply grp_unit_r. +Defined. + +Global Instance rightunitor_ab_tensor_prod + : RightUnitor ab_tensor_prod abgroup_Z. +Proof. + snrapply Build_NatEquiv. + - intros A. + apply ab_tensor_prod_Z_r. + - snrapply Build_Is1Natural. + intros A A' f. + snrapply ab_tensor_prod_ind_homotopy. + intros a z. + rhs nrapply (ap f). + 2: nrapply ab_tensor_prod_rec_beta_tensor. + change (ab_tensor_prod_Z_r (fmap (flip ab_tensor_prod abgroup_Z) f (tensor a z)) + = f (grp_pow_homo a z)). + lhs nrapply ap. + 1: nrapply functor_ab_tensor_prod_beta_tensor. + lhs nrapply ab_tensor_prod_rec_beta_tensor. + symmetry. + apply grp_pow_natural. +Defined. + +Global Instance left_unitor_ab_tensor_prod + : LeftUnitor ab_tensor_prod abgroup_Z. +Proof. + rapply left_unitor_twist. +Defined. + +Global Instance associator_ab_tensor_prod : Associator ab_tensor_prod. +Proof. + srapply associator_twist. + - exact @ab_tensor_prod_twist. + - intros; nrapply ab_tensor_prod_twist_twist. + - intros; nrapply ab_tensor_prod_twist_natural. +Defined. + +Global Instance triangle_ab_tensor_prod + : TriangleIdentity ab_tensor_prod abgroup_Z. +Proof. + snrapply triangle_twist. + intros A B. + snrapply ab_tensor_prod_ind_homotopy_triple. + intros a b z. + change (functor_ab_tensor_prod (Id A) (rightunitor_ab_tensor_prod B) (tensor a (tensor b z)) + = ab_tensor_swap (functor_ab_tensor_prod (Id B) + (rightunitor_ab_tensor_prod A) (ab_tensor_prod_twist (tensor a (tensor b z))))). + rewrite ab_tensor_prod_twist_beta_tensor_tensor. + rewrite 2 functor_ab_tensor_prod_beta_tensor. + rewrite ab_tensor_swap_beta_tensor. + lhs nrapply ap. + 1: rapply ab_tensor_prod_rec_beta_tensor. + rhs nrapply (ap (fun x => tensor x _)). + 2: rapply ab_tensor_prod_rec_beta_tensor. + exact (tensor_grp_pow _ _ _)^. +Defined. + +Global Instance hexagon_ab_tensor_prod : HexagonIdentity ab_tensor_prod. +Proof. + snrapply hexagon_twist. + intros A B C. + snrapply ab_tensor_prod_ind_homotopy_triple. + intros b a c. + change (functor_ab_tensor_prod (Id C) ab_tensor_swap (ab_tensor_prod_twist + (functor_ab_tensor_prod (Id B) ab_tensor_swap (tensor b (tensor a c)))) + = ab_tensor_prod_twist (functor_ab_tensor_prod (Id A) ab_tensor_swap + (ab_tensor_prod_twist (tensor b (tensor a c))))). + rewrite functor_ab_tensor_prod_beta_tensor. + rewrite ab_tensor_swap_beta_tensor. + rewrite 2 ab_tensor_prod_twist_beta_tensor_tensor. + rewrite 2 functor_ab_tensor_prod_beta_tensor. + rewrite 2 ab_tensor_swap_beta_tensor. + rewrite ab_tensor_prod_twist_beta_tensor_tensor. + reflexivity. +Defined. + +Global Instance pentagon_ab_tensor_prod : PentagonIdentity ab_tensor_prod. +Proof. + snrapply pentagon_twist. + intros A B C D. + snrapply ab_tensor_prod_ind_homotopy_quad. + intros a b c d. + change ( + functor_ab_tensor_prod (Id C) ab_tensor_swap + (ab_tensor_prod_twist + (ab_tensor_swap + (ab_tensor_prod_twist + (functor_ab_tensor_prod (Id A) ab_tensor_swap + (tensor a (tensor b (tensor c d))))))) + = functor_ab_tensor_prod (Id C) ab_tensor_prod_twist + (functor_ab_tensor_prod (Id C) (functor_ab_tensor_prod (Id A) (@ab_tensor_swap B D)) + (ab_tensor_prod_twist + (functor_ab_tensor_prod (Id A) ab_tensor_prod_twist + (tensor a (tensor b (tensor c d))))))). + rewrite 2 functor_ab_tensor_prod_beta_tensor. + rewrite ab_tensor_swap_beta_tensor. + rewrite 3 ab_tensor_prod_twist_beta_tensor_tensor. + rewrite ab_tensor_swap_beta_tensor. + rewrite ab_tensor_prod_twist_beta_tensor_tensor. + rewrite 4 functor_ab_tensor_prod_beta_tensor. + rewrite 2 ab_tensor_swap_beta_tensor. + rewrite ab_tensor_prod_twist_beta_tensor_tensor. + reflexivity. +Defined. + +Global Instance ismonoidal_ab_tensor_prod + : IsMonoidal AbGroup ab_tensor_prod abgroup_Z + := {}. + +Global Instance issymmmetricmonoidal_ab_tensor_prod + : IsSymmetricMonoidal AbGroup ab_tensor_prod abgroup_Z + := {}. diff --git a/theories/Algebra/AbGroups/Z.v b/theories/Algebra/AbGroups/Z.v index d476119a3f1..e500b7e38a4 100644 --- a/theories/Algebra/AbGroups/Z.v +++ b/theories/Algebra/AbGroups/Z.v @@ -30,3 +30,42 @@ Proof. 1: exact (grp_pow g). intros m n; apply grp_pow_add. Defined. + +Local Open Scope mc_add_scope. + +(** For every abelian group [A], [grp_pow] distributes over the group operation. *) +Definition grp_pow_plus {A : AbGroup} (a a' : A) (z : Int) + : grp_pow (a + a') z = grp_pow a z + grp_pow a' z. +Proof. + induction z. + - symmetry; apply grp_unit_l. + - rewrite 3 grp_pow_succ. + rewrite <- 2 grp_assoc. + nrapply (ap (a +)). + rewrite (ab_comm (grp_pow a n)). + rewrite <- grp_assoc. + nrapply (ap (a' +)). + rhs nrapply ab_comm. + exact IHz. + - rewrite 3 grp_pow_pred. + rewrite grp_inv_op. + rewrite (ab_comm (negate a')). + rewrite <- 2 grp_assoc. + nrapply (ap (_ +)). + rewrite grp_assoc. + rewrite (ab_comm (grp_pow _ _)). + rewrite <- grp_assoc. + nrapply (ap (_ +)). + exact IHz. +Defined. + +Definition abgroup_Z_grp_pow_1 (z : Int) + : grp_pow (G:=abgroup_Z) 1%int z = z. +Proof. + induction z. + - reflexivity. + - rewrite grp_pow_succ. + f_ap. + - rewrite grp_pow_pred. + f_ap. +Defined. diff --git a/theories/Algebra/Groups/FreeGroup.v b/theories/Algebra/Groups/FreeGroup.v index e766a320695..208ca4e1c95 100644 --- a/theories/Algebra/Groups/FreeGroup.v +++ b/theories/Algebra/Groups/FreeGroup.v @@ -357,6 +357,38 @@ Section Reduction. Defined. Coercion freegroup_in : A >-> group_type. + + Definition FreeGroup_ind_hprop' (P : FreeGroup -> Type) + `{forall x, IsHProp (P x)} + (H1 : forall w, P (freegroup_eta w)) + : forall x, P x. + Proof. + rapply Trunc_ind. + snrapply Coeq_ind. + - exact H1. + - intro; apply path_ishprop. + Defined. + + Definition FreeGroup_ind_hprop (P : FreeGroup -> Type) + `{forall x, IsHProp (P x)} + (H1 : P mon_unit) + (Hin : forall x, P (freegroup_in x)) + (Hinv : forall x, P x -> P (- x)) + (Hop : forall x y, P x -> P y -> P (x * y)) + (* (H1 : forall w, P (freegroup_eta w)) *) + : forall x, P x. + Proof. + rapply FreeGroup_ind_hprop'. + intros w. + induction w as [|a w IHw]. + - exact H1. + - destruct a as [a|a]. + + change (P ((freegroup_in a) * freegroup_eta w)). + by apply Hop. + + change (P (-(freegroup_in a) * freegroup_eta w)). + apply Hop; trivial. + by apply Hinv. + Defined. End Reduction. diff --git a/theories/Algebra/Groups/QuotientGroup.v b/theories/Algebra/Groups/QuotientGroup.v index 802a6ff18d7..1e25c49df94 100644 --- a/theories/Algebra/Groups/QuotientGroup.v +++ b/theories/Algebra/Groups/QuotientGroup.v @@ -158,7 +158,6 @@ Section QuotientGroup. - intro x. refine (Quotient_ind_hprop _ _ _). intro y. revert x. - refine (Quotient_ind_hprop _ _ _). intro x; simpl. apply grp_homo_op. From 5b89691ae7f684c5b7c9838cb3a44cb4ee976421 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Wed, 10 Jul 2024 21:22:52 +0200 Subject: [PATCH 03/44] more comments and simplify some proofs Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/TensorProduct.v | 166 +++++++++++++++++----- 1 file changed, 132 insertions(+), 34 deletions(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index a611cfea3de..9d006cdee53 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -7,7 +7,8 @@ Require Import Algebra.AbGroups.AbelianGroup Algebra.AbGroups.Biproduct. Require Import Algebra.AbGroups.AbHom Algebra.AbGroups.FreeAbelianGroup. Require Import Algebra.AbGroups.Abelianization Algebra Algebra.Groups.FreeGroup. Require Import Colimits.Quotient. -Require Import Spaces.List.Core. +Require Import Spaces.List.Core Spaces.Int. +Require Import AbGroups.Z. Require Import Truncations. Local Open Scope mc_scope. @@ -38,12 +39,19 @@ Proof. + exact (a, b2). Defined. +(** The tesnor product [ab_tensor_prod A B] of two abelian groups [A] and [B] is defined to ba a quotient of the free abelian group on pairs of elements [A * B] by the subgroup of bilinear pairs. *) Definition ab_tensor_prod (A B : AbGroup) : AbGroup := QuotientAbGroup (FreeAbGroup (A * B)) subgroup_bilinear_pairs. +(** The tensor product of [A] and [B] contains formal combinations of pairs of elements from [A] and [B]. We denote these pairs as elementary tensors and name them [tensor]. *) Definition tensor {A B : AbGroup} : A -> B -> ab_tensor_prod A B := fun a b => grp_quotient_map (freeabgroup_in (a, b)). +(** ** Properties of tensors *) + +(** The characterizing property of elementary tensors are that they are bilinear in their arguments. *) + +(** A [tensor] of a sum distributes over the sum on the left. *) Definition tensor_dist_l {A B : AbGroup} (a : A) (b b' : B) : tensor a (b + b') = tensor a b + tensor a b'. Proof. @@ -60,6 +68,7 @@ Proof. by exists a, b, b'. Defined. +(** A [tensor] of a sum distributes over the sum on the right. *) Definition tensor_dist_r {A B : AbGroup} (a a' : A) (b : B) : tensor (a + a') b = tensor a b + tensor a' b. Proof. @@ -76,16 +85,8 @@ Proof. by exists a, a', b. Defined. -Definition grp_homo_tensor_l {A B : AbGroup} (b : B) - : A $-> ab_tensor_prod A B. -Proof. - snrapply Build_GroupHomomorphism. - - exact (fun a => tensor a b). - - intros a a'. - nrapply tensor_dist_r. -Defined. - -Definition grp_homo_tensor_r {A B : AbGroup} (a : A) +(** Tensoring on the left is a group homomorphism. *) +Definition grp_homo_tensor_l {A B : AbGroup} (a : A) : B $-> ab_tensor_prod A B. Proof. snrapply Build_GroupHomomorphism. @@ -94,40 +95,49 @@ Proof. nrapply tensor_dist_l. Defined. +(** Tensoring on the right is a group homomorphism. *) +Definition grp_homo_tensor_r {A B : AbGroup} (b : B) + : A $-> ab_tensor_prod A B. +Proof. + snrapply Build_GroupHomomorphism. + - exact (fun a => tensor a b). + - intros a a'. + nrapply tensor_dist_r. +Defined. + +(** Tensors preserve negation in the left argument. *) Definition tensor_neg_l {A B : AbGroup} (a : A) (b : B) : tensor (-a) b = - tensor a b. Proof. - change (grp_homo_tensor_l b (-a) = - tensor a b). + change (grp_homo_tensor_r b (-a) = - tensor a b). by rewrite grp_homo_inv. Defined. +(** Tensors preserve negation in the right argument. *) Definition tensor_neg_r {A B : AbGroup} (a : A) (b : B) : tensor a (-b) = - tensor a b. Proof. - change (grp_homo_tensor_r a (-b) = - tensor a b). + change (grp_homo_tensor_l a (-b) = - tensor a b). by rewrite grp_homo_inv. Defined. +(** Tensoring by zero on the left is zero. *) Definition tensor_zero_l {A B : AbGroup} (b : B) : tensor (A:=A) 0 b = 0. Proof. - change (grp_homo_tensor_l (A:=A) b 0 = 0). + change (grp_homo_tensor_r (A:=A) b 0 = 0). nrapply grp_homo_unit. Defined. +(** Tensoring by zero on the right is zero. *) Definition tensor_zero_r {A B : AbGroup} (a : A) : tensor (B:=B) a 0 = 0. Proof. - change (grp_homo_tensor_r (B:=B) a 0 = 0). + change (grp_homo_tensor_l (B:=B) a 0 = 0). nrapply grp_homo_unit. Defined. -Definition tensor_zero {A B : AbGroup} - : @tensor A B 0 0 = 0. -Proof. - apply tensor_zero_l. -Defined. - +(** The [tensor] map is bilinear and therefore can be written in a curried form using the internal abelian group hom. *) Definition grp_homo_tensor `{Funext} {A B : AbGroup} : A $-> ab_hom B (ab_tensor_prod A B). Proof. @@ -142,6 +152,11 @@ Proof. nrapply tensor_dist_r. Defined. +(** ** Induction principles *) + +(** Here we write down some induction principles to help us prove lemmas about the tensor product. Some of these are quite specialised but are patterns that appear often in practice. *) + +(** Our main recursion principle states that in order to build a map out of the tensor product, it is sufficient to provide a map out of the direct product which is bilinear, that is, a map that preserves addition in both arguments of the product. *) Definition ab_tensor_prod_rec {A B C : AbGroup} (f : A * B -> C) (l : forall a b b', f (a, b + b') = f (a, b) + f (a, b')) @@ -187,6 +202,7 @@ Proof. exact(H1 @ H2^). Defined. +(** Since we defined [ab_tensor_prod_rec] using the recursors of the underlying type, we get an annoying artifact of [x + 0] instead of [x] when acting on elementary tensors. Typically in an argument we want our recursor to act on elementary tensors without the extra [0] and this lemma makes sure of that. *) Definition ab_tensor_prod_rec_beta_tensor {A B C : AbGroup} (f : A * B -> C) (l : forall a b b', f (a, b + b') = f (a, b) + f (a, b')) @@ -198,6 +214,11 @@ Proof. apply grp_unit_r. Defined. +(** The induction principle is a little different to the recursor. In the recursor, which is the non-dependent case of the induction principle, we were landing in an abelian group hence the codomain came equipped with the group operations which we wish to presere with the binlinearity conditions. + +The induction principle will require these bilinearity conditions, but we have to postulate the data of a "dependent group" in the codomain in order to state these properly. In general, we don't have any use for a general induction principle into a hset and so we can drop these depedent bilinearity paths. + +The hprop induction principle therefore requires that the codomain is a hprop in addition to being closed under the various group operations of the domain. Most importantly we hypothsise that we can prove a property on an elementary tensor [tensor a b]. *) Definition ab_tensor_prod_ind_hprop {A B : AbGroup} (P : ab_tensor_prod A B -> Type) {H : forall x, IsHProp (P x)} @@ -229,6 +250,7 @@ Proof. by apply H4. Defined. +(** As a commonly occuring special case of the above induction principle, we have the case when the predicate in question is showing two group homomorphisms are homotopic. In order to do this, it suffices to show it only for elementary tensors. The homotopy is closed under all the group operations so we don't need to hyptoehsise anything else. *) Definition ab_tensor_prod_ind_homotopy {A B G : AbGroup} {f f' : ab_tensor_prod A B $-> G} (H : forall a b, f (tensor a b) = f' (tensor a b)) @@ -245,12 +267,14 @@ Proof. exact (ap011 (+) p q). Defined. +(** As an even more specialised case, we occasionally have the second homomorphism being a sum of abelian group homomorphism. In those cases, it is easier to give this specialised lemma. *) Definition ab_tensor_prod_ind_homotopy_plus {A B G : AbGroup} {f f' f'' : ab_tensor_prod A B $-> G} (H : forall a b, f (tensor a b) = f' (tensor a b) + f'' (tensor a b)) : forall x, f x = f' x + f'' x := ab_tensor_prod_ind_homotopy (f':=ab_homo_add f' f'') H. +(** Here we give an induction principle for a triple tensor, a.k.a a dependent trilinear function. As before we need a "dependent group" as the codomain but we may now assume a "triple elmentary tensor" as a hypothesis. *) Definition ab_tensor_prod_ind_hprop_triple {A B C : AbGroup} (P : ab_tensor_prod A (ab_tensor_prod B C) -> Type) (H : forall x, IsHProp (P x)) @@ -276,6 +300,8 @@ Proof. - exact H4. Defined. +(** Similar to before, we specialise the triple tensor induction principle for proving homotopies of trilinear functions. *) +(* TODO: The proof is almost exactly the same as the bilinear case. Is there a way we can share the work? *) Definition ab_tensor_prod_ind_homotopy_triple {A B C G : AbGroup} {f f' : ab_tensor_prod A (ab_tensor_prod B C) $-> G} (H : forall a b c, f (tensor a (tensor b c)) = f' (tensor a (tensor b c))) @@ -292,6 +318,7 @@ Proof. exact (ap011 (+) p q). Defined. +(** As explained for the bilinear and trilinear cases, we also derive an induction principle for quadruple tensors giving us dependent quadrilinear maps. *) Definition ab_tensor_prod_ind_hprop_quad {A B C D : AbGroup} (P : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) -> Type) (H : forall x, IsHProp (P x)) @@ -317,6 +344,7 @@ Proof. - exact H4. Defined. +(** To construct a homotopy between quadrilinear maps we need only check equality for the quadruple elementary tensor. *) Definition ab_tensor_prod_ind_homotopy_quad {A B C D G : AbGroup} {f f' : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) $-> G} (H : forall a b c d, f (tensor a (tensor b (tensor c d))) @@ -334,6 +362,11 @@ Proof. exact (ap011 (+) p q). Defined. +(** ** Functoriality of the Tensor Product *) + +(** The tensor product produces a bifunctor and we will later show that it gives a symmetric monoidal structure on the category of abelian groups. *) + +(** Given a pair of maps, we can produce a homomorphism between the pairwise tensor products of the domains and codomains. *) Definition functor_ab_tensor_prod {A B A' B' : AbGroup} (f : A $-> A') (g : B $-> B') : ab_tensor_prod A B $-> ab_tensor_prod A' B'. @@ -349,6 +382,7 @@ Proof. by rewrite tensor_dist_r. Defined. +(** The tensor product functor acts on elementary tensors by mapping each component. *) Definition functor_ab_tensor_prod_beta_tensor {A B A' B' : AbGroup} (f : A $-> A') (g : B $-> B') (a : A) (b : B) : functor_ab_tensor_prod f g (tensor a b) = tensor (f a) (g b). @@ -356,6 +390,7 @@ Proof. nrapply ab_tensor_prod_rec_beta_tensor. Defined. +(** 2-functoriality of the tensor product. *) Definition functor2_ab_tensor_prod {A B A' B' : AbGroup} {f f' : A $-> A'} (p : f $== f') {g g' : B $-> B'} (q : g $== g') : functor_ab_tensor_prod f g $== functor_ab_tensor_prod f' g'. @@ -366,6 +401,7 @@ Proof. exact (ap011 tensor (p _) (q _)). Defined. +(** The tensor product functor preserves identity morphisms. *) Definition functor_ab_tensor_prod_id (A B : AbGroup) : functor_ab_tensor_prod (Id A) (Id B) $== Id (ab_tensor_prod A B). Proof. @@ -374,6 +410,7 @@ Proof. apply functor_ab_tensor_prod_beta_tensor. Defined. +(** The tensor product functor preserves composition. *) Definition functor_ab_tensor_prod_compose {A B C A' B' C' : AbGroup} (f : A $-> B) (g : B $-> C) (f' : A' $-> B') (g' : B' $-> C') : functor_ab_tensor_prod (g $o f) (g' $o f') @@ -387,6 +424,7 @@ Proof. by rewrite 2 functor_ab_tensor_prod_beta_tensor. Defined. +(** The tensor product functor is a 0-bifunctor. *) Global Instance is0bifunctor_ab_tensor_prod : Is0Bifunctor ab_tensor_prod. Proof. rapply Build_Is0Bifunctor'. @@ -395,6 +433,7 @@ Proof. exact (functor_ab_tensor_prod f g). Defined. +(** The tensor product functor is a bifunctor. *) Global Instance is1bifunctor_ab_tensor_prod : Is1Bifunctor ab_tensor_prod. Proof. rapply Build_Is1Bifunctor'. @@ -407,6 +446,11 @@ Proof. exact (functor_ab_tensor_prod_compose f f' g g'). Defined. +(** ** Symmetry of the Tensor Product *) + +(** The tensor product is symmetric in that the order in which we take the tensor shouldn't matter upto isomorphism. *) + +(** We can define a swap map which swaps the order of elementary tensors. *) Definition ab_tensor_swap {A B} : ab_tensor_prod A B $-> ab_tensor_prod B A. Proof. snrapply ab_tensor_prod_rec. @@ -423,6 +467,7 @@ Proof. apply ab_tensor_prod_rec_beta_tensor. Defined. +(** [ab_tensor_swap] is involutive. *) Definition ab_tensor_swap_swap {A B} : ab_tensor_swap $o @ab_tensor_swap A B $== Id _. Proof. @@ -432,6 +477,7 @@ Proof. by rewrite 2 ab_tensor_swap_beta_tensor. Defined. +(** [ab_tensor_swap] is natural in both arguments. This means that it also acts on tensor functors. *) Definition ab_tensor_swap_natural {A B A' B'} (f : A $-> A') (g : B $-> B') : ab_tensor_swap $o functor_ab_tensor_prod f g $== functor_ab_tensor_prod g f $o ab_tensor_swap. @@ -445,6 +491,7 @@ Proof. by rewrite functor_ab_tensor_prod_beta_tensor. Defined. +(** The data of swap together gives us a symmetric braiding on the category of abelian groups. We will later show it is a full symmetric monoidal category. *) Global Instance symmetricbraiding_ab_tensor_prod : SymmetricBraiding ab_tensor_prod. Proof. snrapply Build_SymmetricBraiding. @@ -455,6 +502,11 @@ Proof. - intros; nrapply ab_tensor_swap_swap. Defined. +(** ** Twisting Triple Tensors *) + +(** In order to construct the symmetric monoidal category, we will use what is termed the "Twist construction" in Monoidal.v. This simplifies the data of a symmetric monoidal category by constructing it from simpler parts. For instance, instead of having to prove full associativity [(A ⊗ B) ⊗ C $-> A ⊗ (B ⊗ C)], we can provide a twist map [A ⊗ (B ⊗ C) $-> B ⊗ (A ⊗ C)] and use the symmetric braiding we have so far to prove associativity. *) + +(** Given a triple tensor product, we have a twist map which permutes the first two components. *) Definition ab_tensor_prod_twist {A B C} : ab_tensor_prod A (ab_tensor_prod B C) $-> ab_tensor_prod B (ab_tensor_prod A C). Proof. @@ -478,12 +530,14 @@ Proof. by rewrite tensor_dist_r, tensor_dist_l. Defined. +(** The twist map acts in the expected way on elementary tensors. *) Definition ab_tensor_prod_twist_beta_tensor_tensor {A B C} a b c : @ab_tensor_prod_twist A B C (tensor a (tensor b c)) = tensor b (tensor a c). Proof. rapply ab_tensor_swap_beta_tensor. Defined. +(** The twist map is involutive. *) Definition ab_tensor_prod_twist_twist {A B C} : ab_tensor_prod_twist $o @ab_tensor_prod_twist A B C $== Id _. Proof. @@ -494,6 +548,7 @@ Proof. by rewrite 2 ab_tensor_prod_twist_beta_tensor_tensor. Defined. +(** The twist map is natural in all 3 arguments. This means that the twist map acts on the triple tensor functor in the same way. *) Definition ab_tensor_prod_twist_natural {A B C A' B' C'} (f : A $-> A') (g : B $-> B') (h : C $-> C') : ab_tensor_prod_twist $o fmap11 ab_tensor_prod f (fmap11 ab_tensor_prod g h) @@ -508,33 +563,62 @@ Proof. by rewrite 2 functor_ab_tensor_prod_beta_tensor. Defined. -Require Import Spaces.Int. -Require Import AbGroups.Z. +(** ** Unitality of [abgroup_Z] *) -Definition tensor_grp_pow {A B : AbGroup} (z : Int) (a : A) (b : B) - : tensor (grp_pow a z) b = tensor a (grp_pow b z). +(** In the symmetric monoidal structure on abelian groups, [abgroup_Z] provides the role of a unit. We show that tensoring with [abgroup_Z] on the right is isomorphic to the original group. *) + +(** First we characterise the action of integers via [grp_pow] and their interaction on tensors. This is just a generalisation of the distributivity laws for tensors. *) + +(** Multiplication in the first factor can be factored out. *) +Definition tensor_grp_pow_l {A B : AbGroup} (z : Int) (a : A) (b : B) + : tensor (grp_pow a z) b = grp_pow (tensor a b) z. +Proof. + induction z as [|z IHz|z IHz]. + - nrapply tensor_zero_l. + - rewrite 2 grp_pow_succ. + lhs nrapply tensor_dist_r. + nrapply ap. + exact IHz. + - rewrite 2 grp_pow_pred. + lhs nrapply tensor_dist_r. + snrapply ap011. + + nrapply tensor_neg_l. + + exact IHz. +Defined. + +(** Multiplilcation in the second factor can be factore out. *) +Definition tensor_grp_pow_r {A B : AbGroup} (z : Int) (a : A) (b : B) + : tensor a (grp_pow b z) = grp_pow (tensor a b) z. Proof. - induction z. - - rhs nrapply tensor_zero_r. - nrapply tensor_zero_l. + induction z as [|z IHz|z IHz]. + - nrapply tensor_zero_r. - rewrite 2 grp_pow_succ. - rewrite tensor_dist_r, tensor_dist_l. + lhs nrapply tensor_dist_l. nrapply ap. exact IHz. - rewrite 2 grp_pow_pred. - rewrite tensor_dist_r, tensor_dist_l. + lhs nrapply tensor_dist_l. snrapply ap011. - + rhs nrapply tensor_neg_r. - apply tensor_neg_l. + + nrapply tensor_neg_r. + exact IHz. Defined. +(** Multiplication can be transferred from one factor to the other. The tensor product of [R]-modules will include this as an extra axiom, but here we have [Z]-modules and we can prove it. *) +Definition tensor_grp_pow {A B : AbGroup} (z : Int) (a : A) (b : B) + : tensor (grp_pow a z) b = tensor a (grp_pow b z). +Proof. + rhs nrapply tensor_grp_pow_r. + nrapply tensor_grp_pow_l. +Defined. + +(** [abgroup_Z] is a right identity for the tensor product. *) Definition ab_tensor_prod_Z_r {A} : ab_tensor_prod A abgroup_Z $<~> A. Proof. + (** Checking the inverse map is a homomorphism is easier. *) symmetry. snrapply Build_GroupIsomorphism. - - nrapply grp_homo_tensor_l. + - nrapply grp_homo_tensor_r. exact 1%int. - snrapply isequiv_adjointify. + snrapply ab_tensor_prod_rec. @@ -548,7 +632,7 @@ Proof. with (f $o g $== Id _). snrapply ab_tensor_prod_ind_homotopy. intros a z. - lhs nrapply (ap (grp_homo_tensor_l _)). + lhs nrapply (ap (grp_homo_tensor_r _)). 1: apply ab_tensor_prod_rec_beta_tensor. change (tensor (B:=abgroup_Z) (grp_pow a z) 1%int = tensor a z). lhs nrapply tensor_grp_pow. @@ -560,6 +644,7 @@ Proof. apply grp_unit_r. Defined. +(** We have a right unitor for the tensor product given by unit [abgroup_Z]. Naturality of [ab_tensor_prod_Z_r] is straightforward to prove. *) Global Instance rightunitor_ab_tensor_prod : RightUnitor ab_tensor_prod abgroup_Z. Proof. @@ -581,12 +666,16 @@ Proof. apply grp_pow_natural. Defined. +(** Since we have symmetry of the tensor product, we get left unitality for free. *) Global Instance left_unitor_ab_tensor_prod : LeftUnitor ab_tensor_prod abgroup_Z. Proof. rapply left_unitor_twist. Defined. +(** ** Symmetric Monoidal Strucutre of Tensor Product *) + +(** Using the twist construction we can derive an associator for the tensor product. In other words, we have associativity of the tensor product of abelian groups natural in each factor. *) Global Instance associator_ab_tensor_prod : Associator ab_tensor_prod. Proof. srapply associator_twist. @@ -595,6 +684,7 @@ Proof. - intros; nrapply ab_tensor_prod_twist_natural. Defined. +(** The triangle identity is straightforward to prove using the custom induction principles we proved earlier. *) Global Instance triangle_ab_tensor_prod : TriangleIdentity ab_tensor_prod abgroup_Z. Proof. @@ -602,6 +692,8 @@ Proof. intros A B. snrapply ab_tensor_prod_ind_homotopy_triple. intros a b z. + (** Here we have to get the goal into the correct form to be able to reduce the functions on the elementary tensors. *) + (** TODO: work out a way to reduce these change statements. *) change (functor_ab_tensor_prod (Id A) (rightunitor_ab_tensor_prod B) (tensor a (tensor b z)) = ab_tensor_swap (functor_ab_tensor_prod (Id B) (rightunitor_ab_tensor_prod A) (ab_tensor_prod_twist (tensor a (tensor b z))))). @@ -615,6 +707,7 @@ Proof. exact (tensor_grp_pow _ _ _)^. Defined. +(** The hexagon identity is also straighforward to prove. We simply have to reduce all the involved functions on the elementary tensors using our custom triple tensor induction principle. *) Global Instance hexagon_ab_tensor_prod : HexagonIdentity ab_tensor_prod. Proof. snrapply hexagon_twist. @@ -634,6 +727,7 @@ Proof. reflexivity. Defined. +(** Finally, we can prove the pentagon identity using the quadruple tensor induction principle. As we did before, the work only involves reducing the involved functions on the elementary tensor redexes. *) Global Instance pentagon_ab_tensor_prod : PentagonIdentity ab_tensor_prod. Proof. snrapply pentagon_twist. @@ -663,10 +757,14 @@ Proof. reflexivity. Defined. +(** We therefore have all the data of a monoidal category. *) Global Instance ismonoidal_ab_tensor_prod : IsMonoidal AbGroup ab_tensor_prod abgroup_Z := {}. +(** And furthermore, all the data of a symmetric monoidal category. *) Global Instance issymmmetricmonoidal_ab_tensor_prod : IsSymmetricMonoidal AbGroup ab_tensor_prod abgroup_Z := {}. + +(** TODO: Show that the category of abelian groups is symmetric closed and therefore we have adjoint pair with the tesnor and internal hom. This should allow us to prove lemmas such as tensors distributing over coproducts. *) From b733df518c2f1804b2edae7661700f58b4f0dd49 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 11 Jul 2024 11:32:16 +0200 Subject: [PATCH 04/44] add universal property Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/TensorProduct.v | 104 ++++++++++++++++++---- 1 file changed, 87 insertions(+), 17 deletions(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index 9d006cdee53..776986ed47f 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -1,5 +1,5 @@ Require Import Basics.Overture Basics.Tactics. -Require Import Types.Forall. +Require Import Types.Forall Types.Sigma. Require Import WildCat.Core WildCat.Equiv WildCat.Monoidal WildCat.Bifunctor. Require Import WildCat.NatTrans. Require Import Algebra.Groups.Group Algebra.Groups.QuotientGroup. @@ -158,16 +158,16 @@ Defined. (** Our main recursion principle states that in order to build a map out of the tensor product, it is sufficient to provide a map out of the direct product which is bilinear, that is, a map that preserves addition in both arguments of the product. *) Definition ab_tensor_prod_rec {A B C : AbGroup} - (f : A * B -> C) - (l : forall a b b', f (a, b + b') = f (a, b) + f (a, b')) - (r : forall a a' b, f (a + a', b) = f (a, b) + f (a', b)) + (f : A -> B -> C) + (l : forall a b b', f a (b + b') = f a b + f a b') + (r : forall a a' b, f (a + a') b = f a b + f a' b) : ab_tensor_prod A B $-> C. Proof. unfold ab_tensor_prod. snrapply grp_quotient_rec. - snrapply grp_homo_abel_rec. snrapply FreeGroup_rec. - exact f. + exact (uncurry f). - intros x H. strip_truncations. induction H as @@ -204,13 +204,13 @@ Defined. (** Since we defined [ab_tensor_prod_rec] using the recursors of the underlying type, we get an annoying artifact of [x + 0] instead of [x] when acting on elementary tensors. Typically in an argument we want our recursor to act on elementary tensors without the extra [0] and this lemma makes sure of that. *) Definition ab_tensor_prod_rec_beta_tensor {A B C : AbGroup} - (f : A * B -> C) - (l : forall a b b', f (a, b + b') = f (a, b) + f (a, b')) - (r : forall a a' b, f (a + a', b) = f (a, b) + f (a', b)) + (f : A -> B -> C) + (l : forall a b b', f a (b + b') = f a b + f a b') + (r : forall a a' b, f (a + a') b = f a b + f a' b) (a : A) (b : B) - : ab_tensor_prod_rec f l r (tensor a b) = f (a, b). + : ab_tensor_prod_rec f l r (tensor a b) = f a b. Proof. - change (f (a, b) + mon_unit = f (a, b)). + change (f a b + mon_unit = f a b). apply grp_unit_r. Defined. @@ -362,6 +362,77 @@ Proof. exact (ap011 (+) p q). Defined. +(** ** Universal Property of the Tensor Product *) + +(** A function of two variables is biadditive if it preserves the operation in each variable. *) +Class IsBiadditive {A B C : Type} `{SgOp A, SgOp B, SgOp C} (f : A -> B -> C) := { + isbiadditive_l :: forall b, IsSemiGroupPreserving (flip f b); + isbiadditive_r :: forall a, IsSemiGroupPreserving (f a); +}. + +Definition issig_IsBiadditive {A B C : Type} `{SgOp A, SgOp B, SgOp C} + (f : A -> B -> C) + : _ <~> IsBiadditive f + := ltac:(issig). + +(** The truncation level of the [IsBiadditive f] predicate is determined by the truncation level of the codomain. This will almost always be a hset. *) +Global Instance istrunc_isbiadditive `{Funext} + {A B C : Type} `{SgOp A, SgOp B, SgOp C} + (f : A -> B -> C) n `{IsTrunc n.+1 C} + : IsTrunc n (IsBiadditive f). +Proof. + nrapply istrunc_equiv_istrunc. + 1: rapply issig_IsBiadditive. + unfold IsSemiGroupPreserving. + exact _. +Defined. + +(** The elementary tensor map is biadditive. *) +Global Instance isbiadditive_tensor (A B : AbGroup) + : IsBiadditive (@tensor A B) := {| + isbiadditive_l := fun b a a' => tensor_dist_r a a' b; + isbiadditive_r := tensor_dist_l; +|}. + +(** The type of biadditive maps. *) +Record Biadditive (A B C : Type) `{SgOp A, SgOp B, SgOp C} := { + biadditive_fun :> A -> B -> C; + biadditive_isbiadditive :: IsBiadditive biadditive_fun; +}. + +Definition issig_Biadditive {A B C : Type} `{SgOp A, SgOp B, SgOp C} + : _ <~> Biadditive A B C + := ltac:(issig). + +(** The universal property of the tensor product is that biadditive maps between abelian groups are in one-to-one corresondance with maps out of the tensor product. In this sense, the tensor product is the most perfect object describing biadditive maps between two abelian groups. *) +Definition equiv_ab_tensor_prod_rec `{Funext} (A B C : AbGroup) + : Biadditive A B C <~> (ab_tensor_prod A B $-> C). +Proof. + snrapply equiv_adjointify. + - intros [f [l r]]. + exact (ab_tensor_prod_rec f r (fun a a' b => l b a a')). + - intros f. + exists (fun x y => f (tensor x y)). + snrapply Build_IsBiadditive. + + intros b a a'. + unfold flip. + rewrite tensor_dist_r. + nrapply grp_homo_op. + + intros a a' b. + rewrite tensor_dist_l. + nrapply grp_homo_op. + - intros f. + snrapply equiv_path_grouphomomorphism. + snrapply ab_tensor_prod_ind_homotopy. + intros a b. + nrapply ab_tensor_prod_rec_beta_tensor. + - intros [f [l r]]. + snrapply (equiv_ap_inv' issig_Biadditive). + rapply path_sigma_hprop. + funext a b. + snrapply grp_unit_r. +Defined. + (** ** Functoriality of the Tensor Product *) (** The tensor product produces a bifunctor and we will later show that it gives a symmetric monoidal structure on the category of abelian groups. *) @@ -372,7 +443,7 @@ Definition functor_ab_tensor_prod {A B A' B' : AbGroup} : ab_tensor_prod A B $-> ab_tensor_prod A' B'. Proof. snrapply ab_tensor_prod_rec. - - intros [a b]. + - intros a b. exact (tensor (f a) (g b)). - intros a b b'; hnf. rewrite grp_homo_op. @@ -454,7 +525,7 @@ Defined. Definition ab_tensor_swap {A B} : ab_tensor_prod A B $-> ab_tensor_prod B A. Proof. snrapply ab_tensor_prod_rec. - - exact (uncurry (flip tensor)). + - exact (flip tensor). - intros a b b'. apply tensor_dist_r. - intros a a' b. @@ -464,7 +535,7 @@ Defined. Definition ab_tensor_swap_beta_tensor {A B} a b : @ab_tensor_swap A B (tensor a b) = tensor b a. Proof. - apply ab_tensor_prod_rec_beta_tensor. + nrapply ab_tensor_prod_rec_beta_tensor. Defined. (** [ab_tensor_swap] is involutive. *) @@ -511,10 +582,9 @@ Definition ab_tensor_prod_twist {A B C} : ab_tensor_prod A (ab_tensor_prod B C) $-> ab_tensor_prod B (ab_tensor_prod A C). Proof. snrapply ab_tensor_prod_rec. - - apply prod_ind. - intros a. + - intros a. snrapply ab_tensor_prod_rec. - + intros [b c]. + + intros b c. exact (tensor b (tensor a c)). + intros b c c'; hnf. lhs nrapply ap. @@ -622,7 +692,7 @@ Proof. exact 1%int. - snrapply isequiv_adjointify. + snrapply ab_tensor_prod_rec. - * exact (uncurry grp_pow_homo). + * exact grp_pow_homo. * intros a z z'; cbn beta; unfold uncurry, fst, snd. nrapply grp_homo_op. * intros a a' z; cbn beta; unfold uncurry, fst, snd. From f9c589c80d1ef8ded00cc73138aa1614f4b8ffc9 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Fri, 12 Jul 2024 16:34:16 -0400 Subject: [PATCH 05/44] TensorProduct: fix typos in comments --- theories/Algebra/AbGroups/TensorProduct.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index 776986ed47f..b36e99755ba 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -214,11 +214,11 @@ Proof. apply grp_unit_r. Defined. -(** The induction principle is a little different to the recursor. In the recursor, which is the non-dependent case of the induction principle, we were landing in an abelian group hence the codomain came equipped with the group operations which we wish to presere with the binlinearity conditions. +(** The induction principle is a little different to the recursor. In the recursor, which is the non-dependent case of the induction principle, we were landing in an abelian group hence the codomain came equipped with the group operations which we wish to preserve with the bilinearity conditions. -The induction principle will require these bilinearity conditions, but we have to postulate the data of a "dependent group" in the codomain in order to state these properly. In general, we don't have any use for a general induction principle into a hset and so we can drop these depedent bilinearity paths. +The induction principle will require these bilinearity conditions, but we have to postulate the data of a "dependent group" in the codomain in order to state these properly. In general, we don't have any use for a general induction principle into a hset and so we can drop these dependent bilinearity paths. -The hprop induction principle therefore requires that the codomain is a hprop in addition to being closed under the various group operations of the domain. Most importantly we hypothsise that we can prove a property on an elementary tensor [tensor a b]. *) +The hprop induction principle therefore requires that the codomain is a hprop in addition to being closed under the various group operations of the domain. Most importantly we hypothesise that we can prove a property on an elementary tensor [tensor a b]. *) Definition ab_tensor_prod_ind_hprop {A B : AbGroup} (P : ab_tensor_prod A B -> Type) {H : forall x, IsHProp (P x)} @@ -250,7 +250,7 @@ Proof. by apply H4. Defined. -(** As a commonly occuring special case of the above induction principle, we have the case when the predicate in question is showing two group homomorphisms are homotopic. In order to do this, it suffices to show it only for elementary tensors. The homotopy is closed under all the group operations so we don't need to hyptoehsise anything else. *) +(** As a commonly occuring special case of the above induction principle, we have the case when the predicate in question is showing two group homomorphisms are homotopic. In order to do this, it suffices to show it only for elementary tensors. The homotopy is closed under all the group operations so we don't need to hypthesise anything else. *) Definition ab_tensor_prod_ind_homotopy {A B G : AbGroup} {f f' : ab_tensor_prod A B $-> G} (H : forall a b, f (tensor a b) = f' (tensor a b)) @@ -267,7 +267,7 @@ Proof. exact (ap011 (+) p q). Defined. -(** As an even more specialised case, we occasionally have the second homomorphism being a sum of abelian group homomorphism. In those cases, it is easier to give this specialised lemma. *) +(** As an even more specialised case, we occasionally have the second homomorphism being a sum of abelian group homomorphisms. In those cases, it is easier to give this specialised lemma. *) Definition ab_tensor_prod_ind_homotopy_plus {A B G : AbGroup} {f f' f'' : ab_tensor_prod A B $-> G} (H : forall a b, f (tensor a b) = f' (tensor a b) + f'' (tensor a b)) @@ -635,7 +635,7 @@ Defined. (** ** Unitality of [abgroup_Z] *) -(** In the symmetric monoidal structure on abelian groups, [abgroup_Z] provides the role of a unit. We show that tensoring with [abgroup_Z] on the right is isomorphic to the original group. *) +(** In the symmetric monoidal structure on abelian groups, [abgroup_Z] is the unit. We show that tensoring with [abgroup_Z] on the right is isomorphic to the original group. *) (** First we characterise the action of integers via [grp_pow] and their interaction on tensors. This is just a generalisation of the distributivity laws for tensors. *) @@ -656,7 +656,7 @@ Proof. + exact IHz. Defined. -(** Multiplilcation in the second factor can be factore out. *) +(** Multiplication in the second factor can be factored out. *) Definition tensor_grp_pow_r {A B : AbGroup} (z : Int) (a : A) (b : B) : tensor a (grp_pow b z) = grp_pow (tensor a b) z. Proof. @@ -743,7 +743,7 @@ Proof. rapply left_unitor_twist. Defined. -(** ** Symmetric Monoidal Strucutre of Tensor Product *) +(** ** Symmetric Monoidal Structure of Tensor Product *) (** Using the twist construction we can derive an associator for the tensor product. In other words, we have associativity of the tensor product of abelian groups natural in each factor. *) Global Instance associator_ab_tensor_prod : Associator ab_tensor_prod. From df441c611ea8e76268da364f110f2b9dfbdb458c Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Fri, 12 Jul 2024 16:50:44 -0400 Subject: [PATCH 06/44] TensorProduct: drop (P 0) from induction principles --- theories/Algebra/AbGroups/TensorProduct.v | 24 ++++++----------------- 1 file changed, 6 insertions(+), 18 deletions(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index b36e99755ba..2addc04f8df 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -222,7 +222,6 @@ The hprop induction principle therefore requires that the codomain is a hprop in Definition ab_tensor_prod_ind_hprop {A B : AbGroup} (P : ab_tensor_prod A B -> Type) {H : forall x, IsHProp (P x)} - (H1 : P 0) (H2 : forall a b, P (tensor a b)) (H3 : forall x, P x -> P (-x)) (H4 : forall x y, P x -> P y -> P (x + y)) @@ -231,19 +230,17 @@ Proof. unfold ab_tensor_prod. srapply Quotient_ind_hprop. srapply Abel_ind_hprop. - srapply FreeGroup_ind_hprop. - - exact H1. + srapply FreeGroup_ind_hprop; cbn beta. + - exact (transport P (tensor_zero_l 0) (H2 0 0)). - intros [a b]. apply H2. - - cbn beta. - intros w H5. + - intros w H5. rewrite ab_negate. change (P (quotient_abgroup_map _ subgroup_bilinear_pairs (- ab w))). rewrite grp_homo_inv. apply H3. exact H5. - - cbn beta. - intros x y Hx Hy. + - intros x y Hx Hy. change (P (quotient_abgroup_map _ subgroup_bilinear_pairs (ab (x + y)))). rewrite issemigrouppreserving_ab. rewrite grp_homo_op. @@ -257,7 +254,6 @@ Definition ab_tensor_prod_ind_homotopy {A B G : AbGroup} : f $== f'. Proof. rapply (ab_tensor_prod_ind_hprop (fun _ => _)). - - by rewrite 2 grp_homo_unit. - exact H. - intros x p. rewrite 2 grp_homo_inv. @@ -278,17 +274,14 @@ Definition ab_tensor_prod_ind_homotopy_plus {A B G : AbGroup} Definition ab_tensor_prod_ind_hprop_triple {A B C : AbGroup} (P : ab_tensor_prod A (ab_tensor_prod B C) -> Type) (H : forall x, IsHProp (P x)) - (H1 : P 0) (H2 : forall a b c, P (tensor a (tensor b c))) (H3 : forall x, P x -> P (-x)) (H4 : forall x y, P x -> P y -> P (x + y)) : forall x, P x. Proof. - rapply (ab_tensor_prod_ind_hprop P H1). + rapply (ab_tensor_prod_ind_hprop P). - intros a. rapply (ab_tensor_prod_ind_hprop (fun x => P (tensor _ x))). - + rewrite tensor_zero_r. - exact H1. + nrapply H2. + intros x Hx. rewrite tensor_neg_r. @@ -308,7 +301,6 @@ Definition ab_tensor_prod_ind_homotopy_triple {A B C G : AbGroup} : f $== f'. Proof. rapply (ab_tensor_prod_ind_hprop_triple (fun _ => _)). - - by rewrite 2 grp_homo_unit. - exact H. - intros x p. rewrite 2 grp_homo_inv. @@ -322,17 +314,14 @@ Defined. Definition ab_tensor_prod_ind_hprop_quad {A B C D : AbGroup} (P : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) -> Type) (H : forall x, IsHProp (P x)) - (H1 : P 0) (H2 : forall a b c d, P (tensor a (tensor b (tensor c d)))) (H3 : forall x, P x -> P (-x)) (H4 : forall x y, P x -> P y -> P (x + y)) : forall x, P x. Proof. - rapply (ab_tensor_prod_ind_hprop P H1). + rapply (ab_tensor_prod_ind_hprop P). - intros a. rapply (ab_tensor_prod_ind_hprop_triple (fun x => P (tensor _ x))). - + rewrite tensor_zero_r. - exact H1. + nrapply H2. + intros x Hx. rewrite tensor_neg_r. @@ -352,7 +341,6 @@ Definition ab_tensor_prod_ind_homotopy_quad {A B C D G : AbGroup} : f $== f'. Proof. rapply (ab_tensor_prod_ind_hprop_quad (fun _ => _)). - - by rewrite 2 grp_homo_unit. - exact H. - intros x p. rewrite 2 grp_homo_inv. From 87afe8544125819287b65e2731237bd1eae5df24 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sat, 13 Jul 2024 14:00:34 +0200 Subject: [PATCH 07/44] Abelianization: rename ab map to abel_in Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/Abelianization.v | 90 +++++++++++----------- 1 file changed, 46 insertions(+), 44 deletions(-) diff --git a/theories/Algebra/AbGroups/Abelianization.v b/theories/Algebra/AbGroups/Abelianization.v index 4446e0d5b72..cebb7befec7 100644 --- a/theories/Algebra/AbGroups/Abelianization.v +++ b/theories/Algebra/AbGroups/Abelianization.v @@ -52,10 +52,10 @@ From this we can show that Abel G is an abelian group. In fact this models the following HIT: HIT Abel (G : Group) := - | ab : G -> Abel G - | ab_comm : forall x y z, ab (x * (y * z)) = ab (x * (z * y)). + | abel_in : G -> Abel G + | abel_in_comm : forall x y z, abel_in (x * (y * z)) = abel_in (x * (z * y)). -We also derive ab and ab_comm from our coequalizer definition, and even prove the induction and computation rules for this HIT. +We also derive [abel_in] and [abel_in_comm] from our coequalizer definition, and even prove the induction and computation rules for this HIT. This HIT was suggested by Dan Christensen. *) @@ -80,15 +80,15 @@ Section Abel. (uncurry2 (fun a b c : G => a * (c * b)))). (** We have a natural map from G to Abel G. *) - Definition ab : G -> Abel. + Definition abel_in : G -> Abel. Proof. intro g. apply tr, coeq, g. Defined. (** This map satisfies the condition ab_comm. *) - Definition ab_comm a b c - : ab (a * (b * c)) = ab (a * (c * b)). + Definition abel_in_comm a b c + : abel_in (a * (b * c)) = abel_in (a * (c * b)). Proof. apply (ap tr). exact (cglue (a, b, c)). @@ -99,7 +99,7 @@ Section Abel. (** We can derive the induction principle from the ones for truncation and the coequalizer. *) Definition Abel_ind (P : Abel -> Type) `{forall x, IsHSet (P x)} - (a : forall x, P (ab x)) (c : forall x y z, DPath P (ab_comm x y z) + (a : forall x, P (abel_in x)) (c : forall x y z, DPath P (abel_in_comm x y z) (a (x * (y * z))) (a (x * (z * y)))) : forall (x : Abel), P x. Proof. @@ -112,11 +112,11 @@ Section Abel. Defined. (** The computation rule can also be proven. *) - Definition Abel_ind_beta_ab_comm (P : Abel -> Type) - `{forall x, IsHSet (P x)}(a : forall x, P (ab x)) - (c : forall x y z, DPath P (ab_comm x y z) + Definition Abel_ind_beta_abel_in_comm (P : Abel -> Type) + `{forall x, IsHSet (P x)}(a : forall x, P (abel_in x)) + (c : forall x y z, DPath P (abel_in_comm x y z) (a (x * (y * z))) (a (x * (z * y)))) - (x y z : G) : apD (Abel_ind P a c) (ab_comm x y z) = c x y z. + (x y z : G) : apD (Abel_ind P a c) (abel_in_comm x y z) = c x y z. Proof. refine (apD_compose' tr _ _ @ ap _ _ @ concat_V_pp _ _). rapply Coeq_ind_beta_cglue. @@ -133,7 +133,7 @@ Section Abel. (** Here is a simpler version of Abel_ind when our target is an HProp. This lets us discard all the higher paths. *) Definition Abel_ind_hprop (P : Abel -> Type) `{forall x, IsHProp (P x)} - (a : forall x, P (ab x)) : forall (x : Abel), P x. + (a : forall x, P (abel_in x)) : forall (x : Abel), P x. Proof. srapply (Abel_ind _ a). intros; apply path_ishprop. @@ -152,9 +152,10 @@ End Abel. (** The [IsHProp] argument of [Abel_ind_hprop] can usually be found by typeclass resolution, but [srapply] is slow, so we use this tactic instead. *) Local Ltac Abel_ind_hprop x := snrapply Abel_ind_hprop; [exact _ | intro x]. -(** We make sure that G is implicit in the arguments of ab and ab_comm. *) -Arguments ab {_}. -Arguments ab_comm {_}. +(** We make sure that G is implicit in the arguments of [abel_in + and [abel_in_comm]. *) +Arguments abel_in {_}. +Arguments abel_in_comm {_}. (** Now we can show that Abel G is in fact an abelian group. *) @@ -163,7 +164,9 @@ Section AbelGroup. Context (G : Group). (** Firstly we derive the operation on Abel G. This is defined as follows: - ab x + ab y := ab (x y) + << + abel_in x + abel_in y := abel_in (x * y) + >> But we need to also check that it preserves ab_comm in the appropriate way. *) Global Instance abel_sgop : SgOp (Abel G). Proof. @@ -173,21 +176,21 @@ Section AbelGroup. revert a. srapply Abel_rec. { intro a. - exact (ab (a * b)). } + exact (abel_in (a * b)). } intros a c d; hnf. (* The pattern seems to be to alternate associativity and ab_comm. *) refine (ap _ (associativity _ _ _)^ @ _). - refine (ab_comm _ _ _ @ _). + refine (abel_in_comm _ _ _ @ _). refine (ap _ (associativity _ _ _) @ _). - refine (ab_comm _ _ _ @ _). + refine (abel_in_comm _ _ _ @ _). refine (ap _ (associativity _ _ _)^ @ _). - refine (ab_comm _ _ _ @ _). + refine (abel_in_comm _ _ _ @ _). refine (ap _ (associativity _ _ _)). } intros b c d. revert a. Abel_ind_hprop a; simpl. refine (ap _ (associativity _ _ _) @ _). - refine (ab_comm _ _ _ @ _). + refine (abel_in_comm _ _ _ @ _). refine (ap _ (associativity _ _ _)^). Defined. @@ -205,7 +208,7 @@ Section AbelGroup. Global Instance abel_issemigroup : IsSemiGroup (Abel G) := {}. (** We define the unit as ab of the unit of G *) - Global Instance abel_mon_unit : MonUnit (Abel G) := ab mon_unit. + Global Instance abel_mon_unit : MonUnit (Abel G) := abel_in mon_unit. (** By using Abel_ind_hprop we can prove the left and right identity laws. *) Global Instance abel_leftidentity : LeftIdentity abel_sgop abel_mon_unit. @@ -230,25 +233,30 @@ Section AbelGroup. Abel_ind_hprop y. revert x. Abel_ind_hprop x. - refine ((ap ab (left_identity _))^ @ _). - refine (_ @ (ap ab (left_identity _))). - apply ab_comm. + refine ((ap abel_in (left_identity _))^ @ _). + refine (_ @ (ap abel_in (left_identity _))). + apply abel_in_comm. Defined. (** Now we can define the negation. This is just - - (ab g) := (ab (g^-1)) + << + - (abel_in g) := abel_in (- g) + >> However when checking that it respects ab_comm we have to show the following: - ab (- z * - y * - x) = ab (- y * - z * - x) - there is no obvious way to do this, but we note that ab (x * y) is exactly the definition of ab x + ab y! Hence by commutativity we can show this. *) + << + abel_in (- z * - y * - x) = abel_in (- y * - z * - x) + >> + there is no obvious way to do this, but we note that [abel_in (x * y)] is exactly the definition of [abel_in x + abel_in y]! Hence by commutativity we can show this. *) Global Instance abel_negate : Negate (Abel G). Proof. srapply Abel_rec. { intro g. - exact (ab (-g)). } + exact (abel_in (-g)). } intros x y z; cbn. rewrite ?negate_sg_op. - change (ab(- z) * ab(- y) * ab (- x) = ab (- y) * ab (- z) * ab(- x)). - by rewrite (commutativity (ab (-z)) (ab (-y))). + change (abel_in (- z) * abel_in (- y) * abel_in (- x) + = abel_in (- y) * abel_in (- z) * abel_in (- x)). + by rewrite (commutativity (abel_in (-z)) (abel_in (-y))). Defined. (** Again by Abel_ind_hprop and the corresponding laws for G we can prove the left and right inverse laws. *) @@ -270,29 +278,23 @@ Section AbelGroup. (** And since the operation is commutative, an abelian group. *) Global Instance isabgroup_abel : IsAbGroup (Abel G) := {}. - (** By definition, the map ab is also a group homomorphism. *) - Global Instance issemigrouppreserving_ab : IsSemiGroupPreserving ab. + (** By definition, the map [abel_in] is also a group homomorphism. *) + Global Instance issemigrouppreserving_abel_in : IsSemiGroupPreserving abel_in. Proof. by unfold IsSemiGroupPreserving. Defined. - Global Instance ismonoidpreserving_ab : IsMonoidPreserving ab. + Global Instance ismonoidpreserving_abel_in : IsMonoidPreserving abel_in. Proof. split. 1: exact _. reflexivity. Defined. - - (** [ab] preserves negation *) - Definition ab_negate x : ab (-x) = - ab x. - Proof. - exact (preserves_negate (f:=ab) x). - Defined. End AbelGroup. -(** We can easily prove that ab is a surjection. *) -Global Instance issurj_ab {G : Group} : IsSurjection (@ab G). +(** We can easily prove that [abel_in] is a surjection. *) +Global Instance issurj_abel_in {G : Group} : IsSurjection (@abel_in G). Proof. apply BuildIsSurjection. Abel_ind_hprop x. @@ -313,12 +315,12 @@ Proof. - exact _. Defined. -(** The unit of this map is the map ab which typeclasses can pick up to be a homomorphism. We write it out explicitly here. *) +(** The unit of this map is the map [abel_in] which typeclasses can pick up to be a homomorphism. We write it out explicitly here. *) Definition abel_unit (X : Group) : GroupHomomorphism X (abel X). Proof. snrapply @Build_GroupHomomorphism. - + exact ab. + + exact abel_in. + exact _. Defined. From 4c9a8d2a769c282937c395c9fe11cfb6ef28b7bd Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sat, 13 Jul 2024 14:09:16 +0200 Subject: [PATCH 08/44] fix abel_in negation lemma usage Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/Abelianization.v | 8 ++++---- theories/Algebra/AbGroups/FreeAbelianGroup.v | 4 ++-- theories/Algebra/AbGroups/TensorProduct.v | 14 +++++++------- 3 files changed, 13 insertions(+), 13 deletions(-) diff --git a/theories/Algebra/AbGroups/Abelianization.v b/theories/Algebra/AbGroups/Abelianization.v index cebb7befec7..3a699abe659 100644 --- a/theories/Algebra/AbGroups/Abelianization.v +++ b/theories/Algebra/AbGroups/Abelianization.v @@ -316,8 +316,8 @@ Proof. Defined. (** The unit of this map is the map [abel_in] which typeclasses can pick up to be a homomorphism. We write it out explicitly here. *) -Definition abel_unit (X : Group) - : GroupHomomorphism X (abel X). +Definition abel_unit {G : Group} + : GroupHomomorphism G (abel G). Proof. snrapply @Build_GroupHomomorphism. + exact abel_in. @@ -342,7 +342,7 @@ Defined. (** Finally we can prove that our construction abel is an abelianization. *) Global Instance isabelianization_abel {G : Group} - : IsAbelianization (abel G) (abel_unit G). + : IsAbelianization (abel G) abel_unit. Proof. intros A. constructor. { intros h. @@ -392,7 +392,7 @@ Global Instance issurj_isabelianization {G : Group} : IsAbelianization A eta -> IsSurjection eta. Proof. intros k. - pose (homotopic_isabelianization A (abel G) eta (abel_unit G)) as p. + pose (homotopic_isabelianization A (abel G) eta abel_unit) as p. refine (@cancelL_isequiv_conn_map _ _ _ _ _ _ _ (conn_map_homotopic _ _ _ p _)). Defined. diff --git a/theories/Algebra/AbGroups/FreeAbelianGroup.v b/theories/Algebra/AbGroups/FreeAbelianGroup.v index 76267f0d2a7..5c486704406 100644 --- a/theories/Algebra/AbGroups/FreeAbelianGroup.v +++ b/theories/Algebra/AbGroups/FreeAbelianGroup.v @@ -31,7 +31,7 @@ Definition FreeAbGroup (S : Type) : AbGroup := abel (FreeGroup S). Definition freeabgroup_in {S : Type} : S -> FreeAbGroup S - := abel_unit _ o freegroup_in. + := abel_unit o freegroup_in. (** The abelianization of a free group on a set is a free abelian group on that set. *) Global Instance isfreeabgroupon_isabelianization_isfreegroup `{Funext} @@ -54,6 +54,6 @@ Global Instance isfreeabgroup_freeabgroup `{Funext} (S : Type) : IsFreeAbGroup (FreeAbGroup S). Proof. exists S. - exists (abel_unit (FreeGroup S) o freegroup_in). + exists (abel_unit (G:=FreeGroup S) o freegroup_in). srapply isfreeabgroupon_isabelianization_isfreegroup. Defined. diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index 2addc04f8df..88fc636a646 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -180,7 +180,7 @@ Proof. apply grp_moveL_1M^-1%equiv. apply grp_moveL_gM^-1%equiv. unfold freeabgroup_in. - change (grp_homo_abel_rec ?f (abel_unit ?G ?x)) with (f x). + change (grp_homo_abel_rec ?f (abel_unit ?x)) with (f x). simpl. rewrite 3 grp_unit_r. rhs rapply abgroup_commutative. @@ -191,7 +191,7 @@ Proof. apply grp_moveL_1M^-1%equiv. apply grp_moveL_gM^-1%equiv. unfold freeabgroup_in. - change (grp_homo_abel_rec ?f (abel_unit ?G ?x)) with (f x). + change (grp_homo_abel_rec ?f (abel_unit ?x)) with (f x). simpl. rewrite 3 grp_unit_r. rhs rapply abgroup_commutative. @@ -235,15 +235,15 @@ Proof. - intros [a b]. apply H2. - intros w H5. - rewrite ab_negate. - change (P (quotient_abgroup_map _ subgroup_bilinear_pairs (- ab w))). + change (abel_in ?x) with (abel_unit x). + rewrite grp_homo_inv. + change (P (quotient_abgroup_map _ subgroup_bilinear_pairs (- abel_unit w))). rewrite grp_homo_inv. apply H3. exact H5. - intros x y Hx Hy. - change (P (quotient_abgroup_map _ subgroup_bilinear_pairs (ab (x + y)))). - rewrite issemigrouppreserving_ab. - rewrite grp_homo_op. + change (P (quotient_abgroup_map _ subgroup_bilinear_pairs (abel_unit (x + y)))). + rewrite 2 grp_homo_op. by apply H4. Defined. From 4f84baf8f1a67cc83ffcc48b0f0eeb4ec6fd8fe1 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Sat, 13 Jul 2024 10:02:50 -0400 Subject: [PATCH 09/44] Abelianization: inline proof of abel_unit --- theories/Algebra/AbGroups/Abelianization.v | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/theories/Algebra/AbGroups/Abelianization.v b/theories/Algebra/AbGroups/Abelianization.v index 3a699abe659..94c7245cd6a 100644 --- a/theories/Algebra/AbGroups/Abelianization.v +++ b/theories/Algebra/AbGroups/Abelianization.v @@ -317,12 +317,8 @@ Defined. (** The unit of this map is the map [abel_in] which typeclasses can pick up to be a homomorphism. We write it out explicitly here. *) Definition abel_unit {G : Group} - : GroupHomomorphism G (abel G). -Proof. - snrapply @Build_GroupHomomorphism. - + exact abel_in. - + exact _. -Defined. + : GroupHomomorphism G (abel G) + := @Build_GroupHomomorphism G (abel G) abel_in _. Definition grp_homo_abel_rec {G : Group} {A : AbGroup} (f : G $-> A) : abel G $-> A. From 82b0febcec8ad0dadef48260b0165f7599f65e30 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sat, 13 Jul 2024 17:02:58 +0200 Subject: [PATCH 10/44] simplify induction principles Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/TensorProduct.v | 83 ++++++++++------------- theories/Algebra/Groups/FreeGroup.v | 13 ++-- theories/Algebra/Groups/QuotientGroup.v | 9 +++ 3 files changed, 50 insertions(+), 55 deletions(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index 88fc636a646..b8b1227eadb 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -223,27 +223,21 @@ Definition ab_tensor_prod_ind_hprop {A B : AbGroup} (P : ab_tensor_prod A B -> Type) {H : forall x, IsHProp (P x)} (H2 : forall a b, P (tensor a b)) - (H3 : forall x, P x -> P (-x)) - (H4 : forall x y, P x -> P y -> P (x + y)) + (H4 : forall x y, P x -> P y -> P (x - y)) : forall x, P x. Proof. + assert (Hzero : P 0) by exact (transport P (tensor_zero_l 0) (H2 0 0)). unfold ab_tensor_prod. - srapply Quotient_ind_hprop. - srapply Abel_ind_hprop. + srapply grp_quotient_ind_hprop. + srapply Abel_ind_hprop; cbn beta. srapply FreeGroup_ind_hprop; cbn beta. - - exact (transport P (tensor_zero_l 0) (H2 0 0)). + - exact Hzero. - intros [a b]. apply H2. - - intros w H5. - change (abel_in ?x) with (abel_unit x). - rewrite grp_homo_inv. - change (P (quotient_abgroup_map _ subgroup_bilinear_pairs (- abel_unit w))). - rewrite grp_homo_inv. - apply H3. - exact H5. - intros x y Hx Hy. - change (P (quotient_abgroup_map _ subgroup_bilinear_pairs (abel_unit (x + y)))). - rewrite 2 grp_homo_op. + change (P (grp_quotient_map (abel_unit (-x + y)))). + rewrite grp_homo_op, ab_comm, grp_homo_op. + rewrite 2 grp_homo_inv. by apply H4. Defined. @@ -255,12 +249,12 @@ Definition ab_tensor_prod_ind_homotopy {A B G : AbGroup} Proof. rapply (ab_tensor_prod_ind_hprop (fun _ => _)). - exact H. - - intros x p. - rewrite 2 grp_homo_inv. - exact (ap (-) p). - intros x y p q. rewrite 2 grp_homo_op. - exact (ap011 (+) p q). + nrefine (ap011 (+) p _). + rhs nrapply grp_homo_inv. + lhs nrapply grp_homo_inv. + exact (ap (-) q). Defined. (** As an even more specialised case, we occasionally have the second homomorphism being a sum of abelian group homomorphisms. In those cases, it is easier to give this specialised lemma. *) @@ -274,63 +268,56 @@ Definition ab_tensor_prod_ind_homotopy_plus {A B G : AbGroup} Definition ab_tensor_prod_ind_hprop_triple {A B C : AbGroup} (P : ab_tensor_prod A (ab_tensor_prod B C) -> Type) (H : forall x, IsHProp (P x)) - (H2 : forall a b c, P (tensor a (tensor b c))) - (H3 : forall x, P x -> P (-x)) - (H4 : forall x y, P x -> P y -> P (x + y)) + (Hin : forall a b c, P (tensor a (tensor b c))) + (Hop : forall x y, P x -> P y -> P (x - y)) : forall x, P x. Proof. rapply (ab_tensor_prod_ind_hprop P). - intros a. rapply (ab_tensor_prod_ind_hprop (fun x => P (tensor _ x))). - + nrapply H2. - + intros x Hx. - rewrite tensor_neg_r. - by apply H3. + + nrapply Hin. + intros x y Hx Hy. rewrite tensor_dist_l. - by apply H4. - - exact H3. - - exact H4. + rewrite tensor_neg_r. + by apply Hop. + - exact Hop. Defined. (** Similar to before, we specialise the triple tensor induction principle for proving homotopies of trilinear functions. *) -(* TODO: The proof is almost exactly the same as the bilinear case. Is there a way we can share the work? *) Definition ab_tensor_prod_ind_homotopy_triple {A B C G : AbGroup} {f f' : ab_tensor_prod A (ab_tensor_prod B C) $-> G} (H : forall a b c, f (tensor a (tensor b c)) = f' (tensor a (tensor b c))) : f $== f'. Proof. - rapply (ab_tensor_prod_ind_hprop_triple (fun _ => _)). - - exact H. - - intros x p. - rewrite 2 grp_homo_inv. - exact (ap (-) p). + rapply ab_tensor_prod_ind_homotopy. + intros a. + rapply ab_tensor_prod_ind_hprop. + - exact (H a). - intros x y p q. + rewrite tensor_dist_l. + rewrite tensor_neg_r. rewrite 2 grp_homo_op. - exact (ap011 (+) p q). + rewrite 2 grp_homo_inv. + exact (ap011 (fun x y => x - y) p q). Defined. (** As explained for the bilinear and trilinear cases, we also derive an induction principle for quadruple tensors giving us dependent quadrilinear maps. *) Definition ab_tensor_prod_ind_hprop_quad {A B C D : AbGroup} (P : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) -> Type) (H : forall x, IsHProp (P x)) - (H2 : forall a b c d, P (tensor a (tensor b (tensor c d)))) - (H3 : forall x, P x -> P (-x)) - (H4 : forall x y, P x -> P y -> P (x + y)) + (Hin : forall a b c d, P (tensor a (tensor b (tensor c d)))) + (Hop : forall x y, P x -> P y -> P (x - y)) : forall x, P x. Proof. rapply (ab_tensor_prod_ind_hprop P). - intros a. rapply (ab_tensor_prod_ind_hprop_triple (fun x => P (tensor _ x))). - + nrapply H2. - + intros x Hx. - rewrite tensor_neg_r. - by apply H3. + + nrapply Hin. + intros x y Hx Hy. rewrite tensor_dist_l. - by apply H4. - - exact H3. - - exact H4. + rewrite tensor_neg_r. + by apply Hop. + - exact Hop. Defined. (** To construct a homotopy between quadrilinear maps we need only check equality for the quadruple elementary tensor. *) @@ -342,12 +329,10 @@ Definition ab_tensor_prod_ind_homotopy_quad {A B C D G : AbGroup} Proof. rapply (ab_tensor_prod_ind_hprop_quad (fun _ => _)). - exact H. - - intros x p. - rewrite 2 grp_homo_inv. - exact (ap (-) p). - intros x y p q. rewrite 2 grp_homo_op. - exact (ap011 (+) p q). + rewrite 2 grp_homo_inv. + exact (ap011 (fun x y => x - y) p q). Defined. (** ** Universal Property of the Tensor Product *) diff --git a/theories/Algebra/Groups/FreeGroup.v b/theories/Algebra/Groups/FreeGroup.v index 208ca4e1c95..2e7e01cd2b2 100644 --- a/theories/Algebra/Groups/FreeGroup.v +++ b/theories/Algebra/Groups/FreeGroup.v @@ -373,9 +373,7 @@ Section Reduction. `{forall x, IsHProp (P x)} (H1 : P mon_unit) (Hin : forall x, P (freegroup_in x)) - (Hinv : forall x, P x -> P (- x)) - (Hop : forall x y, P x -> P y -> P (x * y)) - (* (H1 : forall w, P (freegroup_eta w)) *) + (Hop : forall x y, P x -> P y -> P (- x * y)) : forall x, P x. Proof. rapply FreeGroup_ind_hprop'. @@ -384,10 +382,13 @@ Section Reduction. - exact H1. - destruct a as [a|a]. + change (P ((freegroup_in a) * freegroup_eta w)). - by apply Hop. + rewrite <- (grp_inv_inv a). + apply Hop. + * rewrite <- grp_unit_r. + by apply Hop. + * assumption. + change (P (-(freegroup_in a) * freegroup_eta w)). - apply Hop; trivial. - by apply Hinv. + by apply Hop. Defined. End Reduction. diff --git a/theories/Algebra/Groups/QuotientGroup.v b/theories/Algebra/Groups/QuotientGroup.v index 1e25c49df94..dd2632d2bbf 100644 --- a/theories/Algebra/Groups/QuotientGroup.v +++ b/theories/Algebra/Groups/QuotientGroup.v @@ -163,6 +163,15 @@ Section QuotientGroup. apply grp_homo_op. Defined. + Definition grp_quotient_ind_hprop (P : QuotientGroup -> Type) + `{forall x, IsHProp (P x)} + (H1 : forall x, P (grp_quotient_map x)) + : forall x, P x. + Proof. + srapply Quotient_ind_hprop. + exact H1. + Defined. + End QuotientGroup. Arguments grp_quotient_map {_ _}. From b63352a288729314679d0a815fb5cd8e4419f44d Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sat, 13 Jul 2024 17:30:22 +0200 Subject: [PATCH 11/44] remove unneeded lemma Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/Abelianization.v | 7 ------- 1 file changed, 7 deletions(-) diff --git a/theories/Algebra/AbGroups/Abelianization.v b/theories/Algebra/AbGroups/Abelianization.v index 94c7245cd6a..29ceb00b7c4 100644 --- a/theories/Algebra/AbGroups/Abelianization.v +++ b/theories/Algebra/AbGroups/Abelianization.v @@ -283,13 +283,6 @@ Section AbelGroup. Proof. by unfold IsSemiGroupPreserving. Defined. - - Global Instance ismonoidpreserving_abel_in : IsMonoidPreserving abel_in. - Proof. - split. - 1: exact _. - reflexivity. - Defined. End AbelGroup. From 5dee8c1753f11d7f5e62b2e892213ce8ad905d3b Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sat, 13 Jul 2024 17:53:22 +0200 Subject: [PATCH 12/44] small simplifications Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/AbelianGroup.v | 6 ++++ theories/Algebra/AbGroups/TensorProduct.v | 38 +++++++---------------- theories/Algebra/Groups/Subgroup.v | 8 +++++ 3 files changed, 26 insertions(+), 26 deletions(-) diff --git a/theories/Algebra/AbGroups/AbelianGroup.v b/theories/Algebra/AbGroups/AbelianGroup.v index 3b9cc0bd8e8..3ec1e8dd535 100644 --- a/theories/Algebra/AbGroups/AbelianGroup.v +++ b/theories/Algebra/AbGroups/AbelianGroup.v @@ -38,6 +38,12 @@ Global Instance negate_abgroup (A : AbGroup) : Negate A := group_inverse. Definition ab_comm {A : AbGroup} (x y : A) : x + y = y + x := commutativity x y. +Definition ab_neg_op {A : AbGroup} (x y : A) : - (x + y) = -x - y. +Proof. + lhs nrapply grp_inv_op. + apply ab_comm. +Defined. + (** ** Paths between abelian groups *) Definition equiv_path_abgroup `{Univalence} {A B : AbGroup@{u}} diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index b8b1227eadb..95c237e1c74 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -27,12 +27,12 @@ Proof. snrapply subgroup_generated. intros x. refine ((exists (a1 a2 : A) (b : B), _) + exists (a : A) (b1 b2 : B), _)%type. - - refine (_ - _ - _ = x). + - refine (_ - (_ + _) = x). 1-3: apply freeabgroup_in. + exact (a1 + a2, b). + exact (a1, b). + exact (a2, b). - - refine (_ - _ - _ = x). + - refine (_ - (_ + _) = x). 1-3: apply freeabgroup_in. + exact (a, b1 + b2). + exact (a, b1). @@ -56,13 +56,9 @@ Definition tensor_dist_l {A B : AbGroup} (a : A) (b b' : B) : tensor a (b + b') = tensor a b + tensor a b'. Proof. apply qglue, tr. - rewrite <- grp_inv_inv. - apply sgt_inv. - rewrite 2 grp_inv_op. + apply sgt_inv'. + rewrite ab_neg_op. rewrite grp_inv_inv. - rewrite (commutativity (- _)). - rewrite commutativity. - rewrite simple_associativity. apply sgt_in. right. by exists a, b, b'. @@ -73,13 +69,9 @@ Definition tensor_dist_r {A B : AbGroup} (a a' : A) (b : B) : tensor (a + a') b = tensor a b + tensor a' b. Proof. apply qglue, tr. - rewrite <- grp_inv_inv. - apply sgt_inv. - rewrite 2 grp_inv_op. + apply sgt_inv'. + rewrite ab_neg_op. rewrite grp_inv_inv. - rewrite (commutativity (- _)). - rewrite commutativity. - rewrite simple_associativity. apply sgt_in. left. by exists a, a', b. @@ -175,26 +167,20 @@ Proof. | | ? ? ? H1 ? H2 ]. + destruct p. - rewrite 2 grp_homo_op. - rewrite 2 grp_homo_inv. + rewrite grp_homo_op. + rewrite grp_homo_inv. apply grp_moveL_1M^-1%equiv. - apply grp_moveL_gM^-1%equiv. unfold freeabgroup_in. change (grp_homo_abel_rec ?f (abel_unit ?x)) with (f x). - simpl. - rewrite 3 grp_unit_r. - rhs rapply abgroup_commutative. + simpl; rewrite 2 grp_unit_r. apply r. + destruct p. - rewrite 2 grp_homo_op. - rewrite 2 grp_homo_inv. + rewrite grp_homo_op. + rewrite grp_homo_inv. apply grp_moveL_1M^-1%equiv. - apply grp_moveL_gM^-1%equiv. unfold freeabgroup_in. change (grp_homo_abel_rec ?f (abel_unit ?x)) with (f x). - simpl. - rewrite 3 grp_unit_r. - rhs rapply abgroup_commutative. + simpl; rewrite 2 grp_unit_r. apply l. + nrapply grp_homo_unit. + rewrite grp_homo_op, grp_homo_inv. diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v index 259cefa77b6..985c254698c 100644 --- a/theories/Algebra/Groups/Subgroup.v +++ b/theories/Algebra/Groups/Subgroup.v @@ -453,6 +453,14 @@ Proof. exact (sgt_op sgt_unit p). Defined. +Definition sgt_inv' {G : Group} {X} {g : G} + : subgroup_generated_type X (- g) -> subgroup_generated_type X g. +Proof. + intros p. + rewrite <- grp_inv_inv. + by apply sgt_inv. +Defined. + Definition sgt_op' {G : Group} {X} {g h : G} : subgroup_generated_type X g -> subgroup_generated_type X h From 8b88d031d14d79f934f51d9d6dfd39a9775f6916 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sat, 13 Jul 2024 18:18:07 +0200 Subject: [PATCH 13/44] simplify induction hypothesis to + Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/TensorProduct.v | 45 +++++++++++++++-------- 1 file changed, 30 insertions(+), 15 deletions(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index 95c237e1c74..2bb904e984c 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -209,7 +209,7 @@ Definition ab_tensor_prod_ind_hprop {A B : AbGroup} (P : ab_tensor_prod A B -> Type) {H : forall x, IsHProp (P x)} (H2 : forall a b, P (tensor a b)) - (H4 : forall x y, P x -> P y -> P (x - y)) + (H4 : forall x y, P x -> P y -> P (x + y)) : forall x, P x. Proof. assert (Hzero : P 0) by exact (transport P (tensor_zero_l 0) (H2 0 0)). @@ -224,7 +224,30 @@ Proof. change (P (grp_quotient_map (abel_unit (-x + y)))). rewrite grp_homo_op, ab_comm, grp_homo_op. rewrite 2 grp_homo_inv. - by apply H4. + apply H4; trivial. + clear y Hy. + clear Hx. + revert x. + srapply FreeGroup_ind_hprop'; intros w; hnf. + induction w. + + rewrite grp_homo_unit. + rewrite grp_inv_unit. + exact Hzero. + + destruct a as [[a b]|[a b]]. + * change (P (- grp_quotient_map (abel_unit (freegroup_in (a, b) + freegroup_eta w)))). + rewrite 2 grp_homo_op. + rewrite grp_inv_op. + apply H4; trivial. + change (P (- tensor a b)). + rewrite <- tensor_neg_l. + apply H2. + * change (P (- grp_quotient_map (abel_unit (- freegroup_in (a, b) + freegroup_eta w)))). + rewrite 2 grp_homo_op. + rewrite 2 grp_homo_inv. + rewrite grp_inv_op. + rewrite grp_inv_inv. + apply H4; trivial. + apply H2. Defined. (** As a commonly occuring special case of the above induction principle, we have the case when the predicate in question is showing two group homomorphisms are homotopic. In order to do this, it suffices to show it only for elementary tensors. The homotopy is closed under all the group operations so we don't need to hypthesise anything else. *) @@ -237,10 +260,7 @@ Proof. - exact H. - intros x y p q. rewrite 2 grp_homo_op. - nrefine (ap011 (+) p _). - rhs nrapply grp_homo_inv. - lhs nrapply grp_homo_inv. - exact (ap (-) q). + nrefine (ap011 (+) p q). Defined. (** As an even more specialised case, we occasionally have the second homomorphism being a sum of abelian group homomorphisms. In those cases, it is easier to give this specialised lemma. *) @@ -255,7 +275,7 @@ Definition ab_tensor_prod_ind_hprop_triple {A B C : AbGroup} (P : ab_tensor_prod A (ab_tensor_prod B C) -> Type) (H : forall x, IsHProp (P x)) (Hin : forall a b c, P (tensor a (tensor b c))) - (Hop : forall x y, P x -> P y -> P (x - y)) + (Hop : forall x y, P x -> P y -> P (x + y)) : forall x, P x. Proof. rapply (ab_tensor_prod_ind_hprop P). @@ -264,7 +284,6 @@ Proof. + nrapply Hin. + intros x y Hx Hy. rewrite tensor_dist_l. - rewrite tensor_neg_r. by apply Hop. - exact Hop. Defined. @@ -281,10 +300,8 @@ Proof. - exact (H a). - intros x y p q. rewrite tensor_dist_l. - rewrite tensor_neg_r. rewrite 2 grp_homo_op. - rewrite 2 grp_homo_inv. - exact (ap011 (fun x y => x - y) p q). + exact (ap011 (+) p q). Defined. (** As explained for the bilinear and trilinear cases, we also derive an induction principle for quadruple tensors giving us dependent quadrilinear maps. *) @@ -292,7 +309,7 @@ Definition ab_tensor_prod_ind_hprop_quad {A B C D : AbGroup} (P : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) -> Type) (H : forall x, IsHProp (P x)) (Hin : forall a b c d, P (tensor a (tensor b (tensor c d)))) - (Hop : forall x y, P x -> P y -> P (x - y)) + (Hop : forall x y, P x -> P y -> P (x + y)) : forall x, P x. Proof. rapply (ab_tensor_prod_ind_hprop P). @@ -301,7 +318,6 @@ Proof. + nrapply Hin. + intros x y Hx Hy. rewrite tensor_dist_l. - rewrite tensor_neg_r. by apply Hop. - exact Hop. Defined. @@ -317,8 +333,7 @@ Proof. - exact H. - intros x y p q. rewrite 2 grp_homo_op. - rewrite 2 grp_homo_inv. - exact (ap011 (fun x y => x - y) p q). + exact (ap011 (+) p q). Defined. (** ** Universal Property of the Tensor Product *) From 08a26b1dd911f3821fa628db13d4fed48b9fb44c Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sat, 13 Jul 2024 18:25:50 +0200 Subject: [PATCH 14/44] cleanup names Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/TensorProduct.v | 18 +++++++++--------- theories/Algebra/Groups/FreeGroup.v | 2 +- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index 2bb904e984c..dbfdac98ec8 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -208,23 +208,23 @@ The hprop induction principle therefore requires that the codomain is a hprop in Definition ab_tensor_prod_ind_hprop {A B : AbGroup} (P : ab_tensor_prod A B -> Type) {H : forall x, IsHProp (P x)} - (H2 : forall a b, P (tensor a b)) - (H4 : forall x y, P x -> P y -> P (x + y)) + (Hin : forall a b, P (tensor a b)) + (Hop : forall x y, P x -> P y -> P (x + y)) : forall x, P x. Proof. - assert (Hzero : P 0) by exact (transport P (tensor_zero_l 0) (H2 0 0)). + assert (Hzero : P 0) by exact (transport P (tensor_zero_l 0) (Hin 0 0)). unfold ab_tensor_prod. srapply grp_quotient_ind_hprop. srapply Abel_ind_hprop; cbn beta. srapply FreeGroup_ind_hprop; cbn beta. - exact Hzero. - intros [a b]. - apply H2. + apply Hin. - intros x y Hx Hy. change (P (grp_quotient_map (abel_unit (-x + y)))). rewrite grp_homo_op, ab_comm, grp_homo_op. rewrite 2 grp_homo_inv. - apply H4; trivial. + apply Hop; trivial. clear y Hy. clear Hx. revert x. @@ -237,17 +237,17 @@ Proof. * change (P (- grp_quotient_map (abel_unit (freegroup_in (a, b) + freegroup_eta w)))). rewrite 2 grp_homo_op. rewrite grp_inv_op. - apply H4; trivial. + apply Hop; trivial. change (P (- tensor a b)). rewrite <- tensor_neg_l. - apply H2. + apply Hin. * change (P (- grp_quotient_map (abel_unit (- freegroup_in (a, b) + freegroup_eta w)))). rewrite 2 grp_homo_op. rewrite 2 grp_homo_inv. rewrite grp_inv_op. rewrite grp_inv_inv. - apply H4; trivial. - apply H2. + apply Hop; trivial. + apply Hin. Defined. (** As a commonly occuring special case of the above induction principle, we have the case when the predicate in question is showing two group homomorphisms are homotopic. In order to do this, it suffices to show it only for elementary tensors. The homotopy is closed under all the group operations so we don't need to hypthesise anything else. *) diff --git a/theories/Algebra/Groups/FreeGroup.v b/theories/Algebra/Groups/FreeGroup.v index 2e7e01cd2b2..887c2c13121 100644 --- a/theories/Algebra/Groups/FreeGroup.v +++ b/theories/Algebra/Groups/FreeGroup.v @@ -368,7 +368,7 @@ Section Reduction. - exact H1. - intro; apply path_ishprop. Defined. - + Definition FreeGroup_ind_hprop (P : FreeGroup -> Type) `{forall x, IsHProp (P x)} (H1 : P mon_unit) From edc74faa02394770e78d6981401d26c15155e34e Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Sat, 13 Jul 2024 13:35:02 -0400 Subject: [PATCH 15/44] TensorProduct: simplify proof of induction principle --- theories/Algebra/AbGroups/TensorProduct.v | 49 ++++++++--------------- 1 file changed, 16 insertions(+), 33 deletions(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index dbfdac98ec8..d529bcc157a 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -212,42 +212,25 @@ Definition ab_tensor_prod_ind_hprop {A B : AbGroup} (Hop : forall x y, P x -> P y -> P (x + y)) : forall x, P x. Proof. - assert (Hzero : P 0) by exact (transport P (tensor_zero_l 0) (Hin 0 0)). unfold ab_tensor_prod. srapply grp_quotient_ind_hprop. srapply Abel_ind_hprop; cbn beta. - srapply FreeGroup_ind_hprop; cbn beta. - - exact Hzero. - - intros [a b]. - apply Hin. - - intros x y Hx Hy. - change (P (grp_quotient_map (abel_unit (-x + y)))). - rewrite grp_homo_op, ab_comm, grp_homo_op. - rewrite 2 grp_homo_inv. - apply Hop; trivial. - clear y Hy. - clear Hx. - revert x. - srapply FreeGroup_ind_hprop'; intros w; hnf. - induction w. - + rewrite grp_homo_unit. - rewrite grp_inv_unit. - exact Hzero. - + destruct a as [[a b]|[a b]]. - * change (P (- grp_quotient_map (abel_unit (freegroup_in (a, b) + freegroup_eta w)))). - rewrite 2 grp_homo_op. - rewrite grp_inv_op. - apply Hop; trivial. - change (P (- tensor a b)). - rewrite <- tensor_neg_l. - apply Hin. - * change (P (- grp_quotient_map (abel_unit (- freegroup_in (a, b) + freegroup_eta w)))). - rewrite 2 grp_homo_op. - rewrite 2 grp_homo_inv. - rewrite grp_inv_op. - rewrite grp_inv_inv. - apply Hop; trivial. - apply Hin. + srapply FreeGroup_ind_hprop'; intros w; cbn beta. + induction w. + - exact (transport P (tensor_zero_l 0) (Hin 0 0)). + - destruct a as [[a b]|[a b]]. + + change (P (grp_quotient_map (abel_unit (freegroup_in (a, b) + freegroup_eta w)))). + (* Both [rewrite]s are [reflexivity], but the Defined is slow if [change] is used instead. *) + rewrite 2 grp_homo_op. + apply Hop; trivial. + apply Hin. + + change (P (grp_quotient_map (abel_unit (- freegroup_in (a, b) + freegroup_eta w)))). + (* The [rewrite]s on the next two lines are all reflexivity. *) + rewrite 2 grp_homo_op. + rewrite 2 grp_homo_inv. + apply Hop; trivial. + rewrite <- tensor_neg_l. + apply Hin. Defined. (** As a commonly occuring special case of the above induction principle, we have the case when the predicate in question is showing two group homomorphisms are homotopic. In order to do this, it suffices to show it only for elementary tensors. The homotopy is closed under all the group operations so we don't need to hypthesise anything else. *) From 9373e4d769c67edf773845497aea383e766ce6d4 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sat, 13 Jul 2024 19:44:46 +0200 Subject: [PATCH 16/44] fix typo Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/TensorProduct.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index d529bcc157a..5af193177ef 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -39,7 +39,7 @@ Proof. + exact (a, b2). Defined. -(** The tesnor product [ab_tensor_prod A B] of two abelian groups [A] and [B] is defined to ba a quotient of the free abelian group on pairs of elements [A * B] by the subgroup of bilinear pairs. *) +(** The tensor product [ab_tensor_prod A B] of two abelian groups [A] and [B] is defined to ba a quotient of the free abelian group on pairs of elements [A * B] by the subgroup of bilinear pairs. *) Definition ab_tensor_prod (A B : AbGroup) : AbGroup := QuotientAbGroup (FreeAbGroup (A * B)) subgroup_bilinear_pairs. From baa3a89a979a50f1f3a274d4eb2771de86e83c9f Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Sat, 13 Jul 2024 14:35:58 -0400 Subject: [PATCH 17/44] TensorProduct: update comments --- theories/Algebra/AbGroups/TensorProduct.v | 38 ++++++++++------------- 1 file changed, 17 insertions(+), 21 deletions(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index 5af193177ef..802e61fb89c 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -43,13 +43,13 @@ Defined. Definition ab_tensor_prod (A B : AbGroup) : AbGroup := QuotientAbGroup (FreeAbGroup (A * B)) subgroup_bilinear_pairs. -(** The tensor product of [A] and [B] contains formal combinations of pairs of elements from [A] and [B]. We denote these pairs as elementary tensors and name them [tensor]. *) +(** The tensor product of [A] and [B] contains formal combinations of pairs of elements from [A] and [B]. We denote these pairs as simple tensors and name them [tensor]. *) Definition tensor {A B : AbGroup} : A -> B -> ab_tensor_prod A B := fun a b => grp_quotient_map (freeabgroup_in (a, b)). (** ** Properties of tensors *) -(** The characterizing property of elementary tensors are that they are bilinear in their arguments. *) +(** The characterizing property of simple tensors are that they are bilinear in their arguments. *) (** A [tensor] of a sum distributes over the sum on the left. *) Definition tensor_dist_l {A B : AbGroup} (a : A) (b b' : B) @@ -148,7 +148,7 @@ Defined. (** Here we write down some induction principles to help us prove lemmas about the tensor product. Some of these are quite specialised but are patterns that appear often in practice. *) -(** Our main recursion principle states that in order to build a map out of the tensor product, it is sufficient to provide a map out of the direct product which is bilinear, that is, a map that preserves addition in both arguments of the product. *) +(** Our main recursion principle states that in order to build a homomorphism out of the tensor product, it is sufficient to provide a map out of the direct product which is bilinear, that is, a map that preserves addition in both arguments of the product. *) Definition ab_tensor_prod_rec {A B C : AbGroup} (f : A -> B -> C) (l : forall a b b', f a (b + b') = f a b + f a b') @@ -188,7 +188,7 @@ Proof. exact(H1 @ H2^). Defined. -(** Since we defined [ab_tensor_prod_rec] using the recursors of the underlying type, we get an annoying artifact of [x + 0] instead of [x] when acting on elementary tensors. Typically in an argument we want our recursor to act on elementary tensors without the extra [0] and this lemma makes sure of that. *) +(** Since we defined [ab_tensor_prod_rec] using the recursors of the underlying type, we get an annoying artifact of [x + 0] instead of [x] when acting on simple tensors. Typically in an argument we want our recursor to act on simple tensors without the extra [0] and this lemma makes sure of that. *) Definition ab_tensor_prod_rec_beta_tensor {A B C : AbGroup} (f : A -> B -> C) (l : forall a b b', f a (b + b') = f a b + f a b') @@ -200,11 +200,7 @@ Proof. apply grp_unit_r. Defined. -(** The induction principle is a little different to the recursor. In the recursor, which is the non-dependent case of the induction principle, we were landing in an abelian group hence the codomain came equipped with the group operations which we wish to preserve with the bilinearity conditions. - -The induction principle will require these bilinearity conditions, but we have to postulate the data of a "dependent group" in the codomain in order to state these properly. In general, we don't have any use for a general induction principle into a hset and so we can drop these dependent bilinearity paths. - -The hprop induction principle therefore requires that the codomain is a hprop in addition to being closed under the various group operations of the domain. Most importantly we hypothesise that we can prove a property on an elementary tensor [tensor a b]. *) +(** We give an induction principle for an hprop-valued type family [P]. It may be surprising at first that we only require [P] to hold for the simple tensors [tensor a b] and be closed under addition. It automatically follows that [P 0] holds (since [tensor 0 0 = 0]) and that [P] is closed under negation (since [tensor -a b = - tensor a b]). This induction principle says that the simple tensors generate the tensor product as a semigroup. *) Definition ab_tensor_prod_ind_hprop {A B : AbGroup} (P : ab_tensor_prod A B -> Type) {H : forall x, IsHProp (P x)} @@ -220,7 +216,7 @@ Proof. - exact (transport P (tensor_zero_l 0) (Hin 0 0)). - destruct a as [[a b]|[a b]]. + change (P (grp_quotient_map (abel_unit (freegroup_in (a, b) + freegroup_eta w)))). - (* Both [rewrite]s are [reflexivity], but the Defined is slow if [change] is used instead. *) + (* Both [rewrite]s are [reflexivity], but the [Defined] is slow if [change] is used instead. *) rewrite 2 grp_homo_op. apply Hop; trivial. apply Hin. @@ -233,7 +229,7 @@ Proof. apply Hin. Defined. -(** As a commonly occuring special case of the above induction principle, we have the case when the predicate in question is showing two group homomorphisms are homotopic. In order to do this, it suffices to show it only for elementary tensors. The homotopy is closed under all the group operations so we don't need to hypthesise anything else. *) +(** As a commonly occuring special case of the above induction principle, we have the case when the predicate in question is showing that two group homomorphisms out of the tensor product are homotopic. In order to do this, it suffices to show it only for simple tensors. The homotopy is closed under addition, so we don't need to hypothesise anything else. *) Definition ab_tensor_prod_ind_homotopy {A B G : AbGroup} {f f' : ab_tensor_prod A B $-> G} (H : forall a b, f (tensor a b) = f' (tensor a b)) @@ -246,14 +242,14 @@ Proof. nrefine (ap011 (+) p q). Defined. -(** As an even more specialised case, we occasionally have the second homomorphism being a sum of abelian group homomorphisms. In those cases, it is easier to give this specialised lemma. *) +(** As an even more specialised case, we occasionally have the second homomorphism being a sum of abelian group homomorphisms. In those cases, it is easier to use this specialised lemma. *) Definition ab_tensor_prod_ind_homotopy_plus {A B G : AbGroup} {f f' f'' : ab_tensor_prod A B $-> G} (H : forall a b, f (tensor a b) = f' (tensor a b) + f'' (tensor a b)) : forall x, f x = f' x + f'' x := ab_tensor_prod_ind_homotopy (f':=ab_homo_add f' f'') H. -(** Here we give an induction principle for a triple tensor, a.k.a a dependent trilinear function. As before we need a "dependent group" as the codomain but we may now assume a "triple elmentary tensor" as a hypothesis. *) +(** Here we give an induction principle for a triple tensor, a.k.a a dependent trilinear function. *) Definition ab_tensor_prod_ind_hprop_triple {A B C : AbGroup} (P : ab_tensor_prod A (ab_tensor_prod B C) -> Type) (H : forall x, IsHProp (P x)) @@ -305,7 +301,7 @@ Proof. - exact Hop. Defined. -(** To construct a homotopy between quadrilinear maps we need only check equality for the quadruple elementary tensor. *) +(** To construct a homotopy between quadrilinear maps we need only check equality for the quadruple simple tensors. *) Definition ab_tensor_prod_ind_homotopy_quad {A B C D G : AbGroup} {f f' : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) $-> G} (H : forall a b c d, f (tensor a (tensor b (tensor c d))) @@ -344,7 +340,7 @@ Proof. exact _. Defined. -(** The elementary tensor map is biadditive. *) +(** The simple tensor map is biadditive. *) Global Instance isbiadditive_tensor (A B : AbGroup) : IsBiadditive (@tensor A B) := {| isbiadditive_l := fun b a a' => tensor_dist_r a a' b; @@ -410,7 +406,7 @@ Proof. by rewrite tensor_dist_r. Defined. -(** The tensor product functor acts on elementary tensors by mapping each component. *) +(** The tensor product functor acts on simple tensors by mapping each component. *) Definition functor_ab_tensor_prod_beta_tensor {A B A' B' : AbGroup} (f : A $-> A') (g : B $-> B') (a : A) (b : B) : functor_ab_tensor_prod f g (tensor a b) = tensor (f a) (g b). @@ -478,7 +474,7 @@ Defined. (** The tensor product is symmetric in that the order in which we take the tensor shouldn't matter upto isomorphism. *) -(** We can define a swap map which swaps the order of elementary tensors. *) +(** We can define a swap map which swaps the order of simple tensors. *) Definition ab_tensor_swap {A B} : ab_tensor_prod A B $-> ab_tensor_prod B A. Proof. snrapply ab_tensor_prod_rec. @@ -557,7 +553,7 @@ Proof. by rewrite tensor_dist_r, tensor_dist_l. Defined. -(** The twist map acts in the expected way on elementary tensors. *) +(** The twist map acts in the expected way on simple tensors. *) Definition ab_tensor_prod_twist_beta_tensor_tensor {A B C} a b c : @ab_tensor_prod_twist A B C (tensor a (tensor b c)) = tensor b (tensor a c). Proof. @@ -719,7 +715,7 @@ Proof. intros A B. snrapply ab_tensor_prod_ind_homotopy_triple. intros a b z. - (** Here we have to get the goal into the correct form to be able to reduce the functions on the elementary tensors. *) + (** Here we have to get the goal into the correct form to be able to reduce the functions on the simple tensors. *) (** TODO: work out a way to reduce these change statements. *) change (functor_ab_tensor_prod (Id A) (rightunitor_ab_tensor_prod B) (tensor a (tensor b z)) = ab_tensor_swap (functor_ab_tensor_prod (Id B) @@ -734,7 +730,7 @@ Proof. exact (tensor_grp_pow _ _ _)^. Defined. -(** The hexagon identity is also straighforward to prove. We simply have to reduce all the involved functions on the elementary tensors using our custom triple tensor induction principle. *) +(** The hexagon identity is also straighforward to prove. We simply have to reduce all the involved functions on the simple tensors using our custom triple tensor induction principle. *) Global Instance hexagon_ab_tensor_prod : HexagonIdentity ab_tensor_prod. Proof. snrapply hexagon_twist. @@ -754,7 +750,7 @@ Proof. reflexivity. Defined. -(** Finally, we can prove the pentagon identity using the quadruple tensor induction principle. As we did before, the work only involves reducing the involved functions on the elementary tensor redexes. *) +(** Finally, we can prove the pentagon identity using the quadruple tensor induction principle. As we did before, the work only involves reducing the involved functions on the simple tensor redexes. *) Global Instance pentagon_ab_tensor_prod : PentagonIdentity ab_tensor_prod. Proof. snrapply pentagon_twist. From 920db0c48d49af11824dfc5a9c7b225c2fc77b11 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Sat, 13 Jul 2024 14:36:26 -0400 Subject: [PATCH 18/44] Add grp_homo_op_agree, and use it in many places --- theories/Algebra/AbGroups/Abelianization.v | 3 +-- theories/Algebra/AbGroups/Biproduct.v | 3 +-- theories/Algebra/AbGroups/TensorProduct.v | 21 ++++++--------------- theories/Algebra/AbSES/Pushout.v | 2 +- theories/Algebra/Groups/FreeProduct.v | 4 ++-- theories/Algebra/Groups/Group.v | 10 ++++++++++ theories/Algebra/Groups/GroupCoeq.v | 2 +- theories/Algebra/Groups/GrpPullback.v | 4 +--- 8 files changed, 23 insertions(+), 26 deletions(-) diff --git a/theories/Algebra/AbGroups/Abelianization.v b/theories/Algebra/AbGroups/Abelianization.v index 29ceb00b7c4..d961cca3f7b 100644 --- a/theories/Algebra/AbGroups/Abelianization.v +++ b/theories/Algebra/AbGroups/Abelianization.v @@ -319,8 +319,7 @@ Proof. snrapply Build_GroupHomomorphism. { srapply (Abel_rec _ _ f). intros x y z. - refine (grp_homo_op _ _ _ @ _ @ (grp_homo_op _ _ _)^). - apply (ap (_ *.)). + nrapply grp_homo_op_agree; trivial. refine (grp_homo_op _ _ _ @ _ @ (grp_homo_op _ _ _)^). apply commutativity. } intros y. diff --git a/theories/Algebra/AbGroups/Biproduct.v b/theories/Algebra/AbGroups/Biproduct.v index 536f2785df8..4b4c3b047d5 100644 --- a/theories/Algebra/AbGroups/Biproduct.v +++ b/theories/Algebra/AbGroups/Biproduct.v @@ -191,8 +191,7 @@ Proof. intros h k. intros [a b]. refine (ap f (ab_biprod_decompose _ _) @ _ @ ap g (ab_biprod_decompose _ _)^). - refine (grp_homo_op _ _ _ @ _ @ (grp_homo_op _ _ _)^). - exact (ap011 (+) (h a) (k b)). + exact (grp_homo_op_agree f g (h a) (k b)). Defined. (* Maps out of biproducts are determined on the two inclusions. *) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index 802e61fb89c..768444adcef 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -235,11 +235,9 @@ Definition ab_tensor_prod_ind_homotopy {A B G : AbGroup} (H : forall a b, f (tensor a b) = f' (tensor a b)) : f $== f'. Proof. - rapply (ab_tensor_prod_ind_hprop (fun _ => _)). + rapply ab_tensor_prod_ind_hprop. - exact H. - - intros x y p q. - rewrite 2 grp_homo_op. - nrefine (ap011 (+) p q). + - intros x y; apply grp_homo_op_agree. Defined. (** As an even more specialised case, we occasionally have the second homomorphism being a sum of abelian group homomorphisms. In those cases, it is easier to use this specialised lemma. *) @@ -273,14 +271,9 @@ Definition ab_tensor_prod_ind_homotopy_triple {A B C G : AbGroup} (H : forall a b c, f (tensor a (tensor b c)) = f' (tensor a (tensor b c))) : f $== f'. Proof. - rapply ab_tensor_prod_ind_homotopy. - intros a. - rapply ab_tensor_prod_ind_hprop. - - exact (H a). - - intros x y p q. - rewrite tensor_dist_l. - rewrite 2 grp_homo_op. - exact (ap011 (+) p q). + rapply ab_tensor_prod_ind_hprop_triple. + - exact H. + - intros x y; apply grp_homo_op_agree. Defined. (** As explained for the bilinear and trilinear cases, we also derive an induction principle for quadruple tensors giving us dependent quadrilinear maps. *) @@ -310,9 +303,7 @@ Definition ab_tensor_prod_ind_homotopy_quad {A B C D G : AbGroup} Proof. rapply (ab_tensor_prod_ind_hprop_quad (fun _ => _)). - exact H. - - intros x y p q. - rewrite 2 grp_homo_op. - exact (ap011 (+) p q). + - intros x y; apply grp_homo_op_agree. Defined. (** ** Universal Property of the Tensor Product *) diff --git a/theories/Algebra/AbSES/Pushout.v b/theories/Algebra/AbSES/Pushout.v index 022f02b7979..ea70463902b 100644 --- a/theories/Algebra/AbSES/Pushout.v +++ b/theories/Algebra/AbSES/Pushout.v @@ -85,7 +85,7 @@ Proof. 1: apply issurj_class_of. 2: exact _. intro x; simpl. - refine (grp_homo_op (projection F) _ _ @ ap011 (+) _ _ @ (grp_homo_op _ _ _ )^). + nrapply grp_homo_op_agree. + refine (_ @ (grp_homo_unit _)^). apply iscomplex_abses. + apply right_square. diff --git a/theories/Algebra/Groups/FreeProduct.v b/theories/Algebra/Groups/FreeProduct.v index 7dfc1063fb6..ff9795fdda7 100644 --- a/theories/Algebra/Groups/FreeProduct.v +++ b/theories/Algebra/Groups/FreeProduct.v @@ -732,8 +732,8 @@ Proof. 1: exact (grp_homo_unit _ @ (grp_homo_unit _)^). Local Notation "[ x ]" := (cons x nil). change (f (amal_eta [gh] * amal_eta w) = g (amal_eta [gh] * amal_eta w)). - refine (grp_homo_op _ _ _ @ _ @ (grp_homo_op _ _ _)^). - f_ap; clear IHw w. + nrapply grp_homo_op_agree. + 2: apply IHw. destruct gh as [g' | h]. + exact (p g'). + exact (q h). diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v index 90d7d037e5c..58850792b75 100644 --- a/theories/Algebra/Groups/Group.v +++ b/theories/Algebra/Groups/Group.v @@ -951,3 +951,13 @@ Proof. refine (ap f _). apply C. Defined. + +(** If two group homomorphisms agree on two elements, then they agree on their product. *) +Definition grp_homo_op_agree {G G' H : Group} (f : G $-> H) (f' : G' $-> H) + {x y : G} {x' y' : G'} (p : f x = f' x') (q : f y = f' y') + : f (x * y) = f' (x' * y'). +Proof. + lhs nrapply grp_homo_op. + rhs nrapply grp_homo_op. + exact (ap011 _ p q). +Defined. diff --git a/theories/Algebra/Groups/GroupCoeq.v b/theories/Algebra/Groups/GroupCoeq.v index 92d1d1a8b80..42f009caf9b 100644 --- a/theories/Algebra/Groups/GroupCoeq.v +++ b/theories/Algebra/Groups/GroupCoeq.v @@ -42,7 +42,7 @@ Proof. simpl. destruct a as [a|a]. 1,2: refine (ap _ (grp_homo_op _ _ _) @ _). - 1,2: refine (grp_homo_op _ _ _ @ _ @ (grp_homo_op _ _ _)^); f_ap. + 1,2: nrapply grp_homo_op_agree; trivial. symmetry. apply p. } { intros [k p] x. diff --git a/theories/Algebra/Groups/GrpPullback.v b/theories/Algebra/Groups/GrpPullback.v index c3c3dca73c3..13b19e43bc3 100644 --- a/theories/Algebra/Groups/GrpPullback.v +++ b/theories/Algebra/Groups/GrpPullback.v @@ -16,9 +16,7 @@ Section GrpPullback. Proof. intros [b [c p]] [d [e q]]. refine (b * d; c * e; _). - refine (grp_homo_op f b d @ (_ @ _) @ (grp_homo_op g c e)^). - - exact (ap (fun y:A => f b * y) q). - - exact (ap (fun x:A => x * g e) p). + exact (grp_homo_op_agree _ _ p q). Defined. Local Instance grp_pullback_sgop_associative From ee4daf5da64d2eb37210f4cf8dec03f9cc332ddb Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Sat, 13 Jul 2024 14:55:18 -0400 Subject: [PATCH 19/44] TensorProduct: factor out defn of bilinear pairs to make goals small --- theories/Algebra/AbGroups/TensorProduct.v | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index 768444adcef..5c198552e39 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -20,11 +20,10 @@ Local Open Scope mc_add_scope. (** We define the tensor product of abelian groups as a quotient of the free abelian group on pairs of elements of the two groups by the subgroup generated by the bilinear pairs. *) -(** Here we define the subgroup of bilinear pairs *) -Definition subgroup_bilinear_pairs {A B : AbGroup} - : Subgroup (FreeAbGroup (A * B)). +(** Here we define the subgroup of bilinear pairs in two steps *) +Definition family_bilinear_pairs {A B : AbGroup} + : FreeAbGroup (A * B) -> Type. Proof. - snrapply subgroup_generated. intros x. refine ((exists (a1 a2 : A) (b : B), _) + exists (a : A) (b1 b2 : B), _)%type. - refine (_ - (_ + _) = x). @@ -39,6 +38,10 @@ Proof. + exact (a, b2). Defined. +Definition subgroup_bilinear_pairs {A B : AbGroup} + : Subgroup (FreeAbGroup (A * B)) + := subgroup_generated family_bilinear_pairs. + (** The tensor product [ab_tensor_prod A B] of two abelian groups [A] and [B] is defined to ba a quotient of the free abelian group on pairs of elements [A * B] by the subgroup of bilinear pairs. *) Definition ab_tensor_prod (A B : AbGroup) : AbGroup := QuotientAbGroup (FreeAbGroup (A * B)) subgroup_bilinear_pairs. From 4758acc89cc719e6383c42adb8447978c00158f3 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Tue, 16 Jul 2024 14:38:55 -0400 Subject: [PATCH 20/44] Simplifications involving grp_pow and ab_mul --- theories/Algebra/AbGroups/TensorProduct.v | 59 +++++++---------------- theories/Algebra/AbGroups/Z.v | 41 ++++------------ theories/Algebra/Groups/Group.v | 48 ++++++++++++------ 3 files changed, 60 insertions(+), 88 deletions(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index 5c198552e39..95f0020f69a 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -587,52 +587,28 @@ Defined. (** First we characterise the action of integers via [grp_pow] and their interaction on tensors. This is just a generalisation of the distributivity laws for tensors. *) (** Multiplication in the first factor can be factored out. *) -Definition tensor_grp_pow_l {A B : AbGroup} (z : Int) (a : A) (b : B) - : tensor (grp_pow a z) b = grp_pow (tensor a b) z. -Proof. - induction z as [|z IHz|z IHz]. - - nrapply tensor_zero_l. - - rewrite 2 grp_pow_succ. - lhs nrapply tensor_dist_r. - nrapply ap. - exact IHz. - - rewrite 2 grp_pow_pred. - lhs nrapply tensor_dist_r. - snrapply ap011. - + nrapply tensor_neg_l. - + exact IHz. -Defined. +Definition tensor_ab_mul_l {A B : AbGroup} (z : Int) (a : A) (b : B) + : tensor (ab_mul z a) b = ab_mul z (tensor a b) + := ab_mul_natural (grp_homo_tensor_r b) z a. (** Multiplication in the second factor can be factored out. *) -Definition tensor_grp_pow_r {A B : AbGroup} (z : Int) (a : A) (b : B) - : tensor a (grp_pow b z) = grp_pow (tensor a b) z. -Proof. - induction z as [|z IHz|z IHz]. - - nrapply tensor_zero_r. - - rewrite 2 grp_pow_succ. - lhs nrapply tensor_dist_l. - nrapply ap. - exact IHz. - - rewrite 2 grp_pow_pred. - lhs nrapply tensor_dist_l. - snrapply ap011. - + nrapply tensor_neg_r. - + exact IHz. -Defined. +Definition tensor_ab_mul_r {A B : AbGroup} (z : Int) (a : A) (b : B) + : tensor a (ab_mul z b) = ab_mul z (tensor a b) + := ab_mul_natural (grp_homo_tensor_l a) z b. (** Multiplication can be transferred from one factor to the other. The tensor product of [R]-modules will include this as an extra axiom, but here we have [Z]-modules and we can prove it. *) -Definition tensor_grp_pow {A B : AbGroup} (z : Int) (a : A) (b : B) - : tensor (grp_pow a z) b = tensor a (grp_pow b z). +Definition tensor_ab_mul {A B : AbGroup} (z : Int) (a : A) (b : B) + : tensor (ab_mul z a) b = tensor a (ab_mul z b). Proof. - rhs nrapply tensor_grp_pow_r. - nrapply tensor_grp_pow_l. + rhs nrapply tensor_ab_mul_r. + nrapply tensor_ab_mul_l. Defined. (** [abgroup_Z] is a right identity for the tensor product. *) Definition ab_tensor_prod_Z_r {A} : ab_tensor_prod A abgroup_Z $<~> A. Proof. - (** Checking the inverse map is a homomorphism is easier. *) + (** Checking that the inverse map is a homomorphism is easier. *) symmetry. snrapply Build_GroupIsomorphism. - nrapply grp_homo_tensor_r. @@ -640,10 +616,10 @@ Proof. - snrapply isequiv_adjointify. + snrapply ab_tensor_prod_rec. * exact grp_pow_homo. - * intros a z z'; cbn beta; unfold uncurry, fst, snd. + * intros a z z'; cbn beta. nrapply grp_homo_op. - * intros a a' z; cbn beta; unfold uncurry, fst, snd. - nrapply grp_pow_plus. + * intros a a' z; cbn beta. + apply (grp_homo_op (ab_mul z)). + hnf. change (forall x : ?A, (grp_homo_map _ _ ?f) ((grp_homo_map _ _ ?g) x) = x) with (f $o g $== Id _). @@ -652,9 +628,10 @@ Proof. lhs nrapply (ap (grp_homo_tensor_r _)). 1: apply ab_tensor_prod_rec_beta_tensor. change (tensor (B:=abgroup_Z) (grp_pow a z) 1%int = tensor a z). - lhs nrapply tensor_grp_pow. + lhs nrapply tensor_ab_mul. nrapply ap. - apply abgroup_Z_grp_pow_1. + lhs nrapply abgroup_Z_ab_mul. + apply int_mul_1_r. + hnf. intros x. lhs nrapply ab_tensor_prod_rec_beta_tensor. @@ -721,7 +698,7 @@ Proof. 1: rapply ab_tensor_prod_rec_beta_tensor. rhs nrapply (ap (fun x => tensor x _)). 2: rapply ab_tensor_prod_rec_beta_tensor. - exact (tensor_grp_pow _ _ _)^. + exact (tensor_ab_mul _ _ _)^. Defined. (** The hexagon identity is also straighforward to prove. We simply have to reduce all the involved functions on the simple tensors using our custom triple tensor induction principle. *) diff --git a/theories/Algebra/AbGroups/Z.v b/theories/Algebra/AbGroups/Z.v index e500b7e38a4..c8a31d9eec2 100644 --- a/theories/Algebra/AbGroups/Z.v +++ b/theories/Algebra/AbGroups/Z.v @@ -22,7 +22,7 @@ Proof. - exact int_add_comm. Defined. -(** For every group [G] and element [g : G], the map sending an integer to that power of [g] is a homomorphism. *) +(** For every group [G] and element [g : G], the map sending an integer to that power of [g] is a homomorphism. See [ab_mul] for the homomorphism [G -> G] when [G] is abelian. *) Definition grp_pow_homo {G : Group} (g : G) : GroupHomomorphism abgroup_Z G. Proof. @@ -33,39 +33,18 @@ Defined. Local Open Scope mc_add_scope. -(** For every abelian group [A], [grp_pow] distributes over the group operation. *) -Definition grp_pow_plus {A : AbGroup} (a a' : A) (z : Int) - : grp_pow (a + a') z = grp_pow a z + grp_pow a' z. -Proof. - induction z. - - symmetry; apply grp_unit_l. - - rewrite 3 grp_pow_succ. - rewrite <- 2 grp_assoc. - nrapply (ap (a +)). - rewrite (ab_comm (grp_pow a n)). - rewrite <- grp_assoc. - nrapply (ap (a' +)). - rhs nrapply ab_comm. - exact IHz. - - rewrite 3 grp_pow_pred. - rewrite grp_inv_op. - rewrite (ab_comm (negate a')). - rewrite <- 2 grp_assoc. - nrapply (ap (_ +)). - rewrite grp_assoc. - rewrite (ab_comm (grp_pow _ _)). - rewrite <- grp_assoc. - nrapply (ap (_ +)). - exact IHz. -Defined. - -Definition abgroup_Z_grp_pow_1 (z : Int) - : grp_pow (G:=abgroup_Z) 1%int z = z. +(** [ab_mul] (and [grp_pow]) give multiplication in [abgroup_Z]. *) +Definition abgroup_Z_ab_mul (z z' : Int) + : ab_mul (A:=abgroup_Z) z z' = z * z'. Proof. induction z. - reflexivity. - - rewrite grp_pow_succ. + - cbn. + lhs nrapply (grp_pow_succ (G:=abgroup_Z)). + rhs nrapply int_mul_succ_l. f_ap. - - rewrite grp_pow_pred. + - cbn. + lhs nrapply (grp_pow_pred (G:=abgroup_Z)). + rhs nrapply int_mul_pred_l. f_ap. Defined. diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v index 58850792b75..9fa2b81ff0b 100644 --- a/theories/Algebra/Groups/Group.v +++ b/theories/Algebra/Groups/Group.v @@ -474,6 +474,29 @@ Section GroupMovement. End GroupMovement. +(** ** Commutation *) + +(** If [g] commutes with [h], then [g] commutes with the inverse [-h]. *) +Definition grp_commutes_inv {G : Group} (g h : G) (p : g * h = h * g) + : g * (-h) = (-h) * g. +Proof. + apply grp_moveR_gV. + rhs_V apply simple_associativity. + by apply grp_moveL_Vg. +Defined. + +(** If [g] commutes with [h] and [h'], then [g] commutes with their product [h * h']. *) +Definition grp_commutes_op {G : Group} (g h h' : G) + (p : g * h = h * g) (p' : g * h' = h' * g) + : g * (h * h') = (h * h') * g. +Proof. + lhs apply simple_associativity. + lhs nrapply (ap (.* h') p). + lhs_V apply simple_associativity. + lhs nrapply (ap (h *.) p'). + by apply simple_associativity. +Defined. + (** ** Power operation *) (** For a given [g : G] we can define the function [Int -> G] sending an integer to that power of [g]. *) @@ -535,31 +558,24 @@ Proof. - reflexivity. Defined. -(** [grp_pow g n] commutes with [h] if [g] commutes with [h]. *) +(** If [h] commutes with [g], then [h] commutes with [grp_pow g n]. *) Definition grp_pow_commutes {G : Group} (n : Int) (g h : G) - (p : g * h = h * g) - : (grp_pow g n) * h = h * (grp_pow g n). + (p : h * g = g * h) + : h * (grp_pow g n) = (grp_pow g n) * h. Proof. induction n. - - exact (grp_unit_l _ @ (grp_unit_r _)^). + - exact (grp_unit_r _ @ (grp_unit_l _)^). - rewrite grp_pow_succ. - rewrite <- simple_associativity. - rewrite IHn. - rewrite 2 simple_associativity. - f_ap. + nrapply grp_commutes_op; assumption. - rewrite grp_pow_pred. - rewrite <- simple_associativity. - rewrite IHn. - rewrite 2 simple_associativity. - f_ap. - apply grp_moveL_gV. - rewrite <- simple_associativity. - by apply grp_moveR_Vg. + nrapply grp_commutes_op. + 2: assumption. + apply grp_commutes_inv, p. Defined. (** [grp_pow g n] commutes with [g]. *) Definition grp_pow_commutes' {G : Group} (n : Int) (g : G) - : grp_pow g n * g = g * grp_pow g n. + : g * grp_pow g n = grp_pow g n * g. Proof. by apply grp_pow_commutes. Defined. From 42207b7f74abbd48e7112add6b2e15b209e1d272 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Wed, 17 Jul 2024 21:02:25 +0200 Subject: [PATCH 21/44] fix arguments of grp_homo_map Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/TensorProduct.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index 95f0020f69a..43a55476b52 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -621,7 +621,7 @@ Proof. * intros a a' z; cbn beta. apply (grp_homo_op (ab_mul z)). + hnf. - change (forall x : ?A, (grp_homo_map _ _ ?f) ((grp_homo_map _ _ ?g) x) = x) + change (forall x : ?A, (grp_homo_map ?f) ((grp_homo_map ?g) x) = x) with (f $o g $== Id _). snrapply ab_tensor_prod_ind_homotopy. intros a z. From 4d246eb152152b17510736ec15784a1426778d79 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Wed, 17 Jul 2024 21:05:42 +0200 Subject: [PATCH 22/44] bilinear -> biadditive for consistency Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/TensorProduct.v | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index 43a55476b52..eb9bd135576 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -18,10 +18,10 @@ Local Open Scope mc_add_scope. (** ** Construction *) -(** We define the tensor product of abelian groups as a quotient of the free abelian group on pairs of elements of the two groups by the subgroup generated by the bilinear pairs. *) +(** We define the tensor product of abelian groups as a quotient of the free abelian group on pairs of elements of the two groups by the subgroup generated by the biadditive pairs. *) -(** Here we define the subgroup of bilinear pairs in two steps *) -Definition family_bilinear_pairs {A B : AbGroup} +(** Here we define the subgroup of biadditive pairs in two steps *) +Definition family_biadditive_pairs {A B : AbGroup} : FreeAbGroup (A * B) -> Type. Proof. intros x. @@ -38,13 +38,13 @@ Proof. + exact (a, b2). Defined. -Definition subgroup_bilinear_pairs {A B : AbGroup} +Definition subgroup_biadditive_pairs {A B : AbGroup} : Subgroup (FreeAbGroup (A * B)) - := subgroup_generated family_bilinear_pairs. + := subgroup_generated family_biadditive_pairs. -(** The tensor product [ab_tensor_prod A B] of two abelian groups [A] and [B] is defined to ba a quotient of the free abelian group on pairs of elements [A * B] by the subgroup of bilinear pairs. *) +(** The tensor product [ab_tensor_prod A B] of two abelian groups [A] and [B] is defined to ba a quotient of the free abelian group on pairs of elements [A * B] by the subgroup of biadditive pairs. *) Definition ab_tensor_prod (A B : AbGroup) : AbGroup - := QuotientAbGroup (FreeAbGroup (A * B)) subgroup_bilinear_pairs. + := QuotientAbGroup (FreeAbGroup (A * B)) subgroup_biadditive_pairs. (** The tensor product of [A] and [B] contains formal combinations of pairs of elements from [A] and [B]. We denote these pairs as simple tensors and name them [tensor]. *) Definition tensor {A B : AbGroup} : A -> B -> ab_tensor_prod A B From 5873da317758a3d4349fbf0e620ffd526a1791a7 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Wed, 17 Jul 2024 20:25:46 -0400 Subject: [PATCH 23/44] TensorProduct, QuotientGroup: some speed-ups --- theories/Algebra/AbGroups/TensorProduct.v | 66 ++++++++++++++--------- theories/Algebra/Groups/QuotientGroup.v | 9 ++-- 2 files changed, 44 insertions(+), 31 deletions(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index eb9bd135576..00f2d4a4e0a 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -152,6 +152,44 @@ Defined. (** Here we write down some induction principles to help us prove lemmas about the tensor product. Some of these are quite specialised but are patterns that appear often in practice. *) (** Our main recursion principle states that in order to build a homomorphism out of the tensor product, it is sufficient to provide a map out of the direct product which is bilinear, that is, a map that preserves addition in both arguments of the product. *) + +(** We separate out the proof of this part, so we can make it opaque. *) +Definition ab_tensor_prod_rec_helper {A B C : AbGroup} + (f : A -> B -> C) + (l : forall a b b', f a (b + b') = f a b + f a b') + (r : forall a a' b, f (a + a') b = f a b + f a' b) + (x : FreeAbGroup (A * B)) (insg : subgroup_biadditive_pairs x) + : grp_homo_abel_rec (FreeGroup_rec (A * B) C (uncurry f)) x = mon_unit. +Proof. + strip_truncations. + induction insg as + [ x [ [ a [ a' [ b p ] ] ] | [ a [ b [ b' p ] ] ] ] + | + | ? ? ? H1 ? H2 ]. + - destruct p. + rewrite grp_homo_op. + rewrite grp_homo_inv. + apply grp_moveL_1M^-1%equiv. + unfold freeabgroup_in. + change (grp_homo_abel_rec ?f (abel_unit ?x)) with (f x). + simpl; rewrite 2 grp_unit_r. + apply r. + - destruct p. + rewrite grp_homo_op. + rewrite grp_homo_inv. + apply grp_moveL_1M^-1%equiv. + unfold freeabgroup_in. + change (grp_homo_abel_rec ?f (abel_unit ?x)) with (f x). + simpl; rewrite 2 grp_unit_r. + apply l. + - nrapply grp_homo_unit. + - rewrite grp_homo_op, grp_homo_inv. + apply grp_moveL_1M^-1. + exact(H1 @ H2^). +Defined. + +Opaque ab_tensor_prod_rec_helper. + Definition ab_tensor_prod_rec {A B C : AbGroup} (f : A -> B -> C) (l : forall a b b', f a (b + b') = f a b + f a b') @@ -163,32 +201,8 @@ Proof. - snrapply grp_homo_abel_rec. snrapply FreeGroup_rec. exact (uncurry f). - - intros x H. - strip_truncations. - induction H as - [ x [ [ a [ a' [ b p ] ] ] | [ a [ b [ b' p ] ] ] ] - | - | ? ? ? H1 ? H2 ]. - + destruct p. - rewrite grp_homo_op. - rewrite grp_homo_inv. - apply grp_moveL_1M^-1%equiv. - unfold freeabgroup_in. - change (grp_homo_abel_rec ?f (abel_unit ?x)) with (f x). - simpl; rewrite 2 grp_unit_r. - apply r. - + destruct p. - rewrite grp_homo_op. - rewrite grp_homo_inv. - apply grp_moveL_1M^-1%equiv. - unfold freeabgroup_in. - change (grp_homo_abel_rec ?f (abel_unit ?x)) with (f x). - simpl; rewrite 2 grp_unit_r. - apply l. - + nrapply grp_homo_unit. - + rewrite grp_homo_op, grp_homo_inv. - apply grp_moveL_1M^-1. - exact(H1 @ H2^). + - unfold normalsubgroup_subgroup. + apply ab_tensor_prod_rec_helper; assumption. Defined. (** Since we defined [ab_tensor_prod_rec] using the recursors of the underlying type, we get an annoying artifact of [x + 0] instead of [x] when acting on simple tensors. Typically in an argument we want our recursor to act on simple tensors without the extra [0] and this lemma makes sure of that. *) diff --git a/theories/Algebra/Groups/QuotientGroup.v b/theories/Algebra/Groups/QuotientGroup.v index dd2632d2bbf..dc844a00b0f 100644 --- a/theories/Algebra/Groups/QuotientGroup.v +++ b/theories/Algebra/Groups/QuotientGroup.v @@ -150,11 +150,10 @@ Section QuotientGroup. - srapply Quotient_rec. + exact f. + cbn; intros x y n. - symmetry. - apply grp_moveL_M1. - rewrite <- grp_homo_inv. - rewrite <- grp_homo_op. - apply h; assumption. + apply grp_moveR_M1. + rhs_V nrapply (ap (.* f y) (grp_homo_inv _ _)). + rhs_V nrapply grp_homo_op. + symmetry; apply h; assumption. - intro x. refine (Quotient_ind_hprop _ _ _). intro y. revert x. From d5ba1575410858b9785371a27b1e095ff7f526bb Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 18 Jul 2024 15:22:41 +0200 Subject: [PATCH 24/44] stagger definition of twist Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/TensorProduct.v | 60 +++++++++++++++++------ 1 file changed, 44 insertions(+), 16 deletions(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index 00f2d4a4e0a..256a85e2b6e 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -538,27 +538,55 @@ Defined. (** In order to construct the symmetric monoidal category, we will use what is termed the "Twist construction" in Monoidal.v. This simplifies the data of a symmetric monoidal category by constructing it from simpler parts. For instance, instead of having to prove full associativity [(A ⊗ B) ⊗ C $-> A ⊗ (B ⊗ C)], we can provide a twist map [A ⊗ (B ⊗ C) $-> B ⊗ (A ⊗ C)] and use the symmetric braiding we have so far to prove associativity. *) +(** In order to be more efficient whilst unfolding definitions, we break up the definition of a twist map into its components. *) + +Local Definition ab_tensor_prod_twist_map {A B C : AbGroup} + : A -> ab_tensor_prod B C -> ab_tensor_prod B (ab_tensor_prod A C). +Proof. + intros a. + snrapply ab_tensor_prod_rec. + - intros b c. + exact (tensor b (tensor a c)). + - intros b c c'; hnf. + lhs nrapply ap. + 1: nrapply tensor_dist_l. + nrapply tensor_dist_l. + - intros b b' c; hnf. + nrapply tensor_dist_r. +Defined. + +Local Definition ab_tensor_prod_twist_map_additive_r {A B C : AbGroup} + (a : A) (b b' : ab_tensor_prod B C) + : ab_tensor_prod_twist_map a (b + b') + = ab_tensor_prod_twist_map a b + ab_tensor_prod_twist_map a b'. +Proof. + intros; nrapply grp_homo_op. +Defined. + +Local Definition ab_tensor_prod_twist_map_additive_l {A B C : AbGroup} + (a a' : A) (b : ab_tensor_prod B C) + : ab_tensor_prod_twist_map (a + a') b + = ab_tensor_prod_twist_map a b + ab_tensor_prod_twist_map a' b. +Proof. + revert b. + nrapply ab_tensor_prod_ind_homotopy_plus. + intros b c. + rhs nrapply (ap011 (+)). + 2,3: nrapply ab_tensor_prod_rec_beta_tensor. + lhs nrapply ab_tensor_prod_rec_beta_tensor. + rhs_V nrapply tensor_dist_l. + snrapply (ap (tensor b)). + nrapply tensor_dist_r. +Defined. + (** Given a triple tensor product, we have a twist map which permutes the first two components. *) Definition ab_tensor_prod_twist {A B C} : ab_tensor_prod A (ab_tensor_prod B C) $-> ab_tensor_prod B (ab_tensor_prod A C). Proof. snrapply ab_tensor_prod_rec. - - intros a. - snrapply ab_tensor_prod_rec. - + intros b c. - exact (tensor b (tensor a c)). - + intros b c c'; hnf. - lhs nrapply ap. - 1: nrapply tensor_dist_l. - nrapply tensor_dist_l. - + intros b b' c; hnf. - nrapply tensor_dist_r. - - intros; nrapply grp_homo_op. - - intros a a'; unfold prod_ind; hnf. - nrapply ab_tensor_prod_ind_homotopy_plus. - intros b c. - rewrite 3 ab_tensor_prod_rec_beta_tensor. - by rewrite tensor_dist_r, tensor_dist_l. + - exact ab_tensor_prod_twist_map. + - exact ab_tensor_prod_twist_map_additive_r. + - exact ab_tensor_prod_twist_map_additive_l. Defined. (** The twist map acts in the expected way on simple tensors. *) From afac23be7d8aed32c323629a8af8e9bebd43bd2d Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 18 Jul 2024 21:07:22 +0200 Subject: [PATCH 25/44] simpl arg hint for ab_tensor_prod_twist_map Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/TensorProduct.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index 256a85e2b6e..de7653963f1 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -555,6 +555,8 @@ Proof. nrapply tensor_dist_r. Defined. +Arguments ab_tensor_prod_twist_map {A B C} _ _ /. + Local Definition ab_tensor_prod_twist_map_additive_r {A B C : AbGroup} (a : A) (b b' : ab_tensor_prod B C) : ab_tensor_prod_twist_map a (b + b') From 5b0692065479f1b6ec6667087a97b724d7afdc42 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Fri, 19 Jul 2024 17:17:36 +0200 Subject: [PATCH 26/44] make `FreeGroup_rec o freegroup_in` definitionally the identity Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/AbPushout.v | 2 +- theories/Algebra/AbGroups/AbelianGroup.v | 2 + theories/Algebra/AbGroups/Abelianization.v | 2 + theories/Algebra/AbGroups/Cyclic.v | 6 +- theories/Algebra/AbGroups/FreeAbelianGroup.v | 2 + theories/Algebra/AbGroups/TensorProduct.v | 105 +++---------- theories/Algebra/Groups/FreeGroup.v | 146 +++++++++++-------- theories/Algebra/Groups/Presentation.v | 25 +--- theories/Algebra/Groups/QuotientGroup.v | 1 + theories/Basics/Overture.v | 2 + theories/Types/Forall.v | 2 + 11 files changed, 129 insertions(+), 166 deletions(-) diff --git a/theories/Algebra/AbGroups/AbPushout.v b/theories/Algebra/AbGroups/AbPushout.v index 26793306e21..bcc5624a86b 100644 --- a/theories/Algebra/AbGroups/AbPushout.v +++ b/theories/Algebra/AbGroups/AbPushout.v @@ -28,7 +28,7 @@ Proof. - intros [x y] q; strip_truncations; simpl. destruct q as [a q]. cbn in q. refine (ap (uncurry (fun x y => b x + c y)) q^ @ _). - unfold uncurry; cbn. + cbn. refine (ap011 sg_op (preserves_negate _) (p a)^ @ _). exact (left_inverse _). Defined. diff --git a/theories/Algebra/AbGroups/AbelianGroup.v b/theories/Algebra/AbGroups/AbelianGroup.v index 3ec1e8dd535..0aaffdc9197 100644 --- a/theories/Algebra/AbGroups/AbelianGroup.v +++ b/theories/Algebra/AbGroups/AbelianGroup.v @@ -106,6 +106,8 @@ Defined. Definition QuotientAbGroup (G : AbGroup) (H : Subgroup G) : AbGroup := (Build_AbGroup (QuotientGroup' G H (isnormal_ab_subgroup G H)) _). +Arguments QuotientAbGroup G H : simpl never. + Definition quotient_abgroup_map (G : AbGroup) (H : Subgroup G) : GroupHomomorphism G (QuotientAbGroup G H). Proof. diff --git a/theories/Algebra/AbGroups/Abelianization.v b/theories/Algebra/AbGroups/Abelianization.v index d961cca3f7b..f84631ea01d 100644 --- a/theories/Algebra/AbGroups/Abelianization.v +++ b/theories/Algebra/AbGroups/Abelianization.v @@ -308,6 +308,8 @@ Proof. - exact _. Defined. +Arguments abel G : simpl never. + (** The unit of this map is the map [abel_in] which typeclasses can pick up to be a homomorphism. We write it out explicitly here. *) Definition abel_unit {G : Group} : GroupHomomorphism G (abel G) diff --git a/theories/Algebra/AbGroups/Cyclic.v b/theories/Algebra/AbGroups/Cyclic.v index d8e00f31df6..172984a1f52 100644 --- a/theories/Algebra/AbGroups/Cyclic.v +++ b/theories/Algebra/AbGroups/Cyclic.v @@ -48,8 +48,7 @@ Lemma Z1_mul_nat_beta {A : AbGroup} (a : A) (n : nat) Proof. induction n as [|n H]. 1: easy. - refine (grp_pow_natural _ _ _ @ _); simpl. - by rewrite grp_unit_r. + exact (grp_pow_natural _ _ _). Defined. (** [ab_Z1] is projective. *) @@ -65,8 +64,7 @@ Proof. apply path_homomorphism_from_free_group. simpl. intros []. - refine (_ @ a.2). - exact (ap p (grp_unit_r _)). + exact a.2. Defined. (** The map sending the generator to [1 : Int]. *) diff --git a/theories/Algebra/AbGroups/FreeAbelianGroup.v b/theories/Algebra/AbGroups/FreeAbelianGroup.v index 5c486704406..8adeb1f8ddc 100644 --- a/theories/Algebra/AbGroups/FreeAbelianGroup.v +++ b/theories/Algebra/AbGroups/FreeAbelianGroup.v @@ -30,6 +30,8 @@ Global Instance isfreeabgroup_isfreeabgroupon (S : Type) (F_S : AbGroup) (i : S Definition FreeAbGroup (S : Type) : AbGroup := abel (FreeGroup S). +Arguments FreeAbGroup S : simpl never. + Definition freeabgroup_in {S : Type} : S -> FreeAbGroup S := abel_unit o freegroup_in. diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index de7653963f1..fe537a2c3b5 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -46,6 +46,8 @@ Definition subgroup_biadditive_pairs {A B : AbGroup} Definition ab_tensor_prod (A B : AbGroup) : AbGroup := QuotientAbGroup (FreeAbGroup (A * B)) subgroup_biadditive_pairs. +Arguments ab_tensor_prod A B : simpl never. + (** The tensor product of [A] and [B] contains formal combinations of pairs of elements from [A] and [B]. We denote these pairs as simple tensors and name them [tensor]. *) Definition tensor {A B : AbGroup} : A -> B -> ab_tensor_prod A B := fun a b => grp_quotient_map (freeabgroup_in (a, b)). @@ -170,18 +172,12 @@ Proof. rewrite grp_homo_op. rewrite grp_homo_inv. apply grp_moveL_1M^-1%equiv. - unfold freeabgroup_in. - change (grp_homo_abel_rec ?f (abel_unit ?x)) with (f x). - simpl; rewrite 2 grp_unit_r. - apply r. + exact (r a a' b). - destruct p. rewrite grp_homo_op. rewrite grp_homo_inv. apply grp_moveL_1M^-1%equiv. - unfold freeabgroup_in. - change (grp_homo_abel_rec ?f (abel_unit ?x)) with (f x). - simpl; rewrite 2 grp_unit_r. - apply l. + exact (l a b b'). - nrapply grp_homo_unit. - rewrite grp_homo_op, grp_homo_inv. apply grp_moveL_1M^-1. @@ -205,17 +201,13 @@ Proof. apply ab_tensor_prod_rec_helper; assumption. Defined. -(** Since we defined [ab_tensor_prod_rec] using the recursors of the underlying type, we get an annoying artifact of [x + 0] instead of [x] when acting on simple tensors. Typically in an argument we want our recursor to act on simple tensors without the extra [0] and this lemma makes sure of that. *) Definition ab_tensor_prod_rec_beta_tensor {A B C : AbGroup} (f : A -> B -> C) (l : forall a b b', f a (b + b') = f a b + f a b') (r : forall a a' b, f (a + a') b = f a b + f a' b) (a : A) (b : B) - : ab_tensor_prod_rec f l r (tensor a b) = f a b. -Proof. - change (f a b + mon_unit = f a b). - apply grp_unit_r. -Defined. + : ab_tensor_prod_rec f l r (tensor a b) = f a b + := idpath. (** We give an induction principle for an hprop-valued type family [P]. It may be surprising at first that we only require [P] to hold for the simple tensors [tensor a b] and be closed under addition. It automatically follows that [P 0] holds (since [tensor 0 0 = 0]) and that [P] is closed under negation (since [tensor -a b = - tensor a b]). This induction principle says that the simple tensors generate the tensor product as a semigroup. *) Definition ab_tensor_prod_ind_hprop {A B : AbGroup} @@ -390,8 +382,7 @@ Proof. - intros [f [l r]]. snrapply (equiv_ap_inv' issig_Biadditive). rapply path_sigma_hprop. - funext a b. - snrapply grp_unit_r. + reflexivity. Defined. (** ** Functoriality of the Tensor Product *) @@ -504,9 +495,8 @@ Definition ab_tensor_swap_swap {A B} : ab_tensor_swap $o @ab_tensor_swap A B $== Id _. Proof. snrapply ab_tensor_prod_ind_homotopy. - intros a b; hnf. - change (ab_tensor_swap (ab_tensor_swap (tensor a b)) = tensor a b). - by rewrite 2 ab_tensor_swap_beta_tensor. + intros a b; simpl. + reflexivity. Defined. (** [ab_tensor_swap] is natural in both arguments. This means that it also acts on tensor functors. *) @@ -515,12 +505,8 @@ Definition ab_tensor_swap_natural {A B A' B'} (f : A $-> A') (g : B $-> B') $== functor_ab_tensor_prod g f $o ab_tensor_swap. Proof. snrapply ab_tensor_prod_ind_homotopy. - intros a b. - change (ab_tensor_swap (functor_ab_tensor_prod f g (tensor a b)) - = functor_ab_tensor_prod g f (ab_tensor_swap (tensor a b))). - rewrite functor_ab_tensor_prod_beta_tensor. - rewrite 2 ab_tensor_swap_beta_tensor. - by rewrite functor_ab_tensor_prod_beta_tensor. + intros a b; simpl. + reflexivity. Defined. (** The data of swap together gives us a symmetric braiding on the category of abelian groups. We will later show it is a full symmetric monoidal category. *) @@ -604,9 +590,8 @@ Definition ab_tensor_prod_twist_twist {A B C} Proof. snrapply ab_tensor_prod_ind_homotopy_triple. intros a b c. - change (ab_tensor_prod_twist (ab_tensor_prod_twist (tensor a (tensor b c))) - = tensor a (tensor b c)). - by rewrite 2 ab_tensor_prod_twist_beta_tensor_tensor. + change (tensor a (tensor b c) = tensor a (tensor b c)). + exact idpath. Defined. (** The twist map is natural in all 3 arguments. This means that the twist map acts on the triple tensor functor in the same way. *) @@ -617,11 +602,8 @@ Definition ab_tensor_prod_twist_natural {A B C A' B' C'} Proof. snrapply ab_tensor_prod_ind_homotopy_triple. intros a b c. - change (ab_tensor_prod_twist (functor_ab_tensor_prod f (functor_ab_tensor_prod g h) (tensor a (tensor b c))) - = functor_ab_tensor_prod g (functor_ab_tensor_prod f h) (ab_tensor_prod_twist (tensor a (tensor b c)))). - rewrite 2 functor_ab_tensor_prod_beta_tensor. - rewrite 2 ab_tensor_prod_twist_beta_tensor_tensor. - by rewrite 2 functor_ab_tensor_prod_beta_tensor. + change (tensor (g b) (tensor (f a) (h c)) = tensor (g b) (tensor (f a) (h c))). + exact idpath. Defined. (** ** Unitality of [abgroup_Z] *) @@ -695,13 +677,8 @@ Proof. intros a z. rhs nrapply (ap f). 2: nrapply ab_tensor_prod_rec_beta_tensor. - change (ab_tensor_prod_Z_r (fmap (flip ab_tensor_prod abgroup_Z) f (tensor a z)) - = f (grp_pow_homo a z)). - lhs nrapply ap. - 1: nrapply functor_ab_tensor_prod_beta_tensor. - lhs nrapply ab_tensor_prod_rec_beta_tensor. - symmetry. - apply grp_pow_natural. + simpl; symmetry. + nrapply grp_pow_natural. Defined. (** Since we have symmetry of the tensor product, we get left unitality for free. *) @@ -730,18 +707,6 @@ Proof. intros A B. snrapply ab_tensor_prod_ind_homotopy_triple. intros a b z. - (** Here we have to get the goal into the correct form to be able to reduce the functions on the simple tensors. *) - (** TODO: work out a way to reduce these change statements. *) - change (functor_ab_tensor_prod (Id A) (rightunitor_ab_tensor_prod B) (tensor a (tensor b z)) - = ab_tensor_swap (functor_ab_tensor_prod (Id B) - (rightunitor_ab_tensor_prod A) (ab_tensor_prod_twist (tensor a (tensor b z))))). - rewrite ab_tensor_prod_twist_beta_tensor_tensor. - rewrite 2 functor_ab_tensor_prod_beta_tensor. - rewrite ab_tensor_swap_beta_tensor. - lhs nrapply ap. - 1: rapply ab_tensor_prod_rec_beta_tensor. - rhs nrapply (ap (fun x => tensor x _)). - 2: rapply ab_tensor_prod_rec_beta_tensor. exact (tensor_ab_mul _ _ _)^. Defined. @@ -752,17 +717,8 @@ Proof. intros A B C. snrapply ab_tensor_prod_ind_homotopy_triple. intros b a c. - change (functor_ab_tensor_prod (Id C) ab_tensor_swap (ab_tensor_prod_twist - (functor_ab_tensor_prod (Id B) ab_tensor_swap (tensor b (tensor a c)))) - = ab_tensor_prod_twist (functor_ab_tensor_prod (Id A) ab_tensor_swap - (ab_tensor_prod_twist (tensor b (tensor a c))))). - rewrite functor_ab_tensor_prod_beta_tensor. - rewrite ab_tensor_swap_beta_tensor. - rewrite 2 ab_tensor_prod_twist_beta_tensor_tensor. - rewrite 2 functor_ab_tensor_prod_beta_tensor. - rewrite 2 ab_tensor_swap_beta_tensor. - rewrite ab_tensor_prod_twist_beta_tensor_tensor. - reflexivity. + change (tensor c (tensor a b) = tensor c (tensor a b)). + exact idpath. Defined. (** Finally, we can prove the pentagon identity using the quadruple tensor induction principle. As we did before, the work only involves reducing the involved functions on the simple tensor redexes. *) @@ -772,27 +728,8 @@ Proof. intros A B C D. snrapply ab_tensor_prod_ind_homotopy_quad. intros a b c d. - change ( - functor_ab_tensor_prod (Id C) ab_tensor_swap - (ab_tensor_prod_twist - (ab_tensor_swap - (ab_tensor_prod_twist - (functor_ab_tensor_prod (Id A) ab_tensor_swap - (tensor a (tensor b (tensor c d))))))) - = functor_ab_tensor_prod (Id C) ab_tensor_prod_twist - (functor_ab_tensor_prod (Id C) (functor_ab_tensor_prod (Id A) (@ab_tensor_swap B D)) - (ab_tensor_prod_twist - (functor_ab_tensor_prod (Id A) ab_tensor_prod_twist - (tensor a (tensor b (tensor c d))))))). - rewrite 2 functor_ab_tensor_prod_beta_tensor. - rewrite ab_tensor_swap_beta_tensor. - rewrite 3 ab_tensor_prod_twist_beta_tensor_tensor. - rewrite ab_tensor_swap_beta_tensor. - rewrite ab_tensor_prod_twist_beta_tensor_tensor. - rewrite 4 functor_ab_tensor_prod_beta_tensor. - rewrite 2 ab_tensor_swap_beta_tensor. - rewrite ab_tensor_prod_twist_beta_tensor_tensor. - reflexivity. + change (tensor c (tensor d (tensor a b)) = tensor c (tensor d (tensor a b))). + exact idpath. Defined. (** We therefore have all the data of a monoidal category. *) diff --git a/theories/Algebra/Groups/FreeGroup.v b/theories/Algebra/Groups/FreeGroup.v index 5555950736a..6882962b8c6 100644 --- a/theories/Algebra/Groups/FreeGroup.v +++ b/theories/Algebra/Groups/FreeGroup.v @@ -260,40 +260,61 @@ Section Reduction. Proof. snrapply (Build_Group freegroup_type); repeat split; exact _. Defined. + + Definition word_rec (G : Group) (s : A -> G) : A + A -> G. + Proof. + intros [x|x]. + - exact (s x). + - exact (- s x). + Defined. Definition words_rec (G : Group) (s : A -> G) : Words -> G. Proof. intro x. - induction x as [|x xs]. - 1: exact mon_unit. - refine (_ * IHxs). - destruct x as [x|x]. - 1: exact (s x). - exact (- s x). + induction x as [|x xs IHxs]. + - exact mon_unit. + - destruct xs. + + exact (word_rec G s x). + + exact (word_rec G s x * IHxs). + Defined. + + Definition words_rec_cons (G : Group) (s : A -> G) (x : A + A) (xs : Words) + : words_rec G s (x :: xs)%list = word_rec G s x * words_rec G s xs. + Proof. + induction xs in x |- *. + - symmetry; nrapply grp_unit_r. + - reflexivity. Defined. Lemma words_rec_pp (G : Group) (s : A -> G) (x y : Words) : words_rec G s (x @ y) = words_rec G s x * words_rec G s y. Proof. - induction x. - 1: symmetry; apply left_identity. - cbn; rewrite <- simple_associativity. - f_ap. + induction x as [|x xs IHxs] in y |- *. + - symmetry; nrapply grp_unit_l. + - change ((?x :: ?xs)%list @ y) with (x :: xs @ y)%list. + lhs nrapply words_rec_cons. + lhs nrapply ap. + 1: nrapply IHxs. + lhs nrapply grp_assoc. + nrapply (ap (.* _)). + symmetry. + apply words_rec_cons. Defined. Lemma words_rec_coh (G : Group) (s : A -> G) (a : A + A) (b c : Words) : words_rec G s (map1 (b, a, c)) = words_rec G s (map2 (b, a, c)). Proof. unfold map1, map2. - refine (concat _ (words_rec_pp G s _ _)^). - refine (concat (words_rec_pp G s _ _) _); f_ap. - refine (concat _ (right_identity _)). - refine (concat (ap _ (word_concat_w_ww _ _ _)^) _). - refine (concat (words_rec_pp G s _ _) _); f_ap. - refine (concat (concat (simple_associativity _ _ _) _) (left_identity mon_unit)). - destruct a; simpl; f_ap. - + apply right_inverse. - + apply left_inverse. + rhs nrapply (words_rec_pp G s). + lhs nrapply words_rec_pp. + nrapply (ap (.* _)). + rewrite <- word_concat_w_ww. + lhs nrapply words_rec_pp. + rhs_V nrapply grp_unit_r. + nrapply (ap (_ *.)). + destruct a; simpl. + - nrapply grp_inv_r. + - nrapply grp_inv_l. Defined. (** Given a group [G] we can construct a group homomorphism [FreeGroup A -> G] if we have a map [A -> G] *) @@ -313,48 +334,12 @@ Section Reduction. apply words_rec_pp. Defined. - (** Now we need to prove that the free group satisifes the unviersal property of the free group. *) - (** TODO: remove funext from here and universal property of free group *) - Global Instance isfreegroupon_freegroup `{Funext} - : IsFreeGroupOn A FreeGroup (freegroup_eta o word_sing o inl). - Proof. - intros G f. - snrapply Build_Contr. - { srefine (_;_); simpl. - 1: apply FreeGroup_rec, f. - intro x; simpl. - apply right_identity. } - intros [g h]. - nrapply path_sigma_hprop; [ exact _ |]. - simpl. - apply equiv_path_grouphomomorphism. - intro x. - rewrite <- (path_forall _ _ h). - strip_truncations; revert x. - snrapply Coeq_ind; intro x; [|apply path_ishprop]. - hnf; symmetry. - induction x. - 1: apply (grp_homo_unit g). - refine (concat (grp_homo_op g (freegroup_eta [a]) (freegroup_eta x)) _). - simpl. - f_ap. - destruct a. - 1: reflexivity. - exact (grp_homo_inv g (freegroup_eta [inl a])). - Defined. - - (** Typeclass search can already find this but we leave it here as a definition for reference. *) - Definition isfreegroup_freegroup `{Funext} : IsFreeGroup FreeGroup := _. - Definition freegroup_in : A -> FreeGroup := freegroup_eta o word_sing o inl. - Lemma FreeGroup_rec_beta {G : Group} (f : A -> G) - : FreeGroup_rec _ f o freegroup_in == f. - Proof. - intros x. - apply grp_unit_r. - Defined. + Definition FreeGroup_rec_beta {G : Group} (f : A -> G) + : FreeGroup_rec _ f o freegroup_in == f + := fun _ => idpath. Coercion freegroup_in : A >-> group_type. @@ -390,6 +375,51 @@ Section Reduction. + change (P (-(freegroup_in a) * freegroup_eta w)). by apply Hop. Defined. + + Definition FreeGroup_ind_homotopy {G : Group} {f f' : FreeGroup $-> G} + (H : forall x, f (freegroup_in x) = f' (freegroup_in x)) + : f $== f'. + Proof. + rapply FreeGroup_ind_hprop'. + induction w as [|[a|a] w IHw]. + - rhs nrapply grp_homo_unit. + nrapply grp_homo_unit. + - change (f (freegroup_in a * freegroup_eta w) + = f' (freegroup_in a * freegroup_eta w)). + lhs nrapply grp_homo_op. + rhs nrapply grp_homo_op. + exact (ap011 (.*.) (H a) IHw). + - change (f (-freegroup_in a * freegroup_eta w) + = f' (- freegroup_in a * freegroup_eta w)). + lhs nrapply grp_homo_op. + rhs nrapply grp_homo_op. + nrefine (ap011 (.*.) _ IHw). + lhs nrapply grp_homo_inv. + rhs nrapply grp_homo_inv. + exact (ap (-) (H _)). + Defined. + + (** Now we need to prove that the free group satisifes the unviersal property of the free group. *) + (** TODO: remove funext from here and universal property of free group *) + Global Instance isfreegroupon_freegroup `{Funext} + : IsFreeGroupOn A FreeGroup (freegroup_eta o word_sing o inl). + Proof. + intros G f. + snrapply Build_Contr. + { srefine (_;_); simpl. + 1: apply FreeGroup_rec, f. + intro x; reflexivity. } + intros [g h]. + nrapply path_sigma_hprop; [ exact _ |]. + simpl. + apply equiv_path_grouphomomorphism. + symmetry. + snrapply FreeGroup_ind_homotopy. + exact h. + Defined. + + (** Typeclass search can already find this but we leave it here as a definition for reference. *) + Definition isfreegroup_freegroup `{Funext} : IsFreeGroup FreeGroup := _. End Reduction. diff --git a/theories/Algebra/Groups/Presentation.v b/theories/Algebra/Groups/Presentation.v index 18d99526b76..db86b4bea9c 100644 --- a/theories/Algebra/Groups/Presentation.v +++ b/theories/Algebra/Groups/Presentation.v @@ -3,7 +3,7 @@ Require Import Truncations.Core. Require Import Algebra.Groups.Group. Require Import Algebra.Groups.FreeGroup. Require Import Algebra.Groups.GroupCoeq. -Require Import Spaces.Finite. +Require Import Spaces.Finite Spaces.List.Core. Require Import WildCat. @@ -92,21 +92,10 @@ Proof. intros f. srapply equiv_iff_hprop. { intros p. - hnf. - rapply Trunc_ind. - srapply Coeq.Coeq_ind. - 2: intros; apply path_ishprop. - intros w; hnf. - induction w. - 1: reflexivity. - simpl. - refine (_ @ _ @ _^). - 1,3: exact (grp_homo_op (FreeGroup_rec _ _ _) _ _). - f_ap. - destruct a. - 1: refine (p _ @ (grp_homo_unit _)^). - refine (grp_homo_inv _ _ @ ap _ _ @ (grp_homo_inv _ _)^). - refine (p _ @ (grp_homo_unit _)^). } + change (equiv_freegroup_rec H _ f $o FreeGroup_rec _ _ (gp_relators P) + $== equiv_freegroup_rec _ _ f $o FreeGroup_rec _ _ (fun _ => group_unit)). + rapply FreeGroup_ind_homotopy. + exact p. } intros p r. hnf in p. pose (p' := p o freegroup_eta). @@ -115,9 +104,7 @@ Proof. refine (_ @ p'). clear p'. symmetry. - refine (grp_homo_op _ _ _ @ _). - refine (_ @ right_identity _). - f_ap. + reflexivity. Defined. (** ** Constructors for finite presentations *) diff --git a/theories/Algebra/Groups/QuotientGroup.v b/theories/Algebra/Groups/QuotientGroup.v index dc844a00b0f..41ea9e6104a 100644 --- a/theories/Algebra/Groups/QuotientGroup.v +++ b/theories/Algebra/Groups/QuotientGroup.v @@ -173,6 +173,7 @@ Section QuotientGroup. End QuotientGroup. +Arguments QuotientGroup G N : simpl never. Arguments grp_quotient_map {_ _}. Notation "G / N" := (QuotientGroup G N) : group_scope. diff --git a/theories/Basics/Overture.v b/theories/Basics/Overture.v index f658b7db203..c0f3b0150d7 100644 --- a/theories/Basics/Overture.v +++ b/theories/Basics/Overture.v @@ -209,6 +209,8 @@ Notation "x .2" := (pr2 x) : fibration_scope. Definition uncurry {A B C} (f : A -> B -> C) (p : A * B) : C := f (fst p) (snd p). +Arguments uncurry {A B C} f%_function_scope p /. + (** Composition of functions. *) Notation compose := (fun g f x => g (f x)). diff --git a/theories/Types/Forall.v b/theories/Types/Forall.v index e0dd105f7e6..1aff29ca05d 100644 --- a/theories/Types/Forall.v +++ b/theories/Types/Forall.v @@ -366,6 +366,8 @@ Definition flip `{P : A -> B -> Type} : (forall a b, P a b) -> (forall b a, P a b) := fun f b a => f a b. +Arguments flip {A B P} f b a /. + Global Instance isequiv_flip `{P : A -> B -> Type} : IsEquiv (@flip _ _ P) | 0. Proof. From 1589b7103f672c4e9ff7d39b7d0e41d0715dc267 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Fri, 19 Jul 2024 15:39:35 -0400 Subject: [PATCH 27/44] FreeGroup, TensorProduct: some cleanups --- theories/Algebra/AbGroups/TensorProduct.v | 8 +++----- theories/Algebra/Groups/FreeGroup.v | 22 ++++++---------------- theories/Algebra/Groups/Presentation.v | 8 +------- 3 files changed, 10 insertions(+), 28 deletions(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index fe537a2c3b5..f3e41d61e36 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -495,7 +495,6 @@ Definition ab_tensor_swap_swap {A B} : ab_tensor_swap $o @ab_tensor_swap A B $== Id _. Proof. snrapply ab_tensor_prod_ind_homotopy. - intros a b; simpl. reflexivity. Defined. @@ -505,7 +504,7 @@ Definition ab_tensor_swap_natural {A B A' B'} (f : A $-> A') (g : B $-> B') $== functor_ab_tensor_prod g f $o ab_tensor_swap. Proof. snrapply ab_tensor_prod_ind_homotopy. - intros a b; simpl. + simpl. (* This speeds up the [reflexivity] and the [Defined]. *) reflexivity. Defined. @@ -589,9 +588,7 @@ Definition ab_tensor_prod_twist_twist {A B C} : ab_tensor_prod_twist $o @ab_tensor_prod_twist A B C $== Id _. Proof. snrapply ab_tensor_prod_ind_homotopy_triple. - intros a b c. - change (tensor a (tensor b c) = tensor a (tensor b c)). - exact idpath. + reflexivity. Defined. (** The twist map is natural in all 3 arguments. This means that the twist map acts on the triple tensor functor in the same way. *) @@ -602,6 +599,7 @@ Definition ab_tensor_prod_twist_natural {A B C A' B' C'} Proof. snrapply ab_tensor_prod_ind_homotopy_triple. intros a b c. + (* This [change] speeds up the [reflexivity]. [simpl] produces a goal that looks the same, but is still slow. *) change (tensor (g b) (tensor (f a) (h c)) = tensor (g b) (tensor (f a) (h c))). exact idpath. Defined. diff --git a/theories/Algebra/Groups/FreeGroup.v b/theories/Algebra/Groups/FreeGroup.v index 6882962b8c6..31a3be61bb5 100644 --- a/theories/Algebra/Groups/FreeGroup.v +++ b/theories/Algebra/Groups/FreeGroup.v @@ -380,29 +380,19 @@ Section Reduction. (H : forall x, f (freegroup_in x) = f' (freegroup_in x)) : f $== f'. Proof. - rapply FreeGroup_ind_hprop'. - induction w as [|[a|a] w IHw]. - - rhs nrapply grp_homo_unit. - nrapply grp_homo_unit. - - change (f (freegroup_in a * freegroup_eta w) - = f' (freegroup_in a * freegroup_eta w)). - lhs nrapply grp_homo_op. - rhs nrapply grp_homo_op. - exact (ap011 (.*.) (H a) IHw). - - change (f (-freegroup_in a * freegroup_eta w) - = f' (- freegroup_in a * freegroup_eta w)). - lhs nrapply grp_homo_op. - rhs nrapply grp_homo_op. - nrefine (ap011 (.*.) _ IHw). + rapply FreeGroup_ind_hprop. + - exact (concat (grp_homo_unit f) (grp_homo_unit f')^). + - exact H. + - intros x y p q. refine (grp_homo_op_agree f f' _ q). lhs nrapply grp_homo_inv. rhs nrapply grp_homo_inv. - exact (ap (-) (H _)). + exact (ap _ p). Defined. (** Now we need to prove that the free group satisifes the unviersal property of the free group. *) (** TODO: remove funext from here and universal property of free group *) Global Instance isfreegroupon_freegroup `{Funext} - : IsFreeGroupOn A FreeGroup (freegroup_eta o word_sing o inl). + : IsFreeGroupOn A FreeGroup freegroup_in. Proof. intros G f. snrapply Build_Contr. diff --git a/theories/Algebra/Groups/Presentation.v b/theories/Algebra/Groups/Presentation.v index db86b4bea9c..0a1a7b2b182 100644 --- a/theories/Algebra/Groups/Presentation.v +++ b/theories/Algebra/Groups/Presentation.v @@ -98,13 +98,7 @@ Proof. exact p. } intros p r. hnf in p. - pose (p' := p o freegroup_eta). - clearbody p'; clear p. - specialize (p' (FreeGroup.word_sing _ (inl r))). - refine (_ @ p'). - clear p'. - symmetry. - reflexivity. + exact (p (freegroup_in r)). Defined. (** ** Constructors for finite presentations *) From 0a58839788a943ca31c6befe00c18f8c0df9e45e Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Fri, 19 Jul 2024 21:46:13 +0200 Subject: [PATCH 28/44] remove reduction rules as they are definitional Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/TensorProduct.v | 80 ++++++----------------- 1 file changed, 20 insertions(+), 60 deletions(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index f3e41d61e36..db8cb843a6d 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -201,14 +201,6 @@ Proof. apply ab_tensor_prod_rec_helper; assumption. Defined. -Definition ab_tensor_prod_rec_beta_tensor {A B C : AbGroup} - (f : A -> B -> C) - (l : forall a b b', f a (b + b') = f a b + f a b') - (r : forall a a' b, f (a + a') b = f a b + f a' b) - (a : A) (b : B) - : ab_tensor_prod_rec f l r (tensor a b) = f a b - := idpath. - (** We give an induction principle for an hprop-valued type family [P]. It may be surprising at first that we only require [P] to hold for the simple tensors [tensor a b] and be closed under addition. It automatically follows that [P 0] holds (since [tensor 0 0 = 0]) and that [P] is closed under negation (since [tensor -a b = - tensor a b]). This induction principle says that the simple tensors generate the tensor product as a semigroup. *) Definition ab_tensor_prod_ind_hprop {A B : AbGroup} (P : ab_tensor_prod A B -> Type) @@ -367,21 +359,22 @@ Proof. - intros f. exists (fun x y => f (tensor x y)). snrapply Build_IsBiadditive. - + intros b a a'. - unfold flip. - rewrite tensor_dist_r. + + intros b a a'; simpl. + lhs nrapply (ap f). + 1: nrapply tensor_dist_r. nrapply grp_homo_op. - + intros a a' b. - rewrite tensor_dist_l. + + intros a a' b; simpl. + lhs nrapply (ap f). + 1: nrapply tensor_dist_l. nrapply grp_homo_op. - intros f. snrapply equiv_path_grouphomomorphism. snrapply ab_tensor_prod_ind_homotopy. - intros a b. - nrapply ab_tensor_prod_rec_beta_tensor. + intros a b; simpl. + reflexivity. - intros [f [l r]]. snrapply (equiv_ap_inv' issig_Biadditive). - rapply path_sigma_hprop. + rapply path_sigma_hprop; simpl. reflexivity. Defined. @@ -405,22 +398,13 @@ Proof. by rewrite tensor_dist_r. Defined. -(** The tensor product functor acts on simple tensors by mapping each component. *) -Definition functor_ab_tensor_prod_beta_tensor {A B A' B' : AbGroup} - (f : A $-> A') (g : B $-> B') (a : A) (b : B) - : functor_ab_tensor_prod f g (tensor a b) = tensor (f a) (g b). -Proof. - nrapply ab_tensor_prod_rec_beta_tensor. -Defined. - (** 2-functoriality of the tensor product. *) Definition functor2_ab_tensor_prod {A B A' B' : AbGroup} {f f' : A $-> A'} (p : f $== f') {g g' : B $-> B'} (q : g $== g') : functor_ab_tensor_prod f g $== functor_ab_tensor_prod f' g'. Proof. snrapply ab_tensor_prod_ind_homotopy. - intros a b. - rewrite 2 functor_ab_tensor_prod_beta_tensor. + intros a b; simpl. exact (ap011 tensor (p _) (q _)). Defined. @@ -429,8 +413,8 @@ Definition functor_ab_tensor_prod_id (A B : AbGroup) : functor_ab_tensor_prod (Id A) (Id B) $== Id (ab_tensor_prod A B). Proof. snrapply ab_tensor_prod_ind_homotopy. - intros a b. - apply functor_ab_tensor_prod_beta_tensor. + intros a b; simpl. + reflexivity. Defined. (** The tensor product functor preserves composition. *) @@ -440,11 +424,8 @@ Definition functor_ab_tensor_prod_compose {A B C A' B' C' : AbGroup} $== functor_ab_tensor_prod g g' $o functor_ab_tensor_prod f f'. Proof. snrapply ab_tensor_prod_ind_homotopy. - intros a b; hnf. - lhs nrapply functor_ab_tensor_prod_beta_tensor. - change (tensor (g (f a)) (g' (f' b)) - = functor_ab_tensor_prod g g' (functor_ab_tensor_prod f f' (tensor a b))). - by rewrite 2 functor_ab_tensor_prod_beta_tensor. + intros a b; simpl. + reflexivity. Defined. (** The tensor product functor is a 0-bifunctor. *) @@ -484,12 +465,6 @@ Proof. apply tensor_dist_l. Defined. -Definition ab_tensor_swap_beta_tensor {A B} a b - : @ab_tensor_swap A B (tensor a b) = tensor b a. -Proof. - nrapply ab_tensor_prod_rec_beta_tensor. -Defined. - (** [ab_tensor_swap] is involutive. *) Definition ab_tensor_swap_swap {A B} : ab_tensor_swap $o @ab_tensor_swap A B $== Id _. @@ -558,11 +533,10 @@ Proof. revert b. nrapply ab_tensor_prod_ind_homotopy_plus. intros b c. - rhs nrapply (ap011 (+)). - 2,3: nrapply ab_tensor_prod_rec_beta_tensor. - lhs nrapply ab_tensor_prod_rec_beta_tensor. + change (tensor b (tensor (a + a') c) + = tensor b (tensor a c) + tensor b (tensor a' c)). rhs_V nrapply tensor_dist_l. - snrapply (ap (tensor b)). + nrapply (ap (tensor b)). nrapply tensor_dist_r. Defined. @@ -576,13 +550,6 @@ Proof. - exact ab_tensor_prod_twist_map_additive_l. Defined. -(** The twist map acts in the expected way on simple tensors. *) -Definition ab_tensor_prod_twist_beta_tensor_tensor {A B C} a b c - : @ab_tensor_prod_twist A B C (tensor a (tensor b c)) = tensor b (tensor a c). -Proof. - rapply ab_tensor_swap_beta_tensor. -Defined. - (** The twist map is involutive. *) Definition ab_tensor_prod_twist_twist {A B C} : ab_tensor_prod_twist $o @ab_tensor_prod_twist A B C $== Id _. @@ -649,17 +616,12 @@ Proof. with (f $o g $== Id _). snrapply ab_tensor_prod_ind_homotopy. intros a z. - lhs nrapply (ap (grp_homo_tensor_r _)). - 1: apply ab_tensor_prod_rec_beta_tensor. change (tensor (B:=abgroup_Z) (grp_pow a z) 1%int = tensor a z). lhs nrapply tensor_ab_mul. nrapply ap. lhs nrapply abgroup_Z_ab_mul. apply int_mul_1_r. - + hnf. - intros x. - lhs nrapply ab_tensor_prod_rec_beta_tensor. - apply grp_unit_r. + + exact grp_unit_r. Defined. (** We have a right unitor for the tensor product given by unit [abgroup_Z]. Naturality of [ab_tensor_prod_Z_r] is straightforward to prove. *) @@ -673,10 +635,8 @@ Proof. intros A A' f. snrapply ab_tensor_prod_ind_homotopy. intros a z. - rhs nrapply (ap f). - 2: nrapply ab_tensor_prod_rec_beta_tensor. - simpl; symmetry. - nrapply grp_pow_natural. + change (grp_pow (f a) z = f (grp_pow a z)). + exact (grp_pow_natural _ _ _)^. Defined. (** Since we have symmetry of the tensor product, we get left unitality for free. *) From 67e9b6c22c078028a52b87445c4bf5b00935369f Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Fri, 19 Jul 2024 23:30:56 +0200 Subject: [PATCH 29/44] cleanup in FreeGroup.v Signed-off-by: Ali Caglayan --- theories/Algebra/Groups/FreeGroup.v | 173 +++++++++++++--------------- 1 file changed, 80 insertions(+), 93 deletions(-) diff --git a/theories/Algebra/Groups/FreeGroup.v b/theories/Algebra/Groups/FreeGroup.v index 31a3be61bb5..189ef1e215a 100644 --- a/theories/Algebra/Groups/FreeGroup.v +++ b/theories/Algebra/Groups/FreeGroup.v @@ -14,6 +14,8 @@ Section Reduction. Universe u. Context (A : Type@{u}). + + Local Open Scope list_scope. (** We define words (with inverses) on A to be lists of marked elements of A *) Local Definition Words : Type@{u} := list (A + A). @@ -30,48 +32,30 @@ Section Reduction. by destruct a. Defined. - (** We can concatenate words using list concatenation *) - Local Definition word_concat : Words -> Words -> Words := @app _. - - (** We introduce a local notation for word_concat. *) - Local Infix "@" := word_concat. - - Local Definition word_concat_w_nil x : x @ nil = x. - Proof. - induction x; trivial. - cbn; f_ap. - Defined. - - Local Definition word_concat_w_ww x y z : x @ (y @ z) = (x @ y) @ z. - Proof. - apply app_assoc. - Defined. - - (** Singleton word *) - Local Definition word_sing (x : A + A) : Words := (cons x nil). - - Local Notation "[ x ]" := (word_sing x). - (** Now we wish to define the free group on A as the following HIT: HIT N(A) : hSet | eta : Words -> N(A) | tau (x : Words) (a : A + A) (y : Words) - : eta (x @ [a] @ [a^] @ y) = eta (x @ y). + : eta (x ++ [a] ++ [a^] ++ y) = eta (x ++ y). Since we cannot write our HITs directly like this (without resorting to private inductive types), we will construct this HIT out of HITs we know. In fact, we can define N(A) as a coequalizer. *) Local Definition map1 : Words * (A + A) * Words -> Words. Proof. intros [[x a] y]. - exact (x @ [a] @ [a^] @ y). + exact (x ++ [a] ++ [a^] ++ y). Defined. + + Arguments map1 _ /. Local Definition map2 : Words * (A + A) * Words -> Words. Proof. intros [[x a] y]. - exact (x @ y). + exact (x ++ y). Defined. + + Arguments map2 _ /. (** Now we can define the underlying type of the free group as the 0-truncated coequalizer of these two maps *) Definition freegroup_type : Type := Tr 0 (Coeq map1 map2). @@ -81,7 +65,7 @@ Section Reduction. (** This is the path constructor *) Definition freegroup_tau (x : Words) (a : A + A) (y : Words) - : freegroup_eta (x @ [a] @ [a^] @ y) = freegroup_eta (x @ y). + : freegroup_eta (x ++ [a] ++ [a^] ++ y) = freegroup_eta (x ++ y). Proof. apply path_Tr, tr. exact ((cglue (x, a, y))). @@ -96,87 +80,89 @@ Section Reduction. { intros x; revert y. snrapply Coeq_rec. { intros y. - exact (freegroup_eta (x @ y)). } - intros [[y a] z]; cbn. - refine (concat (ap _ _) _). - { refine (concat (word_concat_w_ww _ _ _) _). - rapply (ap (fun t => t @ _)). - refine (concat (word_concat_w_ww _ _ _) _). - rapply (ap (fun t => t @ _)). - refine (word_concat_w_ww _ _ _). } - refine (concat _ (ap _ _^)). - 2: apply word_concat_w_ww. - apply freegroup_tau. } + exact (freegroup_eta (x ++ y)). } + intros [[y a] z]; simpl. + change (freegroup_eta (x ++ y ++ ([a] ++ [a^] ++ z)) + = freegroup_eta (x ++ y ++ z)). + rhs nrapply ap. + 2: nrapply app_assoc. + lhs nrapply ap. + 1: nrapply app_assoc. + nrapply (freegroup_tau _ a). } intros [[c b] d]. - simpl. revert y. snrapply Coeq_ind. - { simpl. - intro a. - rewrite <- word_concat_w_ww. - rewrite <- (word_concat_w_ww _ _ a). - rapply (freegroup_tau c b (d @ a)). } - intro; rapply path_ishprop. + 2: intro; rapply path_ishprop. + intro a. + change (freegroup_eta ((c ++ [b] ++ [b^] ++ d) ++ a) + = freegroup_eta ((c ++ d) ++ a)). + lhs_V nrapply ap. + 1: nrapply app_assoc. + lhs_V nrapply (ap (fun x => freegroup_eta (c ++ x))). + 1: nrapply app_assoc. + lhs_V nrapply (ap (fun x => freegroup_eta (c ++ _ ++ x))). + 1: nrapply app_assoc. + rhs_V nrapply ap. + 2: nrapply app_assoc. + nrapply freegroup_tau. Defined. (** The unit of the free group is the empty word *) - Global Instance monunit_freegroup_type : MonUnit freegroup_type. - Proof. - apply freegroup_eta. - exact nil. - Defined. + Global Instance monunit_freegroup_type : MonUnit freegroup_type + := freegroup_eta nil. (** We can change the sign of all the elements in a word and reverse the order. This will be the inversion in the group *) Fixpoint word_change_sign (x : Words) : Words. Proof. destruct x as [|x xs]. - 1: exact nil. - exact (word_change_sign xs @ [change_sign x]). + - exact nil. + - exact (word_change_sign xs ++ [ change_sign x ]). Defined. (** Changing the sign changes the order of word concatenation *) Definition word_change_sign_ww (x y : Words) - : word_change_sign (x @ y) = word_change_sign y @ word_change_sign x. + : word_change_sign (x ++ y) = word_change_sign y ++ word_change_sign x. Proof. - induction x. - { symmetry. - apply word_concat_w_nil. } - simpl. - refine (concat _ (inverse (word_concat_w_ww _ _ _))). - f_ap. + induction x as [|x a IHx]. + - symmetry; nrapply app_nil. + - simpl. + rhs nrapply app_assoc. + nrapply (ap (fun x => x ++ _)). + exact IHx. Defined. (** This is also involutive *) Lemma word_change_sign_inv x : word_change_sign (word_change_sign x) = x. Proof. - induction x. + induction x as [|x ? IHx]. 1: reflexivity. simpl. - rewrite word_change_sign_ww. - cbn; f_ap. - apply change_sign_inv. + lhs nrapply word_change_sign_ww. + simpl; nrapply ap011. + 1: nrapply change_sign_inv. + exact IHx. Defined. (** Changing the sign gives us left inverses *) - Lemma word_concat_Vw x : freegroup_eta (word_change_sign x @ x) = mon_unit. + Lemma word_concat_Vw x : freegroup_eta (word_change_sign x ++ x) = mon_unit. Proof. induction x. 1: reflexivity. simpl. set (a' := a^). rewrite <- (change_sign_inv a). - change (freegroup_eta ((word_change_sign x @ [a']) @ ([a'^] @ x)) = mon_unit). - rewrite word_concat_w_ww. - rewrite freegroup_tau. + change (freegroup_eta ((word_change_sign x ++ [a']) ++ ([a'^] ++ x)) = mon_unit). + rewrite <- app_assoc. + lhs nrapply freegroup_tau. apply IHx. Defined. (** And since changing the sign is involutive we get right inverses from left inverses *) - Lemma word_concat_wV x : freegroup_eta (x @ word_change_sign x) = mon_unit. + Lemma word_concat_wV x : freegroup_eta (x ++ word_change_sign x) = mon_unit. Proof. set (x' := word_change_sign x). rewrite <- (word_change_sign_inv x). - change (freegroup_eta (word_change_sign x' @ x') = mon_unit). + change (freegroup_eta (word_change_sign x' ++ x') = mon_unit). apply word_concat_Vw. Defined. @@ -191,21 +177,20 @@ Section Reduction. exact (word_change_sign x). } intros [[b a] c]. unfold map1, map2. - refine (concat _ (ap _ (inverse _))). - 2: apply word_change_sign_ww. - refine (concat (ap _ _) _). - { refine (concat (word_change_sign_ww _ _) _). - apply ap. - refine (concat (ap _ (inverse (word_concat_w_ww _ _ _))) _). - refine (concat (word_change_sign_ww _ _) _). - rapply (ap (fun t => t @ word_change_sign b)). - apply word_change_sign_ww. } - refine (concat _ (freegroup_tau _ a _)). - apply ap. - refine (concat (word_concat_w_ww _ _ _) _); f_ap. - refine (concat (word_concat_w_ww _ _ _) _); f_ap. - f_ap; cbn; f_ap. - apply change_sign_inv. + lhs nrapply ap. + { lhs nrapply word_change_sign_ww. + nrapply (ap (fun x => x ++ _)). + lhs nrapply word_change_sign_ww. + nrapply (ap (fun x => x ++ _)). + lhs nrapply word_change_sign_ww. + nrapply (ap (fun x => _ ++ x)). + nrapply (word_change_sign_inv [a]). } + lhs_V nrapply ap. + 1: rhs_V nrapply app_assoc. + 1: nrapply app_assoc. + rhs nrapply ap. + 2: nrapply word_change_sign_ww. + nrapply freegroup_tau. Defined. (** Now we can start to prove the group laws. Since these are hprops we can ignore what happens with the path constructor. *) @@ -218,8 +203,8 @@ Section Reduction. revert x; snrapply Coeq_ind; intro x; [ | apply path_ishprop]. revert y; snrapply Coeq_ind; intro y; [ | apply path_ishprop]. revert z; snrapply Coeq_ind; intro z; [ | apply path_ishprop]. - rapply (ap (tr o coeq)). - apply word_concat_w_ww. + nrapply (ap (tr o coeq)). + nrapply app_assoc. Defined. (** Left identity *) @@ -236,7 +221,7 @@ Section Reduction. rapply Trunc_ind. srapply Coeq_ind; intro x; [ | apply path_ishprop]. apply (ap tr), ap. - apply word_concat_w_nil. + nrapply app_nil. Defined. (** Left inverse *) @@ -287,11 +272,11 @@ Section Reduction. Defined. Lemma words_rec_pp (G : Group) (s : A -> G) (x y : Words) - : words_rec G s (x @ y) = words_rec G s x * words_rec G s y. + : words_rec G s (x ++ y) = words_rec G s x * words_rec G s y. Proof. induction x as [|x xs IHxs] in y |- *. - symmetry; nrapply grp_unit_l. - - change ((?x :: ?xs)%list @ y) with (x :: xs @ y)%list. + - change ((?x :: ?xs) ++ y) with (x :: xs ++ y). lhs nrapply words_rec_cons. lhs nrapply ap. 1: nrapply IHxs. @@ -307,11 +292,13 @@ Section Reduction. unfold map1, map2. rhs nrapply (words_rec_pp G s). lhs nrapply words_rec_pp. - nrapply (ap (.* _)). - rewrite <- word_concat_w_ww. - lhs nrapply words_rec_pp. - rhs_V nrapply grp_unit_r. nrapply (ap (_ *.)). + lhs nrapply words_rec_pp. + lhs nrapply ap. + 1: nrapply words_rec_pp. + lhs nrapply grp_assoc. + rhs_V nrapply grp_unit_l. + nrapply (ap (.* _)). destruct a; simpl. - nrapply grp_inv_r. - nrapply grp_inv_l. @@ -335,7 +322,7 @@ Section Reduction. Defined. Definition freegroup_in : A -> FreeGroup - := freegroup_eta o word_sing o inl. + := freegroup_eta o (fun x => [ x ]) o inl. Definition FreeGroup_rec_beta {G : Group} (f : A -> G) : FreeGroup_rec _ f o freegroup_in == f From 1d49f735f929e65154de7b5e8171e159a09419d2 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Fri, 19 Jul 2024 23:34:48 +0200 Subject: [PATCH 30/44] add comment about words_rec Signed-off-by: Ali Caglayan --- theories/Algebra/Groups/FreeGroup.v | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/theories/Algebra/Groups/FreeGroup.v b/theories/Algebra/Groups/FreeGroup.v index 189ef1e215a..29ba6385938 100644 --- a/theories/Algebra/Groups/FreeGroup.v +++ b/theories/Algebra/Groups/FreeGroup.v @@ -253,14 +253,14 @@ Section Reduction. - exact (- s x). Defined. + (** When we have a list of words we can recursively define a group element. The obvious choice would be to map [nil] to the identity and [x :: xs] to [x * words_rec xs]. This has the disadvantage that a single generating element gets mapped to [x * 1] instead of [x]. To fix this issue, we map [nil] to the identity, the singleton to the element we want, and do the rest recursively. *) Definition words_rec (G : Group) (s : A -> G) : Words -> G. Proof. - intro x. - induction x as [|x xs IHxs]. + intro xs. + induction xs as [|x [|y xs] IHxs]. - exact mon_unit. - - destruct xs. - + exact (word_rec G s x). - + exact (word_rec G s x * IHxs). + - exact (word_rec G s x). + - exact (word_rec G s x * IHxs). Defined. Definition words_rec_cons (G : Group) (s : A -> G) (x : A + A) (xs : Words) @@ -304,7 +304,7 @@ Section Reduction. - nrapply grp_inv_l. Defined. - (** Given a group [G] we can construct a group homomorphism [FreeGroup A -> G] if we have a map [A -> G] *) + (** Given a group [G] we can construct a group homomorphism [FreeGroup A -> G] if we have a map [A -> G]. *) Definition FreeGroup_rec (G : Group) (s : A -> G) : GroupHomomorphism FreeGroup G. Proof. From 7c74b6ec7e631bfec50fb16388d0ccfc725f7708 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Fri, 19 Jul 2024 23:36:00 +0200 Subject: [PATCH 31/44] remove exact idpath Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/TensorProduct.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index db8cb843a6d..e3ab8ef0e68 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -568,7 +568,7 @@ Proof. intros a b c. (* This [change] speeds up the [reflexivity]. [simpl] produces a goal that looks the same, but is still slow. *) change (tensor (g b) (tensor (f a) (h c)) = tensor (g b) (tensor (f a) (h c))). - exact idpath. + reflexivity. Defined. (** ** Unitality of [abgroup_Z] *) @@ -676,7 +676,7 @@ Proof. snrapply ab_tensor_prod_ind_homotopy_triple. intros b a c. change (tensor c (tensor a b) = tensor c (tensor a b)). - exact idpath. + reflexivity. Defined. (** Finally, we can prove the pentagon identity using the quadruple tensor induction principle. As we did before, the work only involves reducing the involved functions on the simple tensor redexes. *) @@ -687,7 +687,7 @@ Proof. snrapply ab_tensor_prod_ind_homotopy_quad. intros a b c d. change (tensor c (tensor d (tensor a b)) = tensor c (tensor d (tensor a b))). - exact idpath. + reflexivity. Defined. (** We therefore have all the data of a monoidal category. *) From 7ddd945c8a1ef3a9b723cbb2663b8fdc2a5e52a9 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Fri, 19 Jul 2024 22:10:29 -0400 Subject: [PATCH 32/44] FreeGroup: use a instead of x for a "letter" in A + A --- theories/Algebra/Groups/FreeGroup.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Algebra/Groups/FreeGroup.v b/theories/Algebra/Groups/FreeGroup.v index 29ba6385938..1742d119f24 100644 --- a/theories/Algebra/Groups/FreeGroup.v +++ b/theories/Algebra/Groups/FreeGroup.v @@ -24,7 +24,7 @@ Section Reduction. Local Definition change_sign : A + A -> A + A := equiv_sum_symm A A. (** We introduce a local notation for [change_sign]. It is only defined in this section however. *) - Local Notation "x ^" := (change_sign x). + Local Notation "a ^" := (change_sign a). (** Changing sign is an involution *) Local Definition change_sign_inv a : a^^ = a. From 46c1bf066b8d640ce23ca200d419d01bd5db179c Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sat, 20 Jul 2024 13:18:59 +0200 Subject: [PATCH 33/44] use more list operations in FreeGroup.v Signed-off-by: Ali Caglayan --- theories/Algebra/Groups/FreeGroup.v | 42 ++++++++++++++--------------- theories/Spaces/List/Theory.v | 36 +++++++++++++++++++++++++ 2 files changed, 56 insertions(+), 22 deletions(-) diff --git a/theories/Algebra/Groups/FreeGroup.v b/theories/Algebra/Groups/FreeGroup.v index 1742d119f24..a0c8a5954d1 100644 --- a/theories/Algebra/Groups/FreeGroup.v +++ b/theories/Algebra/Groups/FreeGroup.v @@ -112,35 +112,30 @@ Section Reduction. := freegroup_eta nil. (** We can change the sign of all the elements in a word and reverse the order. This will be the inversion in the group *) - Fixpoint word_change_sign (x : Words) : Words. - Proof. - destruct x as [|x xs]. - - exact nil. - - exact (word_change_sign xs ++ [ change_sign x ]). - Defined. + Definition word_change_sign (x : Words) : Words + := reverse (list_map change_sign x). (** Changing the sign changes the order of word concatenation *) Definition word_change_sign_ww (x y : Words) : word_change_sign (x ++ y) = word_change_sign y ++ word_change_sign x. Proof. - induction x as [|x a IHx]. - - symmetry; nrapply app_nil. - - simpl. - rhs nrapply app_assoc. - nrapply (ap (fun x => x ++ _)). - exact IHx. + unfold word_change_sign. + lhs nrapply (ap reverse). + 1: nrapply list_map_app. + nrapply reverse_app. Defined. (** This is also involutive *) Lemma word_change_sign_inv x : word_change_sign (word_change_sign x) = x. Proof. - induction x as [|x ? IHx]. - 1: reflexivity. - simpl. - lhs nrapply word_change_sign_ww. - simpl; nrapply ap011. - 1: nrapply change_sign_inv. - exact IHx. + unfold word_change_sign. + lhs_V nrapply list_map_reverse. + lhs nrapply ap. + 1: nrapply reverse_reverse. + lhs_V nrapply list_map_compose. + snrapply list_map_id. + intros a ?. + apply change_sign_inv. Defined. (** Changing the sign gives us left inverses *) @@ -148,11 +143,14 @@ Section Reduction. Proof. induction x. 1: reflexivity. - simpl. + lhs nrapply (ap (fun x => freegroup_eta (x ++ _))). + 1: nrapply reverse_cons. + change (freegroup_eta ((word_change_sign x ++ [a^]) ++ [a] ++ x) + = mon_unit). + lhs_V nrapply ap. + 1: nrapply app_assoc. set (a' := a^). rewrite <- (change_sign_inv a). - change (freegroup_eta ((word_change_sign x ++ [a']) ++ ([a'^] ++ x)) = mon_unit). - rewrite <- app_assoc. lhs nrapply freegroup_tau. apply IHx. Defined. diff --git a/theories/Spaces/List/Theory.v b/theories/Spaces/List/Theory.v index 5c18da7f420..71251638e7f 100644 --- a/theories/Spaces/List/Theory.v +++ b/theories/Spaces/List/Theory.v @@ -145,6 +145,15 @@ Proof. exact (y'; (p, inr i')). Defined. +(** Mapping a function over a concatenated list is the concatenation of the mapped lists. *) +Definition list_map_app {A B : Type} (f : A -> B) (l l' : list A) + : list_map f (l ++ l') = list_map f l ++ list_map f l'. +Proof. + induction l as [|a l IHl]. + 1: reflexivity. + simpl; f_ap. +Defined. + (** A function that acts as the identity on the elements of a list is the identity on the mapped list. *) Lemma list_map_id {A : Type} (f : A -> A) (l : list A) (Hf : forall x, InList x l -> f x = x) @@ -287,6 +296,33 @@ Proof. cbn; apply reverse_acc_cons. Defined. +(** The [reverse] of a concatenated list is the concatenation of the reversed lists in reverse order. *) +Definition reverse_app {A : Type} (l l' : list A) + : reverse (l ++ l') = reverse l' ++ reverse l. +Proof. + induction l as [|a l IHl] in l' |- *. + 1: symmetry; apply app_nil. + simpl. + lhs nrapply reverse_cons. + rhs nrapply ap. + 2: nrapply reverse_cons. + rhs nrapply app_assoc. + nrapply (ap (fun l => l ++ [a])). + exact (IHl l'). +Defined. + +(** [reverse] is involutive. *) +Definition reverse_reverse {A : Type} (l : list A) + : reverse (reverse l) = l. +Proof. + induction l. + 1: reflexivity. + lhs nrapply ap. + 1: nrapply reverse_cons. + lhs nrapply reverse_app. + exact (ap _ IHl). +Defined. + (** ** Getting elements *) (** A variant of [nth] that returns an element of the list and a proof that it is the [n]-th element. *) From e2f8d7421e2d9061d6e6acbe0d38651675671867 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sat, 20 Jul 2024 13:36:40 +0200 Subject: [PATCH 34/44] write a little intro for tensor products Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/TensorProduct.v | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index e3ab8ef0e68..05f5476b014 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -14,7 +14,13 @@ Require Import Truncations. Local Open Scope mc_scope. Local Open Scope mc_add_scope. -(** * Tensor Product of Abelian Groups *) +(** * The Tensor Product of Abelian Groups *) + +(** Various operations on abelian groups [A × B → C] are biadditive meaning that they are group homomorphisms when we fix the left or right argument. + +The tensor product of abelian groups is a special construction that produces a new abelian group [A ⊗ B] which provides the "best" possible way to create a biadditive function, meaning that any bilinear map [A × B → C] factors uniquely through the tensor product. This fully encapsulates all the ways [A] and [B] can interact biadditively. + +Biadditive functions appear in all sorts of contexts ranging from linear algebra to analysis. Therefore having a way to systematically study them is very useful. *) (** ** Construction *) From f2c9ec7610db1afb73f3ea887954c355b5a3ed56 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sat, 20 Jul 2024 13:39:28 +0200 Subject: [PATCH 35/44] small changes to comments Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/TensorProduct.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index 05f5476b014..987aa4c4dbf 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -48,13 +48,13 @@ Definition subgroup_biadditive_pairs {A B : AbGroup} : Subgroup (FreeAbGroup (A * B)) := subgroup_generated family_biadditive_pairs. -(** The tensor product [ab_tensor_prod A B] of two abelian groups [A] and [B] is defined to ba a quotient of the free abelian group on pairs of elements [A * B] by the subgroup of biadditive pairs. *) +(** The tensor product [ab_tensor_prod A B] of two abelian groups [A] and [B] is defined to be a quotient of the free abelian group on pairs of elements [A * B] by the subgroup of biadditive pairs. *) Definition ab_tensor_prod (A B : AbGroup) : AbGroup := QuotientAbGroup (FreeAbGroup (A * B)) subgroup_biadditive_pairs. Arguments ab_tensor_prod A B : simpl never. -(** The tensor product of [A] and [B] contains formal combinations of pairs of elements from [A] and [B]. We denote these pairs as simple tensors and name them [tensor]. *) +(** The tensor product of [A] and [B] contains formal combinations of pairs of elements from [A] and [B]. We denote these pairs as "simple tensors" and name them [tensor]. *) Definition tensor {A B : AbGroup} : A -> B -> ab_tensor_prod A B := fun a b => grp_quotient_map (freeabgroup_in (a, b)). From 1b5da89a5dd85e1cfc3ab1e5d351c66f24291a08 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Sat, 20 Jul 2024 16:22:56 -0400 Subject: [PATCH 36/44] TensorProduct: update introductory comments --- theories/Algebra/AbGroups/TensorProduct.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index 987aa4c4dbf..0120bd45ccd 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -16,9 +16,9 @@ Local Open Scope mc_add_scope. (** * The Tensor Product of Abelian Groups *) -(** Various operations on abelian groups [A × B → C] are biadditive meaning that they are group homomorphisms when we fix the left or right argument. +(** Various maps [A * B → C] from the cartesian product of two abelian groups to another abelian group are "biadditive", meaning that they are group homomorphisms when we fix the left or right argument. -The tensor product of abelian groups is a special construction that produces a new abelian group [A ⊗ B] which provides the "best" possible way to create a biadditive function, meaning that any bilinear map [A × B → C] factors uniquely through the tensor product. This fully encapsulates all the ways [A] and [B] can interact biadditively. +The tensor product of abelian groups is a construction that produces an abelian group [A ⊗ B] along with a biadditive map [A * B -> A ⊗ B] which is initial among biadditive maps from [A * B]. This means that any bilinear map [A * B → C] factors uniquely through the tensor product via a group homomorphism [A ⊗ B -> C]. Biadditive functions appear in all sorts of contexts ranging from linear algebra to analysis. Therefore having a way to systematically study them is very useful. *) @@ -26,7 +26,7 @@ Biadditive functions appear in all sorts of contexts ranging from linear algebra (** We define the tensor product of abelian groups as a quotient of the free abelian group on pairs of elements of the two groups by the subgroup generated by the biadditive pairs. *) -(** Here we define the subgroup of biadditive pairs in two steps *) +(** Here we define the subgroup of biadditive pairs in two steps. *) Definition family_biadditive_pairs {A B : AbGroup} : FreeAbGroup (A * B) -> Type. Proof. From b68787831a9b14079f45da68091d4fe7989568ef Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Mon, 22 Jul 2024 10:50:10 -0400 Subject: [PATCH 37/44] premetric.v: get rid of shadowed definition of uncurry --- theories/Classes/theory/premetric.v | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/theories/Classes/theory/premetric.v b/theories/Classes/theory/premetric.v index 06ec0fccf93..4674d0976cc 100644 --- a/theories/Classes/theory/premetric.v +++ b/theories/Classes/theory/premetric.v @@ -21,7 +21,6 @@ Generalizable Variables A B. Local Set Universe Minimization ToSet. - Class Closeness@{i} (A : Type@{i}) := close : Q+ -> Relation@{i i} A. Global Instance Q_close@{} : Closeness Q := fun e q r => - ' e < q - r < ' e. @@ -299,8 +298,7 @@ Class Continuous@{UA UB} Arguments continuous {A _ B _} f {_} _ _. Definition BinaryDup@{i} {A : Type@{i} } : A -> A /\ A := fun x => (x, x). -Definition uncurry {A B C} (f : A -> B -> C) : A /\ B -> C - := fun x => f (fst x) (snd x). + Definition map2 {A B C D} (f : A -> C) (g : B -> D) : A /\ B -> C /\ D := fun x => (f (fst x), g (snd x)). @@ -464,7 +462,7 @@ Global Instance uncurry_lipschitz (f : A -> B -> C) L1 L2 : Lipschitz (uncurry f) (L1 + L2). Proof. intros e [u1 u2] [v1 v2] [xi1 xi2]. simpl in xi1,xi2. -unfold uncurry;simpl. +simpl. assert (Hrw : (L1 + L2) * e = L1 * e + L2 * e) by abstract (apply pos_eq;ring_tac.ring_with_nat); rewrite Hrw;clear Hrw. From a6873f06f42c397ee201d583ef892951ae35f58d Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 22 Jul 2024 18:15:40 +0200 Subject: [PATCH 38/44] fix typo Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/TensorProduct.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index 0120bd45ccd..7064475eec7 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -706,4 +706,4 @@ Global Instance issymmmetricmonoidal_ab_tensor_prod : IsSymmetricMonoidal AbGroup ab_tensor_prod abgroup_Z := {}. -(** TODO: Show that the category of abelian groups is symmetric closed and therefore we have adjoint pair with the tesnor and internal hom. This should allow us to prove lemmas such as tensors distributing over coproducts. *) +(** 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. *) From da274271cccd8b6659d0152060410df7a05a61cc Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Mon, 22 Jul 2024 13:47:27 -0400 Subject: [PATCH 39/44] TensorProduct: simplify and/or speed up some proofs --- theories/Algebra/AbGroups/TensorProduct.v | 86 +++++++++-------------- 1 file changed, 32 insertions(+), 54 deletions(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index 7064475eec7..e1cb8fc3c5b 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -32,12 +32,12 @@ Definition family_biadditive_pairs {A B : AbGroup} Proof. intros x. refine ((exists (a1 a2 : A) (b : B), _) + exists (a : A) (b1 b2 : B), _)%type. - - refine (_ - (_ + _) = x). + - refine (- _ + (_ + _) = x). 1-3: apply freeabgroup_in. + exact (a1 + a2, b). + exact (a1, b). + exact (a2, b). - - refine (_ - (_ + _) = x). + - refine (- _ + (_ + _) = x). 1-3: apply freeabgroup_in. + exact (a, b1 + b2). + exact (a, b1). @@ -67,9 +67,6 @@ Definition tensor_dist_l {A B : AbGroup} (a : A) (b b' : B) : tensor a (b + b') = tensor a b + tensor a b'. Proof. apply qglue, tr. - apply sgt_inv'. - rewrite ab_neg_op. - rewrite grp_inv_inv. apply sgt_in. right. by exists a, b, b'. @@ -80,9 +77,6 @@ Definition tensor_dist_r {A B : AbGroup} (a a' : A) (b : B) : tensor (a + a') b = tensor a b + tensor a' b. Proof. apply qglue, tr. - apply sgt_inv'. - rewrite ab_neg_op. - rewrite grp_inv_inv. apply sgt_in. left. by exists a, a', b. @@ -110,35 +104,23 @@ Defined. (** Tensors preserve negation in the left argument. *) Definition tensor_neg_l {A B : AbGroup} (a : A) (b : B) - : tensor (-a) b = - tensor a b. -Proof. - change (grp_homo_tensor_r b (-a) = - tensor a b). - by rewrite grp_homo_inv. -Defined. + : tensor (-a) b = - tensor a b + := grp_homo_inv (grp_homo_tensor_r b) a. (** Tensors preserve negation in the right argument. *) Definition tensor_neg_r {A B : AbGroup} (a : A) (b : B) - : tensor a (-b) = - tensor a b. -Proof. - change (grp_homo_tensor_l a (-b) = - tensor a b). - by rewrite grp_homo_inv. -Defined. + : tensor a (-b) = - tensor a b + := grp_homo_inv (grp_homo_tensor_l a) b. (** Tensoring by zero on the left is zero. *) Definition tensor_zero_l {A B : AbGroup} (b : B) - : tensor (A:=A) 0 b = 0. -Proof. - change (grp_homo_tensor_r (A:=A) b 0 = 0). - nrapply grp_homo_unit. -Defined. + : tensor (A:=A) 0 b = 0 + := grp_homo_unit (grp_homo_tensor_r b). (** Tensoring by zero on the right is zero. *) Definition tensor_zero_r {A B : AbGroup} (a : A) - : tensor (B:=B) a 0 = 0. -Proof. - change (grp_homo_tensor_l (B:=B) a 0 = 0). - nrapply grp_homo_unit. -Defined. + : tensor (B:=B) a 0 = 0 + := grp_homo_unit (grp_homo_tensor_l a). (** The [tensor] map is bilinear and therefore can be written in a curried form using the internal abelian group hom. *) Definition grp_homo_tensor `{Funext} {A B : AbGroup} @@ -169,25 +151,18 @@ Definition ab_tensor_prod_rec_helper {A B C : AbGroup} (x : FreeAbGroup (A * B)) (insg : subgroup_biadditive_pairs x) : grp_homo_abel_rec (FreeGroup_rec (A * B) C (uncurry f)) x = mon_unit. Proof. + set (abel_rec := grp_homo_abel_rec (FreeGroup_rec (A * B) C (uncurry f))). strip_truncations. - induction insg as - [ x [ [ a [ a' [ b p ] ] ] | [ a [ b [ b' p ] ] ] ] - | - | ? ? ? H1 ? H2 ]. - - destruct p. - rewrite grp_homo_op. - rewrite grp_homo_inv. - apply grp_moveL_1M^-1%equiv. - exact (r a a' b). - - destruct p. - rewrite grp_homo_op. - rewrite grp_homo_inv. - apply grp_moveL_1M^-1%equiv. - exact (l a b b'). + induction insg as [ x biad | | g h insg_g IHg insg_h IHh ]. + - destruct biad as [ [ a [ a' [ b p ] ] ] | [ a [ b [ b' p ] ] ] ]. + all: destruct p; simpl. + all: apply grp_moveL_M1^-1%equiv; symmetry. + 1: apply r. + apply l. - nrapply grp_homo_unit. - rewrite grp_homo_op, grp_homo_inv. apply grp_moveL_1M^-1. - exact(H1 @ H2^). + exact (IHg @ IHh^). Defined. Opaque ab_tensor_prod_rec_helper. @@ -218,19 +193,22 @@ Proof. unfold ab_tensor_prod. srapply grp_quotient_ind_hprop. srapply Abel_ind_hprop; cbn beta. + set (tensor_in := grp_quotient_map $o abel_unit : FreeGroup (A * B) $-> ab_tensor_prod A B). + change (forall x, P (tensor_in x)). srapply FreeGroup_ind_hprop'; intros w; cbn beta. induction w. - - exact (transport P (tensor_zero_l 0) (Hin 0 0)). - - destruct a as [[a b]|[a b]]. - + change (P (grp_quotient_map (abel_unit (freegroup_in (a, b) + freegroup_eta w)))). - (* Both [rewrite]s are [reflexivity], but the [Defined] is slow if [change] is used instead. *) - rewrite 2 grp_homo_op. + - (* The goal here is [P 0], so we use [Hin 0 0 : P (tensor 0 0)]. *) + exact (transport P (tensor_zero_l 0) (Hin 0 0)). + - change (P (tensor_in (freegroup_eta [a]%list + freegroup_eta w))). + (* This [rewrite] is [reflexivity], but the [Defined] is slow if [change] is used instead. *) + rewrite grp_homo_op. + destruct a as [[a b]|[a b]]. + + change (P (tensor_in (freegroup_in (a, b)) + tensor_in (freegroup_eta w))). apply Hop; trivial. apply Hin. - + change (P (grp_quotient_map (abel_unit (- freegroup_in (a, b) + freegroup_eta w)))). - (* The [rewrite]s on the next two lines are all reflexivity. *) - rewrite 2 grp_homo_op. - rewrite 2 grp_homo_inv. + + change (P (tensor_in (- freegroup_in (a, b)) + tensor_in (freegroup_eta w))). + (* This [rewrite] is also reflexivity. *) + rewrite grp_homo_inv. apply Hop; trivial. rewrite <- tensor_neg_l. apply Hin. @@ -616,7 +594,7 @@ Proof. * intros a z z'; cbn beta. nrapply grp_homo_op. * intros a a' z; cbn beta. - apply (grp_homo_op (ab_mul z)). + nrapply (grp_homo_op (ab_mul z)). + hnf. change (forall x : ?A, (grp_homo_map ?f) ((grp_homo_map ?g) x) = x) with (f $o g $== Id _). @@ -671,7 +649,7 @@ Proof. intros A B. snrapply ab_tensor_prod_ind_homotopy_triple. intros a b z. - exact (tensor_ab_mul _ _ _)^. + exact (tensor_ab_mul z a b)^. Defined. (** The hexagon identity is also straighforward to prove. We simply have to reduce all the involved functions on the simple tensors using our custom triple tensor induction principle. *) From 25a60a4154b340bd56b02a62b186759fc7a4822d Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Mon, 22 Jul 2024 13:48:06 -0400 Subject: [PATCH 40/44] TensorProduct.v: updates to comments --- theories/Algebra/AbGroups/TensorProduct.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index e1cb8fc3c5b..3ceb3daf73a 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -16,9 +16,9 @@ Local Open Scope mc_add_scope. (** * The Tensor Product of Abelian Groups *) -(** Various maps [A * B → C] from the cartesian product of two abelian groups to another abelian group are "biadditive", meaning that they are group homomorphisms when we fix the left or right argument. +(** Various maps [A * B → C] from the cartesian product of two abelian groups to another abelian group are "biadditive" (also called "bilinear"), meaning that they are group homomorphisms when we fix the left or right argument. -The tensor product of abelian groups is a construction that produces an abelian group [A ⊗ B] along with a biadditive map [A * B -> A ⊗ B] which is initial among biadditive maps from [A * B]. This means that any bilinear map [A * B → C] factors uniquely through the tensor product via a group homomorphism [A ⊗ B -> C]. +The tensor product of abelian groups is a construction that produces an abelian group [A ⊗ B] along with a biadditive map [A * B -> A ⊗ B] which is initial among biadditive maps from [A * B]. This means that any biadditive map [A * B → C] factors uniquely through the tensor product via a group homomorphism [A ⊗ B -> C]. Biadditive functions appear in all sorts of contexts ranging from linear algebra to analysis. Therefore having a way to systematically study them is very useful. *) @@ -54,13 +54,13 @@ Definition ab_tensor_prod (A B : AbGroup) : AbGroup Arguments ab_tensor_prod A B : simpl never. -(** The tensor product of [A] and [B] contains formal combinations of pairs of elements from [A] and [B]. We denote these pairs as "simple tensors" and name them [tensor]. *) +(** The tensor product of [A] and [B] contains formal sums and differences of pairs of elements from [A] and [B]. We denote these pairs as "simple tensors" and name them [tensor]. *) Definition tensor {A B : AbGroup} : A -> B -> ab_tensor_prod A B := fun a b => grp_quotient_map (freeabgroup_in (a, b)). (** ** Properties of tensors *) -(** The characterizing property of simple tensors are that they are bilinear in their arguments. *) +(** The characterizing property of simple tensors are that they are biadditive in their arguments. *) (** A [tensor] of a sum distributes over the sum on the left. *) Definition tensor_dist_l {A B : AbGroup} (a : A) (b b' : B) @@ -122,7 +122,7 @@ Definition tensor_zero_r {A B : AbGroup} (a : A) : tensor (B:=B) a 0 = 0 := grp_homo_unit (grp_homo_tensor_l a). -(** The [tensor] map is bilinear and therefore can be written in a curried form using the internal abelian group hom. *) +(** The [tensor] map is biadditive and therefore can be written in a curried form using the internal abelian group hom. *) Definition grp_homo_tensor `{Funext} {A B : AbGroup} : A $-> ab_hom B (ab_tensor_prod A B). Proof. @@ -141,7 +141,7 @@ Defined. (** Here we write down some induction principles to help us prove lemmas about the tensor product. Some of these are quite specialised but are patterns that appear often in practice. *) -(** Our main recursion principle states that in order to build a homomorphism out of the tensor product, it is sufficient to provide a map out of the direct product which is bilinear, that is, a map that preserves addition in both arguments of the product. *) +(** Our main recursion principle states that in order to build a homomorphism out of the tensor product, it is sufficient to provide a map out of the direct product which is biadditive, that is, a map that preserves addition in each argument of the product. *) (** We separate out the proof of this part, so we can make it opaque. *) Definition ab_tensor_prod_rec_helper {A B C : AbGroup} @@ -250,7 +250,7 @@ Proof. - exact Hop. Defined. -(** Similar to before, we specialise the triple tensor induction principle for proving homotopies of trilinear functions. *) +(** Similar to before, we specialise the triple tensor induction principle for proving homotopies of trilinear/triadditive functions. *) Definition ab_tensor_prod_ind_homotopy_triple {A B C G : AbGroup} {f f' : ab_tensor_prod A (ab_tensor_prod B C) $-> G} (H : forall a b c, f (tensor a (tensor b c)) = f' (tensor a (tensor b c))) @@ -261,7 +261,7 @@ Proof. - intros x y; apply grp_homo_op_agree. Defined. -(** As explained for the bilinear and trilinear cases, we also derive an induction principle for quadruple tensors giving us dependent quadrilinear maps. *) +(** As explained for the biadditive and triadditive cases, we also derive an induction principle for quadruple tensors giving us dependent quadrilinear maps. *) Definition ab_tensor_prod_ind_hprop_quad {A B C D : AbGroup} (P : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) -> Type) (H : forall x, IsHProp (P x)) From aed0f0db027abbad94793fa8b15dfb5063666938 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Mon, 22 Jul 2024 13:50:18 -0400 Subject: [PATCH 41/44] Abelianization.v: minor stylistic changes --- theories/Algebra/AbGroups/Abelianization.v | 37 ++++++++++++++-------- 1 file changed, 24 insertions(+), 13 deletions(-) diff --git a/theories/Algebra/AbGroups/Abelianization.v b/theories/Algebra/AbGroups/Abelianization.v index f84631ea01d..e30e3127cd1 100644 --- a/theories/Algebra/AbGroups/Abelianization.v +++ b/theories/Algebra/AbGroups/Abelianization.v @@ -99,8 +99,8 @@ Section Abel. (** We can derive the induction principle from the ones for truncation and the coequalizer. *) Definition Abel_ind (P : Abel -> Type) `{forall x, IsHSet (P x)} - (a : forall x, P (abel_in x)) (c : forall x y z, DPath P (abel_in_comm x y z) - (a (x * (y * z))) (a (x * (z * y)))) + (a : forall x, P (abel_in x)) + (c : forall x y z, DPath P (abel_in_comm x y z) (a (x * (y * z))) (a (x * (z * y)))) : forall (x : Abel), P x. Proof. srapply Trunc_ind. @@ -111,19 +111,28 @@ Section Abel. apply c. Defined. - (** The computation rule can also be proven. *) - Definition Abel_ind_beta_abel_in_comm (P : Abel -> Type) - `{forall x, IsHSet (P x)}(a : forall x, P (abel_in x)) - (c : forall x y z, DPath P (abel_in_comm x y z) - (a (x * (y * z))) (a (x * (z * y)))) - (x y z : G) : apD (Abel_ind P a c) (abel_in_comm x y z) = c x y z. + (** The computation rule on point constructors holds definitionally. *) + Definition Abel_ind_beta_abel_in (P : Abel -> Type) `{forall x, IsHSet (P x)} + (a : forall x, P (abel_in x)) + (c : forall x y z, DPath P (abel_in_comm x y z) (a (x * (y * z))) (a (x * (z * y)))) + (x : G) + : Abel_ind P a c (abel_in x) = a x + := idpath. + + (** The computation rule on paths. *) + Definition Abel_ind_beta_abel_in_comm (P : Abel -> Type) `{forall x, IsHSet (P x)} + (a : forall x, P (abel_in x)) + (c : forall x y z, DPath P (abel_in_comm x y z) (a (x * (y * z))) (a (x * (z * y)))) + (x y z : G) + : apD (Abel_ind P a c) (abel_in_comm x y z) = c x y z. Proof. refine (apD_compose' tr _ _ @ ap _ _ @ concat_V_pp _ _). rapply Coeq_ind_beta_cglue. Defined. (** We also have a recursion princple. *) - Definition Abel_rec (P : Type) `{IsHSet P} (a : G -> P) + Definition Abel_rec (P : Type) `{IsHSet P} + (a : G -> P) (c : forall x y z, a (x * (y * z)) = a (x * (z * y))) : Abel -> P. Proof. @@ -131,9 +140,10 @@ Section Abel. intros; apply dp_const, c. Defined. - (** Here is a simpler version of Abel_ind when our target is an HProp. This lets us discard all the higher paths. *) + (** Here is a simpler version of [Abel_ind] when our target is an [HProp]. This lets us discard all the higher paths. *) Definition Abel_ind_hprop (P : Abel -> Type) `{forall x, IsHProp (P x)} - (a : forall x, P (abel_in x)) : forall (x : Abel), P x. + (a : forall x, P (abel_in x)) + : forall (x : Abel), P x. Proof. srapply (Abel_ind _ a). intros; apply path_ishprop. @@ -141,7 +151,8 @@ Section Abel. (** And its recursion version. *) Definition Abel_rec_hprop (P : Type) `{IsHProp P} - (a : G -> P) : Abel -> P. + (a : G -> P) + : Abel -> P. Proof. apply (Abel_rec _ a). intros; apply path_ishprop. @@ -383,7 +394,7 @@ Global Instance issurj_isabelianization {G : Group} Proof. intros k. pose (homotopic_isabelianization A (abel G) eta abel_unit) as p. - refine (@cancelL_isequiv_conn_map _ _ _ _ _ _ _ + exact (@cancelL_isequiv_conn_map _ _ _ _ _ _ _ (conn_map_homotopic _ _ _ p _)). Defined. From 49c2b7e86080ad9c52c66042f3302dfe83924c5f Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Mon, 22 Jul 2024 13:58:35 -0400 Subject: [PATCH 42/44] TensorProduct: speed up some *ind_hprop* lines --- theories/Algebra/AbGroups/TensorProduct.v | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index 3ceb3daf73a..c8b34223633 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -220,7 +220,8 @@ Definition ab_tensor_prod_ind_homotopy {A B G : AbGroup} (H : forall a b, f (tensor a b) = f' (tensor a b)) : f $== f'. Proof. - rapply ab_tensor_prod_ind_hprop. + nrapply ab_tensor_prod_ind_hprop. + - exact _. - exact H. - intros x y; apply grp_homo_op_agree. Defined. @@ -256,7 +257,8 @@ Definition ab_tensor_prod_ind_homotopy_triple {A B C G : AbGroup} (H : forall a b c, f (tensor a (tensor b c)) = f' (tensor a (tensor b c))) : f $== f'. Proof. - rapply ab_tensor_prod_ind_hprop_triple. + nrapply ab_tensor_prod_ind_hprop_triple. + - exact _. - exact H. - intros x y; apply grp_homo_op_agree. Defined. @@ -271,7 +273,8 @@ Definition ab_tensor_prod_ind_hprop_quad {A B C D : AbGroup} Proof. rapply (ab_tensor_prod_ind_hprop P). - intros a. - rapply (ab_tensor_prod_ind_hprop_triple (fun x => P (tensor _ x))). + nrapply (ab_tensor_prod_ind_hprop_triple (fun x => P (tensor _ x))). + + intro x; apply H. + nrapply Hin. + intros x y Hx Hy. rewrite tensor_dist_l. @@ -286,7 +289,8 @@ Definition ab_tensor_prod_ind_homotopy_quad {A B C D G : AbGroup} = f' (tensor a (tensor b (tensor c d)))) : f $== f'. Proof. - rapply (ab_tensor_prod_ind_hprop_quad (fun _ => _)). + nrapply (ab_tensor_prod_ind_hprop_quad (fun _ => _)). + - exact _. - exact H. - intros x y; apply grp_homo_op_agree. Defined. From a2f3382dfee96ef21781bf7e9f8d4506ea902d90 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 22 Jul 2024 22:42:50 +0200 Subject: [PATCH 43/44] remove redundant quotient_abgroup_map Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/AbelianGroup.v | 6 ------ 1 file changed, 6 deletions(-) diff --git a/theories/Algebra/AbGroups/AbelianGroup.v b/theories/Algebra/AbGroups/AbelianGroup.v index 0aaffdc9197..2dbff11b801 100644 --- a/theories/Algebra/AbGroups/AbelianGroup.v +++ b/theories/Algebra/AbGroups/AbelianGroup.v @@ -108,12 +108,6 @@ Definition QuotientAbGroup (G : AbGroup) (H : Subgroup G) : AbGroup Arguments QuotientAbGroup G H : simpl never. -Definition quotient_abgroup_map (G : AbGroup) (H : Subgroup G) - : GroupHomomorphism G (QuotientAbGroup G H). -Proof. - snrapply grp_quotient_map. -Defined. - Definition quotient_abgroup_rec {G : AbGroup} (N : Subgroup G) (H : AbGroup) (f : GroupHomomorphism G H) (h : forall n : G, N n -> f n = mon_unit) From ade3c4325cf7d5ebeafb638bc630ab6418c3336c Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 22 Jul 2024 22:45:13 +0200 Subject: [PATCH 44/44] fix wording in comment Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/TensorProduct.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v index c8b34223633..ced3538649d 100644 --- a/theories/Algebra/AbGroups/TensorProduct.v +++ b/theories/Algebra/AbGroups/TensorProduct.v @@ -471,7 +471,7 @@ Proof. reflexivity. Defined. -(** The data of swap together gives us a symmetric braiding on the category of abelian groups. We will later show it is a full symmetric monoidal category. *) +(** The swap map gives us a symmetric braiding on the category of abelian groups. We will later show it is a full symmetric monoidal category. *) Global Instance symmetricbraiding_ab_tensor_prod : SymmetricBraiding ab_tensor_prod. Proof. snrapply Build_SymmetricBraiding.