From d7356e94ada739cc198374280a91f2ee0ead4af4 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sun, 29 Dec 2024 17:12:56 +0000 Subject: [PATCH 01/12] constructors and functoriality for GroupCoeq Signed-off-by: Ali Caglayan --- theories/Algebra/Groups/GroupCoeq.v | 88 ++++++++++++++++++++++++++--- 1 file changed, 81 insertions(+), 7 deletions(-) diff --git a/theories/Algebra/Groups/GroupCoeq.v b/theories/Algebra/Groups/GroupCoeq.v index ee59a0f828..9cd372262b 100644 --- a/theories/Algebra/Groups/GroupCoeq.v +++ b/theories/Algebra/Groups/GroupCoeq.v @@ -4,17 +4,51 @@ Require Import Truncations.Core. Require Import Algebra.Groups.Group. Require Import Colimits.Coeq. Require Import Algebra.Groups.FreeProduct. +Require Import List.Core. + +Local Open Scope mc_scope. +Local Open Scope mc_mult_scope. (** Coequalizers of group homomorphisms *) Definition GroupCoeq {A B : Group} (f g : A $-> B) : Group. Proof. - rapply (AmalgamatedFreeProduct (FreeProduct A A) A B). - 1,2: apply FreeProduct_rec. - + exact grp_homo_id. - + exact grp_homo_id. - + exact f. - + exact g. + nrapply (AmalgamatedFreeProduct (FreeProduct A A) A B). + - exact (FreeProduct_rec (Id _) (Id _)). + - exact (FreeProduct_rec f g). +Defined. + +Definition groupcoeq_in {A B : Group} {f g : A $-> B} + : B $-> GroupCoeq f g + := amal_inr. + +Definition groupcoeq_glue {A B : Group} {f g : A $-> B} + : groupcoeq_in (f:=f) (g:=g) $o f $== groupcoeq_in $o g. +Proof. + intros x; simpl. + rewrite <- (right_identity (f x)). + rewrite <- (right_identity (g x)). + rhs_V nrapply (amal_glue (freeproduct_inr x)). + symmetry. + nrapply (amal_glue (freeproduct_inl x)). +Defined. + +Definition groupcoeq_rec {A B C : Group} (f g : A $-> B) + (h : B $-> C) (p : h $o f $== h $o g) + : GroupCoeq f g $-> C. +Proof. + snrapply AmalgamatedFreeProduct_rec. + - exact (h $o f). + - exact h. + - snrapply freeproduct_ind_homotopy. + + change (?f1 $o ?f2 $o ?f3 $o ?f4 $== ?f5 $o ?f6 $o ?f7) + with (f1 $o f2 $o (f3 $o f4) $== f5 $o (f6 $o f7)). + exact ((_ $@L freeproduct_rec_beta_inl _ _) $@ cat_idr _ + $@ (_ $@L freeproduct_rec_beta_inl _ _)^$). + + change (?f1 $o ?f2 $o ?f3 $o ?f4 $== ?f5 $o ?f6 $o ?f7) + with (f1 $o f2 $o (f3 $o f4) $== f5 $o (f6 $o f7)). + exact ((_ $@L freeproduct_rec_beta_inr _ _) $@ (cat_idr _ $@ p) + $@ (_ $@L freeproduct_rec_beta_inr _ _)^$). Defined. Definition equiv_groupcoeq_rec `{Funext} {A B C : Group} (f g : GroupHomomorphism A B) @@ -55,6 +89,46 @@ Proof. pose (q1 := p (freeproduct_inl y)). simpl in q1. rewrite 2 right_identity in q1. - exact q1^. } + symmetry. + exact q1. } hnf; intros; apply path_ishprop. Defined. + +Definition groupcoeq_ind_hprop {G H : Group} {f g : G $-> H} + (P : GroupCoeq f g -> Type) `{forall x, IsHProp (P x)} + (c : forall h, P (groupcoeq_in h)) + (Hop : forall x y, P x -> P y -> P (x * y)) + : forall x, P x. +Proof. + srapply amalgamatedfreeproduct_ind_hprop. + - intros x. + rewrite <- (right_identity x). + refine ((amal_glue (freeproduct_inl x))^ #_). + simpl. + rewrite (right_identity (f x)). + exact (c (f x)). + - exact c. + - exact Hop. +Defined. + +Definition groupcoeq_ind_homotopy {G H K : Group} {f g : G $-> H} + {h h' : GroupCoeq f g $-> K} + (r : h $o groupcoeq_in $== h' $o groupcoeq_in) + : h $== h'. +Proof. + rapply (groupcoeq_ind_hprop _ r). + intros x y p q; by nrapply grp_homo_op_agree. +Defined. + +Definition functor_groupcoeq + {G H : Group} {f g : G $-> H} {G' H' : Group} {f' g' : G' $-> H'} + (h : G $-> G') (k : H $-> H') + (p : k $o f $== f' $o h) (q : k $o g $== g' $o h) + : GroupCoeq f g $-> GroupCoeq f' g'. +Proof. + refine (groupcoeq_rec f g (groupcoeq_in $o k) _). + refine (cat_assoc _ _ _ $@ _ $@ cat_assoc_opp _ _ _). + refine ((_ $@L p) $@ _ $@ (_ $@L q^$)). + refine (cat_assoc_opp _ _ _ $@ (_ $@R _) $@ cat_assoc _ _ _). + apply groupcoeq_glue. +Defined. From d159e726282ce20d9ca83f0fbda7eb13baf4c291 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Tue, 7 Jan 2025 13:19:09 +0000 Subject: [PATCH 02/12] replace ugly change with explicit wildcat term Signed-off-by: Ali Caglayan --- theories/Algebra/Groups/GroupCoeq.v | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/theories/Algebra/Groups/GroupCoeq.v b/theories/Algebra/Groups/GroupCoeq.v index 9cd372262b..76029206ea 100644 --- a/theories/Algebra/Groups/GroupCoeq.v +++ b/theories/Algebra/Groups/GroupCoeq.v @@ -41,12 +41,10 @@ Proof. - exact (h $o f). - exact h. - snrapply freeproduct_ind_homotopy. - + change (?f1 $o ?f2 $o ?f3 $o ?f4 $== ?f5 $o ?f6 $o ?f7) - with (f1 $o f2 $o (f3 $o f4) $== f5 $o (f6 $o f7)). + + refine (cat_assoc _ _ _ $@ _ $@ cat_assoc_opp _ _ _). exact ((_ $@L freeproduct_rec_beta_inl _ _) $@ cat_idr _ $@ (_ $@L freeproduct_rec_beta_inl _ _)^$). - + change (?f1 $o ?f2 $o ?f3 $o ?f4 $== ?f5 $o ?f6 $o ?f7) - with (f1 $o f2 $o (f3 $o f4) $== f5 $o (f6 $o f7)). + + refine (cat_assoc _ _ _ $@ _ $@ cat_assoc_opp _ _ _). exact ((_ $@L freeproduct_rec_beta_inr _ _) $@ (cat_idr _ $@ p) $@ (_ $@L freeproduct_rec_beta_inr _ _)^$). Defined. From bd5c53b2f0c2f21cba89a28891f67a5d896635c0 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Mon, 17 Feb 2025 16:43:17 -0500 Subject: [PATCH 03/12] Groups/FreeProduct: use $-> to simplify later goals; change WildCat imports --- theories/Algebra/Groups/FreeProduct.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/theories/Algebra/Groups/FreeProduct.v b/theories/Algebra/Groups/FreeProduct.v index 4612c31073..48304cc76f 100644 --- a/theories/Algebra/Groups/FreeProduct.v +++ b/theories/Algebra/Groups/FreeProduct.v @@ -1,10 +1,10 @@ Require Import Basics Types. +Require Import WildCat.Core WildCat.Coproducts. Require Import Cubical.DPath. Require Import Spaces.List.Core Spaces.List.Theory. Require Import Colimits.Pushout. Require Import Truncations.Core Truncations.SeparatedTrunc. Require Import Algebra.Groups.Group. -Require Import WildCat. Local Open Scope list_scope. Local Open Scope mc_scope. @@ -624,8 +624,8 @@ Section FreeProduct. Defined. Theorem equiv_amalgamatedfreeproduct_rec `{Funext} (X : Group) - : {h : GroupHomomorphism H X & {k : GroupHomomorphism K X & h o f == k o g }} - <~> GroupHomomorphism AmalgamatedFreeProduct X. + : {h : H $-> X & {k : K $-> X & h o f == k o g }} + <~> (AmalgamatedFreeProduct $-> X). Proof. snapply equiv_adjointify. 1: intros [h [k p]]; exact (AmalgamatedFreeProduct_rec X h k p). @@ -650,8 +650,8 @@ Section FreeProduct. rapply (grp_homo_op r (amal_eta [_]) (amal_eta x)). } intro hkp. simpl. - rapply (equiv_ap' (equiv_sigma_prod - (fun hk : GroupHomomorphism H X * GroupHomomorphism K X + tapply (equiv_ap' (equiv_sigma_prod + (fun hk : (H $-> X) * (K $-> X) => fst hk o f == snd hk o g)) _ _)^-1%equiv. rapply path_sigma_hprop. destruct hkp as [h [k p]]. From ebb73ffb7e5f73beb8cf7fff5e668f0411968804 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Mon, 17 Feb 2025 16:43:44 -0500 Subject: [PATCH 04/12] GroupCoeq: slightly simplify one proof --- theories/Algebra/Groups/GroupCoeq.v | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) diff --git a/theories/Algebra/Groups/GroupCoeq.v b/theories/Algebra/Groups/GroupCoeq.v index 76029206ea..3ac2f6c6db 100644 --- a/theories/Algebra/Groups/GroupCoeq.v +++ b/theories/Algebra/Groups/GroupCoeq.v @@ -37,16 +37,14 @@ Definition groupcoeq_rec {A B C : Group} (f g : A $-> B) (h : B $-> C) (p : h $o f $== h $o g) : GroupCoeq f g $-> C. Proof. - snrapply AmalgamatedFreeProduct_rec. - - exact (h $o f). - - exact h. - - snrapply freeproduct_ind_homotopy. - + refine (cat_assoc _ _ _ $@ _ $@ cat_assoc_opp _ _ _). - exact ((_ $@L freeproduct_rec_beta_inl _ _) $@ cat_idr _ - $@ (_ $@L freeproduct_rec_beta_inl _ _)^$). - + refine (cat_assoc _ _ _ $@ _ $@ cat_assoc_opp _ _ _). - exact ((_ $@L freeproduct_rec_beta_inr _ _) $@ (cat_idr _ $@ p) - $@ (_ $@L freeproduct_rec_beta_inr _ _)^$). + rapply (AmalgamatedFreeProduct_rec C (h $o f) h). + snrapply freeproduct_ind_homotopy. + - refine (cat_assoc _ _ _ $@ _ $@ cat_assoc_opp _ _ _). + exact ((_ $@L freeproduct_rec_beta_inl _ _) $@ cat_idr _ + $@ (_ $@L freeproduct_rec_beta_inl _ _)^$). + - refine (cat_assoc _ _ _ $@ _ $@ cat_assoc_opp _ _ _). + exact ((_ $@L freeproduct_rec_beta_inr _ _) $@ (cat_idr _ $@ p) + $@ (_ $@L freeproduct_rec_beta_inr _ _)^$). Defined. Definition equiv_groupcoeq_rec `{Funext} {A B C : Group} (f g : GroupHomomorphism A B) From 9193956edbb7d0f070a3681d828e41caff61e342 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Tue, 18 Feb 2025 07:55:14 -0500 Subject: [PATCH 05/12] FreeProduct: change Global Instances to Local --- theories/Algebra/Groups/FreeProduct.v | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/theories/Algebra/Groups/FreeProduct.v b/theories/Algebra/Groups/FreeProduct.v index 48304cc76f..5d56f5e7e0 100644 --- a/theories/Algebra/Groups/FreeProduct.v +++ b/theories/Algebra/Groups/FreeProduct.v @@ -273,7 +273,7 @@ Section FreeProduct. (** Now for the group structure *) (** The group operation is concatenation of the underlying list. Most of the work is spent showing that it respects the path constructors. *) - #[export] Instance sgop_amal_type : SgOp amal_type. + Local Instance sgop_amal_type : SgOp amal_type. Proof. intros x y; revert x. srapply amal_type_rec; intros x; revert y. @@ -350,12 +350,12 @@ Section FreeProduct. Defined. (** The identity element is the empty list *) - #[export] Instance monunit_amal_type : MonUnit amal_type. + Local Instance monunit_amal_type : MonUnit amal_type. Proof. exact (amal_eta nil). Defined. - #[export] Instance inverse_amal_type : Inverse amal_type. + Local Instance inverse_amal_type : Inverse amal_type. Proof. srapply amal_type_rec. { intros w. @@ -420,7 +420,7 @@ Section FreeProduct. apply amal_omega_K. } Defined. - #[export] Instance associative_sgop_m : Associative sg_op. + Local Instance associative_sgop_m : Associative sg_op. Proof. intros x y. rapply amal_type_ind_hprop; intro z; revert y. @@ -430,13 +430,13 @@ Section FreeProduct. rapply app_assoc. Defined. - #[export] Instance leftidentity_sgop_amal_type : LeftIdentity sg_op mon_unit. + Local Instance leftidentity_sgop_amal_type : LeftIdentity sg_op mon_unit. Proof. rapply amal_type_ind_hprop; intro x. reflexivity. Defined. - #[export] Instance rightidentity_sgop_amal_type : RightIdentity sg_op mon_unit. + Local Instance rightidentity_sgop_amal_type : RightIdentity sg_op mon_unit. Proof. rapply amal_type_ind_hprop; intro x. napply (ap amal_eta). @@ -505,13 +505,13 @@ Section FreeProduct. apply amal_omega_K. Defined. - #[export] Instance leftinverse_sgop_amal_type : LeftInverse (.*.) (^) mon_unit. + Local Instance leftinverse_sgop_amal_type : LeftInverse (.*.) (^) mon_unit. Proof. rapply amal_type_ind_hprop; intro x. apply amal_eta_word_concat_Vw. Defined. - #[export] Instance rightinverse_sgop_amal_type : RightInverse (.*.) (^) mon_unit. + Local Instance rightinverse_sgop_amal_type : RightInverse (.*.) (^) mon_unit. Proof. rapply amal_type_ind_hprop; intro x. apply amal_eta_word_concat_wV. @@ -564,7 +564,7 @@ Section FreeProduct. rapply left_identity. } Defined. - #[export] Instance issemigrouppreserving_AmalgamatedFreeProduct_rec' + Local Instance issemigrouppreserving_AmalgamatedFreeProduct_rec' (X : Group) (h : GroupHomomorphism H X) (k : GroupHomomorphism K X) (p : h o f == k o g) : IsSemiGroupPreserving (AmalgamatedFreeProduct_rec' X h k p). From 2e82f4273e5865bcf8edfb591574441efccb15ca Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 24 Feb 2025 20:28:58 +0000 Subject: [PATCH 06/12] add comment about unifying equiv_groupcoeq_rec Signed-off-by: Ali Caglayan --- theories/Algebra/Groups/GroupCoeq.v | 1 + 1 file changed, 1 insertion(+) diff --git a/theories/Algebra/Groups/GroupCoeq.v b/theories/Algebra/Groups/GroupCoeq.v index 3ac2f6c6db..0dc8637a59 100644 --- a/theories/Algebra/Groups/GroupCoeq.v +++ b/theories/Algebra/Groups/GroupCoeq.v @@ -47,6 +47,7 @@ Proof. $@ (_ $@L freeproduct_rec_beta_inr _ _)^$). Defined. +(** TODO: unify this with [groupcoeq_rec]. It will require doing the analagous thing for [AmalgamatedFreeProduct]. *) Definition equiv_groupcoeq_rec `{Funext} {A B C : Group} (f g : GroupHomomorphism A B) : {h : B $-> C & h o f == h o g} <~> (GroupCoeq f g $-> C). Proof. From dc15a84b86a566bf6a9563a2583b8570ad2e958f Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 24 Feb 2025 20:31:26 +0000 Subject: [PATCH 07/12] add comment about complicated wildcat term Signed-off-by: Ali Caglayan --- theories/Algebra/Groups/GroupCoeq.v | 1 + 1 file changed, 1 insertion(+) diff --git a/theories/Algebra/Groups/GroupCoeq.v b/theories/Algebra/Groups/GroupCoeq.v index 0dc8637a59..b20b59ab1b 100644 --- a/theories/Algebra/Groups/GroupCoeq.v +++ b/theories/Algebra/Groups/GroupCoeq.v @@ -39,6 +39,7 @@ Definition groupcoeq_rec {A B C : Group} (f g : A $-> B) Proof. rapply (AmalgamatedFreeProduct_rec C (h $o f) h). snrapply freeproduct_ind_homotopy. + (** The goals generated are very simple, but we give explicit proofs with wild cat terms to stop Coq from unfolding terms when checking the proof. Note that the category of groups is definitionally associative. *) - refine (cat_assoc _ _ _ $@ _ $@ cat_assoc_opp _ _ _). exact ((_ $@L freeproduct_rec_beta_inl _ _) $@ cat_idr _ $@ (_ $@L freeproduct_rec_beta_inl _ _)^$). From d0c7d0528250cefe22b187fbf9b2f54b7a87f0a7 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 24 Feb 2025 21:48:56 +0000 Subject: [PATCH 08/12] improve proof of equiv_groupcoeq_rec Signed-off-by: Ali Caglayan --- theories/Algebra/Groups/FreeProduct.v | 37 ++++++++++++----- theories/Algebra/Groups/GroupCoeq.v | 60 ++++++++++----------------- 2 files changed, 48 insertions(+), 49 deletions(-) diff --git a/theories/Algebra/Groups/FreeProduct.v b/theories/Algebra/Groups/FreeProduct.v index 5d56f5e7e0..572eba875c 100644 --- a/theories/Algebra/Groups/FreeProduct.v +++ b/theories/Algebra/Groups/FreeProduct.v @@ -14,6 +14,7 @@ Local Open Scope mc_mult_scope. (** We wish to define the amalgamated free product of a span of group homomorphisms f : G -> H, g : G -> K as the following HIT: +<< HIT M(f,g) | amal_eta : list (H + K) -> M(f,g) | mu_H : forall (x y : list (H + K)) (h1 h2 : H), @@ -26,6 +27,7 @@ Local Open Scope mc_mult_scope. amal_eta (x ++ [inl mon_unit] ++ y) = amal_eta (x ++ y) | omega_K : forall (x y : list (H + K)), amal_eta (x ++ [inr mon_unit] ++ y) = amal_eta (x ++ y). +>> We will build this HIT up successively out of coequalizers. *) @@ -624,7 +626,7 @@ Section FreeProduct. Defined. Theorem equiv_amalgamatedfreeproduct_rec `{Funext} (X : Group) - : {h : H $-> X & {k : K $-> X & h o f == k o g }} + : {h : H $-> X & {k : K $-> X & h $o f $== k $o g }} <~> (AmalgamatedFreeProduct $-> X). Proof. snapply equiv_adjointify. @@ -678,8 +680,8 @@ Section FreeProduct. by apply Hop. Defined. - Definition amalgamatedfreeproduct_ind_homotopy - {k k' : AmalgamatedFreeProduct $-> G} + Definition amalgamatedfreeproduct_ind_homotopy (P : Group) + {k k' : AmalgamatedFreeProduct $-> P} (l : k $o amal_inl $== k' $o amal_inl) (r : k $o amal_inr $== k' $o amal_inr) : k $== k'. @@ -688,6 +690,16 @@ Section FreeProduct. intros x y; napply grp_homo_op_agree. (* A bit slow, ~0.05s *) Defined. (* A bit slow, ~0.05s *) + Definition equiv_amalgamatedfreeproduct_ind_homotopy `{Funext} (P : Group) + (k k' : AmalgamatedFreeProduct $-> P) + : (k $o amal_inl $== k' $o amal_inl) * (k $o amal_inr $== k' $o amal_inr) + <~> k $== k'. + Proof. + rapply equiv_iff_hprop. + - exact (uncurry (amalgamatedfreeproduct_ind_homotopy P)). + - intros p; split; exact (p $@R _). + Defined. + End FreeProduct. Arguments amal_eta {G H K f g} x. @@ -695,7 +707,8 @@ Arguments amal_inl {G H K f g}. Arguments amal_inr {G H K f g}. Arguments AmalgamatedFreeProduct_rec {G H K f g}. Arguments amalgamatedfreeproduct_ind_hprop {G H K f g} _ {_}. -Arguments amalgamatedfreeproduct_ind_homotopy {G H K f g _}. +Arguments amalgamatedfreeproduct_ind_homotopy {G H K f g P k k'} l r. +Arguments equiv_amalgamatedfreeproduct_ind_homotopy {G H K f g _ P} k k'. Arguments amal_glue {G H K f g}. Definition FreeProduct (G H : Group) : Group @@ -712,7 +725,7 @@ Definition FreeProduct_rec {G H K : Group} (f : G $-> K) (g : H $-> K) Proof. snapply (AmalgamatedFreeProduct_rec _ f g). intros []. - exact (grp_homo_unit _ @ (grp_homo_unit _)^). + exact (grp_homo_unit f @ (grp_homo_unit g)^). Defined. Definition freeproduct_ind_hprop {G H} (P : FreeProduct G H -> Type) @@ -727,11 +740,15 @@ Definition freeproduct_ind_homotopy {G H K : Group} {f f' : FreeProduct G H $-> K} (l : f $o freeproduct_inl $== f' $o freeproduct_inl) (r : f $o freeproduct_inr $== f' $o freeproduct_inr) - : f $== f'. -Proof. - rapply (freeproduct_ind_hprop _ l r). - intros x y; napply grp_homo_op_agree. (* Slow, ~0.2s. *) -Defined. (* Slow, ~0.15s. *) + : f $== f' + := amalgamatedfreeproduct_ind_homotopy l r. + +Definition equiv_freeproduct_ind_homotopy {Funext : Funext} {G H K : Group} + (f f' : FreeProduct G H $-> K) + : (f $o freeproduct_inl $== f' $o freeproduct_inl) + * (f $o freeproduct_inr $== f' $o freeproduct_inr) + <~> f $== f' + := equiv_amalgamatedfreeproduct_ind_homotopy _ _. Definition freeproduct_rec_beta_inl {G H K : Group} (f : G $-> K) (g : H $-> K) diff --git a/theories/Algebra/Groups/GroupCoeq.v b/theories/Algebra/Groups/GroupCoeq.v index b20b59ab1b..66173af275 100644 --- a/theories/Algebra/Groups/GroupCoeq.v +++ b/theories/Algebra/Groups/GroupCoeq.v @@ -49,47 +49,29 @@ Proof. Defined. (** TODO: unify this with [groupcoeq_rec]. It will require doing the analagous thing for [AmalgamatedFreeProduct]. *) -Definition equiv_groupcoeq_rec `{Funext} {A B C : Group} (f g : GroupHomomorphism A B) - : {h : B $-> C & h o f == h o g} <~> (GroupCoeq f g $-> C). +Definition equiv_groupcoeq_rec `{Funext} {A B C : Group} (f g : A $-> B) + : {h : B $-> C & h $o f $== h $o g} <~> (GroupCoeq f g $-> C). Proof. - refine (equiv_amalgamatedfreeproduct_rec _ _ _ _ _ _ oE _). - refine (equiv_sigma_symm _ oE _). - apply equiv_functor_sigma_id. + nrefine (equiv_amalgamatedfreeproduct_rec _ _ _ _ _ _ oE _). + nrefine (equiv_sigma_symm _ oE _). + nrapply equiv_functor_sigma_id. intros h. - snapply equiv_adjointify. - { intros p. - exists (grp_homo_compose h f). - hnf; intro x. - refine (p _ @ _). - revert x. - rapply Trunc_ind. - srapply Coeq_ind_hprop. - intros w. hnf. - induction w. - 1: apply ap, grp_homo_unit. - simpl. - destruct a as [a|a]. - 1,2: refine (ap _ (grp_homo_op _ _ _) @ _). - 1,2: napply grp_homo_op_agree; trivial. - symmetry. - apply p. } - { intros [k p] x. - assert (q1 := p (freeproduct_inl x)). - assert (q2 := p (freeproduct_inr x)). - simpl in q1, q2. - rewrite 2 right_identity in q1, q2. - exact (q1^ @ q2). } - { hnf. intros [k p]. - apply path_sigma_hprop. - simpl. - apply equiv_path_grouphomomorphism. - intro y. - pose (q1 := p (freeproduct_inl y)). - simpl in q1. - rewrite 2 right_identity in q1. - symmetry. - exact q1. } - hnf; intros; apply path_ishprop. + transitivity {b : A $-> C & (b $== h $o f) * (b $== h $o g)}%type. + { nrefine (equiv_functor_sigma_id (fun b => equiv_sigma_prod0 _ _) oE _). + nrefine ((equiv_sigma_assoc' _ _)^-1 oE _). + transitivity {fp' : {f' : A $-> C & f' = h $o f} & fp'.1 $== h $o g}. + - refine ((@equiv_contr_sigma _ _ _)^-1 oE _). + reflexivity. + - exact (equiv_functor_sigma_pb + (equiv_functor_sigma_id (fun _ => equiv_path_grouphomomorphism))^-1). } + snrapply equiv_functor_sigma_id. + intros h'. + nrefine (equiv_freeproduct_ind_homotopy _ _ oE _). + snrapply equiv_functor_prod'. + - snrapply equiv_functor_forall_id; simpl; intros a. + by rewrite 2 grp_unit_r. + - snrapply equiv_functor_forall_id; simpl; intros a. + by rewrite 2 grp_unit_r. Defined. Definition groupcoeq_ind_hprop {G H : Group} {f g : G $-> H} From 8b63aec23d9a79bf5a2cf269fcb15ecefc511357 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Thu, 13 Mar 2025 12:47:16 -0400 Subject: [PATCH 09/12] FreeProduct, GroupCoeq: speed up/simplify some proofs --- theories/Algebra/Groups/FreeProduct.v | 13 +++++++++---- theories/Algebra/Groups/GroupCoeq.v | 17 +++++++++-------- 2 files changed, 18 insertions(+), 12 deletions(-) diff --git a/theories/Algebra/Groups/FreeProduct.v b/theories/Algebra/Groups/FreeProduct.v index 572eba875c..68cd787a50 100644 --- a/theories/Algebra/Groups/FreeProduct.v +++ b/theories/Algebra/Groups/FreeProduct.v @@ -244,7 +244,8 @@ Section FreeProduct. (e : forall w, P (amal_eta w)) : forall x, P x. Proof. - srapply amal_type_ind. + snrapply amal_type_ind. + 1: exact _. 1: exact e. all: intros; apply path_ishprop. Defined. @@ -274,12 +275,15 @@ Section FreeProduct. (** Now for the group structure *) + (** We will frequently need to use that path types in [amal_type] are hprops, and so it speeds things up to create this instance. It is fast to use [_] here, but when the terms are large below, it becomes slower. *) + Local Instance ishprop_paths_amal_type (x y : amal_type) : IsHProp (x = y) := _. + (** The group operation is concatenation of the underlying list. Most of the work is spent showing that it respects the path constructors. *) Local Instance sgop_amal_type : SgOp amal_type. Proof. intros x y; revert x. - srapply amal_type_rec; intros x; revert y. - { srapply amal_type_rec; intros y. + snrapply amal_type_rec; only 1: exact _; intros x; revert y. + { snrapply amal_type_rec; only 1: exact _; intros y. 1: exact (amal_eta (x ++ y)). { intros z h1 h2. refine (ap amal_eta _ @ _ @ ap amal_eta _^). @@ -700,7 +704,7 @@ Section FreeProduct. - intros p; split; exact (p $@R _). Defined. -End FreeProduct. +End FreeProduct. (* Slow, ~0.1s *) Arguments amal_eta {G H K f g} x. Arguments amal_inl {G H K f g}. @@ -735,6 +739,7 @@ Definition freeproduct_ind_hprop {G H} (P : FreeProduct G H -> Type) (Hop : forall x y, P x -> P y -> P (x * y)) : forall x, P x := amalgamatedfreeproduct_ind_hprop P l r Hop. +(* The above is slow, ~0.15s. *) Definition freeproduct_ind_homotopy {G H K : Group} {f f' : FreeProduct G H $-> K} diff --git a/theories/Algebra/Groups/GroupCoeq.v b/theories/Algebra/Groups/GroupCoeq.v index 66173af275..30b013ea73 100644 --- a/theories/Algebra/Groups/GroupCoeq.v +++ b/theories/Algebra/Groups/GroupCoeq.v @@ -58,14 +58,14 @@ Proof. intros h. transitivity {b : A $-> C & (b $== h $o f) * (b $== h $o g)}%type. { nrefine (equiv_functor_sigma_id (fun b => equiv_sigma_prod0 _ _) oE _). - nrefine ((equiv_sigma_assoc' _ _)^-1 oE _). + symmetry. + nrefine (_ oE (equiv_sigma_assoc' _ _)). transitivity {fp' : {f' : A $-> C & f' = h $o f} & fp'.1 $== h $o g}. - - refine ((@equiv_contr_sigma _ _ _)^-1 oE _). - reflexivity. - exact (equiv_functor_sigma_pb - (equiv_functor_sigma_id (fun _ => equiv_path_grouphomomorphism))^-1). } + (equiv_functor_sigma_id (fun _ => equiv_path_grouphomomorphism))). + - exact (@equiv_contr_sigma _ _ (contr_basedpaths' (h $o f))). } snrapply equiv_functor_sigma_id. - intros h'. + intros h'; cbn beta. nrefine (equiv_freeproduct_ind_homotopy _ _ oE _). snrapply equiv_functor_prod'. - snrapply equiv_functor_forall_id; simpl; intros a. @@ -80,7 +80,8 @@ Definition groupcoeq_ind_hprop {G H : Group} {f g : G $-> H} (Hop : forall x y, P x -> P y -> P (x * y)) : forall x, P x. Proof. - srapply amalgamatedfreeproduct_ind_hprop. + snrapply amalgamatedfreeproduct_ind_hprop. + - exact _. - intros x. rewrite <- (right_identity x). refine ((amal_glue (freeproduct_inl x))^ #_). @@ -88,8 +89,8 @@ Proof. rewrite (right_identity (f x)). exact (c (f x)). - exact c. - - exact Hop. -Defined. + - exact Hop. (* Slow, ~0.09s *) +Defined. (* Slow, ~0.09s *) Definition groupcoeq_ind_homotopy {G H K : Group} {f g : G $-> H} {h h' : GroupCoeq f g $-> K} From dd823b02264934dba28ecd2b07a356d8a2403764 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Thu, 13 Mar 2025 12:51:17 -0400 Subject: [PATCH 10/12] Move FreeProduct_rec after FreeProduct_ind* --- theories/Algebra/Groups/FreeProduct.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/theories/Algebra/Groups/FreeProduct.v b/theories/Algebra/Groups/FreeProduct.v index 68cd787a50..661e098cbd 100644 --- a/theories/Algebra/Groups/FreeProduct.v +++ b/theories/Algebra/Groups/FreeProduct.v @@ -724,14 +724,6 @@ Definition freeproduct_inl {G H : Group} : GroupHomomorphism G (FreeProduct G H) Definition freeproduct_inr {G H : Group} : GroupHomomorphism H (FreeProduct G H) := amal_inr. -Definition FreeProduct_rec {G H K : Group} (f : G $-> K) (g : H $-> K) - : FreeProduct G H $-> K. -Proof. - snapply (AmalgamatedFreeProduct_rec _ f g). - intros []. - exact (grp_homo_unit f @ (grp_homo_unit g)^). -Defined. - Definition freeproduct_ind_hprop {G H} (P : FreeProduct G H -> Type) `{forall x, IsHProp (P x)} (l : forall g, P (freeproduct_inl g)) @@ -755,6 +747,14 @@ Definition equiv_freeproduct_ind_homotopy {Funext : Funext} {G H K : Group} <~> f $== f' := equiv_amalgamatedfreeproduct_ind_homotopy _ _. +Definition FreeProduct_rec {G H K : Group} (f : G $-> K) (g : H $-> K) + : FreeProduct G H $-> K. +Proof. + srapply (AmalgamatedFreeProduct_rec _ f g). + intros []. + exact (grp_homo_unit f @ (grp_homo_unit g)^). +Defined. + Definition freeproduct_rec_beta_inl {G H K : Group} (f : G $-> K) (g : H $-> K) : FreeProduct_rec f g $o freeproduct_inl $== f From 7fdcbaf071f044c98a814cf1544f83b51c69f87b Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Sat, 15 Mar 2025 09:32:35 -0400 Subject: [PATCH 11/12] FreeProduct: split Section for speed and improve implicit arguments --- theories/Algebra/Groups/FreeProduct.v | 60 ++++++++++++++------------- theories/Algebra/Groups/GroupCoeq.v | 4 +- 2 files changed, 34 insertions(+), 30 deletions(-) diff --git a/theories/Algebra/Groups/FreeProduct.v b/theories/Algebra/Groups/FreeProduct.v index 661e098cbd..14a6594af1 100644 --- a/theories/Algebra/Groups/FreeProduct.v +++ b/theories/Algebra/Groups/FreeProduct.v @@ -33,9 +33,9 @@ Local Open Scope mc_mult_scope. (** We will call M [amal_type] and prefix all the constructors with [amal_] (for amalgamated free product). *) -Section FreeProduct. +Section AmalgamatedFreeProduct. - Context (G H K : Group) + Context {G H K : Group} (f : GroupHomomorphism G H) (g : GroupHomomorphism G K). Local Definition Words : Type := list (H + K). @@ -59,7 +59,6 @@ Section FreeProduct. destruct x; rhs napply app_assoc; f_ap. Defined. - (** There are five source types for the path constructors. We will construct this HIT as the colimit of five forks going into [Words]. We can bundle up this colimit as a single coequalizer. *) (** Source types of path constructors *) @@ -528,11 +527,25 @@ Section FreeProduct. snapply (Build_Group amal_type); repeat split; exact _. Defined. +End AmalgamatedFreeProduct. + +Arguments amal_eta {G H K f g} x. +Arguments amal_mu_H {G H K f g} x y. +Arguments amal_mu_K {G H K f g} x y. +Arguments amal_tau {G H K f g} x y z. +Arguments amal_omega_H {G H K f g} x y. +Arguments amal_omega_K {G H K f g} x y. + +Section RecInd. + + Context {G H K : Group} + {f : GroupHomomorphism G H} {g : GroupHomomorphism G K}. + (** Using foldr. It's important that we use foldr as foldl is near impossible to reason about. *) Definition AmalgamatedFreeProduct_rec' (X : Group) (h : GroupHomomorphism H X) (k : GroupHomomorphism K X) (p : h o f == k o g) - : AmalgamatedFreeProduct -> X. + : AmalgamatedFreeProduct f g -> X. Proof. srapply amal_type_rec. { intro w. @@ -593,14 +606,14 @@ Section FreeProduct. Definition AmalgamatedFreeProduct_rec (X : Group) (h : H $-> X) (k : K $-> X) (p : h $o f $== k $o g) - : AmalgamatedFreeProduct $-> X. + : AmalgamatedFreeProduct f g $-> X. Proof. snapply Build_GroupHomomorphism. 1: srapply (AmalgamatedFreeProduct_rec' X h k p). exact _. Defined. - Definition amal_inl : H $-> AmalgamatedFreeProduct. + Definition amal_inl : H $-> AmalgamatedFreeProduct f g. Proof. snapply Build_GroupHomomorphism. { intro x. @@ -612,7 +625,7 @@ Section FreeProduct. reflexivity. Defined. - Definition amal_inr : K $-> AmalgamatedFreeProduct. + Definition amal_inr : K $-> AmalgamatedFreeProduct f g. Proof. snapply Build_GroupHomomorphism. { intro x. @@ -631,7 +644,7 @@ Section FreeProduct. Theorem equiv_amalgamatedfreeproduct_rec `{Funext} (X : Group) : {h : H $-> X & {k : K $-> X & h $o f $== k $o g }} - <~> (AmalgamatedFreeProduct $-> X). + <~> (AmalgamatedFreeProduct f g $-> X). Proof. snapply equiv_adjointify. 1: intros [h [k p]]; exact (AmalgamatedFreeProduct_rec X h k p). @@ -666,7 +679,7 @@ Section FreeProduct. intro; simpl; rapply right_identity. Defined. - Definition amalgamatedfreeproduct_ind_hprop (P : AmalgamatedFreeProduct -> Type) + Definition amalgamatedfreeproduct_ind_hprop (P : AmalgamatedFreeProduct f g -> Type) `{forall x, IsHProp (P x)} (l : forall a, P (amal_inl a)) (r : forall b, P (amal_inr b)) (Hop : forall x y, P x -> P y -> P (x * y)) @@ -684,39 +697,30 @@ Section FreeProduct. by apply Hop. Defined. - Definition amalgamatedfreeproduct_ind_homotopy (P : Group) - {k k' : AmalgamatedFreeProduct $-> P} + Definition amalgamatedfreeproduct_ind_homotopy {P : Group} + {k k' : AmalgamatedFreeProduct f g $-> P} (l : k $o amal_inl $== k' $o amal_inl) (r : k $o amal_inr $== k' $o amal_inr) : k $== k'. Proof. rapply (amalgamatedfreeproduct_ind_hprop _ l r). - intros x y; napply grp_homo_op_agree. (* A bit slow, ~0.05s *) - Defined. (* A bit slow, ~0.05s *) + intros x y; napply grp_homo_op_agree. + Defined. - Definition equiv_amalgamatedfreeproduct_ind_homotopy `{Funext} (P : Group) - (k k' : AmalgamatedFreeProduct $-> P) + Definition equiv_amalgamatedfreeproduct_ind_homotopy `{Funext} {P : Group} + (k k' : AmalgamatedFreeProduct f g $-> P) : (k $o amal_inl $== k' $o amal_inl) * (k $o amal_inr $== k' $o amal_inr) <~> k $== k'. Proof. rapply equiv_iff_hprop. - - exact (uncurry (amalgamatedfreeproduct_ind_homotopy P)). + - exact (uncurry amalgamatedfreeproduct_ind_homotopy). - intros p; split; exact (p $@R _). Defined. -End FreeProduct. (* Slow, ~0.1s *) - -Arguments amal_eta {G H K f g} x. -Arguments amal_inl {G H K f g}. -Arguments amal_inr {G H K f g}. -Arguments AmalgamatedFreeProduct_rec {G H K f g}. -Arguments amalgamatedfreeproduct_ind_hprop {G H K f g} _ {_}. -Arguments amalgamatedfreeproduct_ind_homotopy {G H K f g P k k'} l r. -Arguments equiv_amalgamatedfreeproduct_ind_homotopy {G H K f g _ P} k k'. -Arguments amal_glue {G H K f g}. +End RecInd. Definition FreeProduct (G H : Group) : Group - := AmalgamatedFreeProduct grp_trivial G H (grp_trivial_rec _) (grp_trivial_rec _). + := AmalgamatedFreeProduct (grp_trivial_rec G) (grp_trivial_rec H). Definition freeproduct_inl {G H : Group} : GroupHomomorphism G (FreeProduct G H) := amal_inl. @@ -769,7 +773,7 @@ Definition equiv_freeproduct_rec `{funext : Funext} (G H K : Group) : (GroupHomomorphism G K) * (GroupHomomorphism H K) <~> GroupHomomorphism (FreeProduct G H) K. Proof. - refine (equiv_amalgamatedfreeproduct_rec _ _ _ _ _ K oE _^-1). + refine (equiv_amalgamatedfreeproduct_rec K oE _^-1). refine (equiv_sigma_prod0 _ _ oE equiv_functor_sigma_id (fun _ => equiv_sigma_contr _)). intros f. rapply contr_forall. diff --git a/theories/Algebra/Groups/GroupCoeq.v b/theories/Algebra/Groups/GroupCoeq.v index 30b013ea73..5b1def87a6 100644 --- a/theories/Algebra/Groups/GroupCoeq.v +++ b/theories/Algebra/Groups/GroupCoeq.v @@ -13,7 +13,7 @@ Local Open Scope mc_mult_scope. Definition GroupCoeq {A B : Group} (f g : A $-> B) : Group. Proof. - nrapply (AmalgamatedFreeProduct (FreeProduct A A) A B). + nrapply (@AmalgamatedFreeProduct (FreeProduct A A) A B). - exact (FreeProduct_rec (Id _) (Id _)). - exact (FreeProduct_rec f g). Defined. @@ -52,7 +52,7 @@ Defined. Definition equiv_groupcoeq_rec `{Funext} {A B C : Group} (f g : A $-> B) : {h : B $-> C & h $o f $== h $o g} <~> (GroupCoeq f g $-> C). Proof. - nrefine (equiv_amalgamatedfreeproduct_rec _ _ _ _ _ _ oE _). + nrefine (equiv_amalgamatedfreeproduct_rec C oE _). nrefine (equiv_sigma_symm _ oE _). nrapply equiv_functor_sigma_id. intros h. From 43e5cd47c1a5479df15a8a01ccb03cfa222d98e0 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Sat, 15 Mar 2025 16:10:34 -0400 Subject: [PATCH 12/12] FreeProduct, GroupCoeq: fix nrapply warnings --- theories/Algebra/Groups/FreeProduct.v | 6 +++--- theories/Algebra/Groups/GroupCoeq.v | 22 +++++++++++----------- 2 files changed, 14 insertions(+), 14 deletions(-) diff --git a/theories/Algebra/Groups/FreeProduct.v b/theories/Algebra/Groups/FreeProduct.v index 14a6594af1..7651c3ddbe 100644 --- a/theories/Algebra/Groups/FreeProduct.v +++ b/theories/Algebra/Groups/FreeProduct.v @@ -243,7 +243,7 @@ Section AmalgamatedFreeProduct. (e : forall w, P (amal_eta w)) : forall x, P x. Proof. - snrapply amal_type_ind. + snapply amal_type_ind. 1: exact _. 1: exact e. all: intros; apply path_ishprop. @@ -281,8 +281,8 @@ Section AmalgamatedFreeProduct. Local Instance sgop_amal_type : SgOp amal_type. Proof. intros x y; revert x. - snrapply amal_type_rec; only 1: exact _; intros x; revert y. - { snrapply amal_type_rec; only 1: exact _; intros y. + snapply amal_type_rec; only 1: exact _; intros x; revert y. + { snapply amal_type_rec; only 1: exact _; intros y. 1: exact (amal_eta (x ++ y)). { intros z h1 h2. refine (ap amal_eta _ @ _ @ ap amal_eta _^). diff --git a/theories/Algebra/Groups/GroupCoeq.v b/theories/Algebra/Groups/GroupCoeq.v index 5b1def87a6..852a59be6d 100644 --- a/theories/Algebra/Groups/GroupCoeq.v +++ b/theories/Algebra/Groups/GroupCoeq.v @@ -13,7 +13,7 @@ Local Open Scope mc_mult_scope. Definition GroupCoeq {A B : Group} (f g : A $-> B) : Group. Proof. - nrapply (@AmalgamatedFreeProduct (FreeProduct A A) A B). + napply (@AmalgamatedFreeProduct (FreeProduct A A) A B). - exact (FreeProduct_rec (Id _) (Id _)). - exact (FreeProduct_rec f g). Defined. @@ -28,9 +28,9 @@ Proof. intros x; simpl. rewrite <- (right_identity (f x)). rewrite <- (right_identity (g x)). - rhs_V nrapply (amal_glue (freeproduct_inr x)). + rhs_V napply (amal_glue (freeproduct_inr x)). symmetry. - nrapply (amal_glue (freeproduct_inl x)). + napply (amal_glue (freeproduct_inl x)). Defined. Definition groupcoeq_rec {A B C : Group} (f g : A $-> B) @@ -38,7 +38,7 @@ Definition groupcoeq_rec {A B C : Group} (f g : A $-> B) : GroupCoeq f g $-> C. Proof. rapply (AmalgamatedFreeProduct_rec C (h $o f) h). - snrapply freeproduct_ind_homotopy. + snapply freeproduct_ind_homotopy. (** The goals generated are very simple, but we give explicit proofs with wild cat terms to stop Coq from unfolding terms when checking the proof. Note that the category of groups is definitionally associative. *) - refine (cat_assoc _ _ _ $@ _ $@ cat_assoc_opp _ _ _). exact ((_ $@L freeproduct_rec_beta_inl _ _) $@ cat_idr _ @@ -54,7 +54,7 @@ Definition equiv_groupcoeq_rec `{Funext} {A B C : Group} (f g : A $-> B) Proof. nrefine (equiv_amalgamatedfreeproduct_rec C oE _). nrefine (equiv_sigma_symm _ oE _). - nrapply equiv_functor_sigma_id. + napply equiv_functor_sigma_id. intros h. transitivity {b : A $-> C & (b $== h $o f) * (b $== h $o g)}%type. { nrefine (equiv_functor_sigma_id (fun b => equiv_sigma_prod0 _ _) oE _). @@ -64,13 +64,13 @@ Proof. - exact (equiv_functor_sigma_pb (equiv_functor_sigma_id (fun _ => equiv_path_grouphomomorphism))). - exact (@equiv_contr_sigma _ _ (contr_basedpaths' (h $o f))). } - snrapply equiv_functor_sigma_id. + snapply equiv_functor_sigma_id. intros h'; cbn beta. nrefine (equiv_freeproduct_ind_homotopy _ _ oE _). - snrapply equiv_functor_prod'. - - snrapply equiv_functor_forall_id; simpl; intros a. + snapply equiv_functor_prod'. + - snapply equiv_functor_forall_id; simpl; intros a. by rewrite 2 grp_unit_r. - - snrapply equiv_functor_forall_id; simpl; intros a. + - snapply equiv_functor_forall_id; simpl; intros a. by rewrite 2 grp_unit_r. Defined. @@ -80,7 +80,7 @@ Definition groupcoeq_ind_hprop {G H : Group} {f g : G $-> H} (Hop : forall x y, P x -> P y -> P (x * y)) : forall x, P x. Proof. - snrapply amalgamatedfreeproduct_ind_hprop. + snapply amalgamatedfreeproduct_ind_hprop. - exact _. - intros x. rewrite <- (right_identity x). @@ -98,7 +98,7 @@ Definition groupcoeq_ind_homotopy {G H K : Group} {f g : G $-> H} : h $== h'. Proof. rapply (groupcoeq_ind_hprop _ r). - intros x y p q; by nrapply grp_homo_op_agree. + intros x y p q; by napply grp_homo_op_agree. Defined. Definition functor_groupcoeq