From 6b727d016f250c23bf925bb7acf99fcca4ecc127 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Tue, 9 Jan 2024 11:42:26 -0500 Subject: [PATCH 1/2] Add pmap_from_psphere_iterated_loops, and needed lemmas --- theories/Pointed/pEquiv.v | 23 +++++++++++++++------ theories/Pointed/pSect.v | 2 +- theories/Pointed/pSusp.v | 42 ++++++++++++++++++++++----------------- theories/Spaces/Circle.v | 22 +++++++++++++++++--- theories/Spaces/Spheres.v | 30 ++++++++++++++++++++++++++++ theories/Types/Bool.v | 3 +++ 6 files changed, 94 insertions(+), 28 deletions(-) diff --git a/theories/Pointed/pEquiv.v b/theories/Pointed/pEquiv.v index 0de7aafd7ce..12f3aca0bcc 100644 --- a/theories/Pointed/pEquiv.v +++ b/theories/Pointed/pEquiv.v @@ -102,13 +102,24 @@ Proof. symmetry; apply peisretr. Defined. -Definition equiv_pequiv_precompose `{Funext} {A B C : pType} (f : A <~>* B) - : (B ->* C) <~> (A ->* C) - := equiv_precompose_cat_equiv f. +Definition pequiv_pequiv_precompose `{Funext} {A B C : pType} (f : A <~>* B) + : (B ->** C) <~>* (A ->** C). +Proof. + srapply Build_pEquiv'. + - exact (equiv_precompose_cat_equiv f). + - (* By using [pelim f], we can avoid [Funext] in this part of the proof. *) + cbn; unfold "o*", point_pforall; cbn. + by pelim f. +Defined. -Definition equiv_pequiv_postcompose `{Funext} {A B C : pType} (f : B <~>* C) - : (A ->* B) <~> (A ->* C) - := equiv_postcompose_cat_equiv f. +Definition pequiv_pequiv_postcompose `{Funext} {A B C : pType} (f : B <~>* C) + : (A ->** B) <~>* (A ->** C). +Proof. + srapply Build_pEquiv'. + - exact (equiv_postcompose_cat_equiv f). + - cbn; unfold "o*", point_pforall; cbn. + by pelim f. +Defined. Proposition equiv_pequiv_inverse `{Funext} {A B : pType} : (A <~>* B) <~> (B <~>* A). diff --git a/theories/Pointed/pSect.v b/theories/Pointed/pSect.v index 4830acc4926..acb529145db 100644 --- a/theories/Pointed/pSect.v +++ b/theories/Pointed/pSect.v @@ -30,7 +30,7 @@ Definition equiv_pequiv_pslice_psect `{Funext} {A B C : pType} : pSect f <~> pSect g. Proof. srapply equiv_functor_sigma'. - 1: exact (equiv_pequiv_postcompose t). + 1: exact (pequiv_pequiv_postcompose t). intro s; cbn. apply equiv_phomotopy_concat_l. refine ((pmap_compose_assoc _ _ _)^* @* _). diff --git a/theories/Pointed/pSusp.v b/theories/Pointed/pSusp.v index 13963f4e250..453ad0f739c 100644 --- a/theories/Pointed/pSusp.v +++ b/theories/Pointed/pSusp.v @@ -3,6 +3,7 @@ Require Import Types. Require Import Pointed.Core. Require Import Pointed.Loops. Require Import Pointed.pTrunc. +Require Import Pointed.pEquiv. Require Import Homotopy.Suspension. Require Import Homotopy.Freudenthal. Require Import Truncations. @@ -241,25 +242,30 @@ Qed. (** Now we can finally construct the adjunction equivalence. *) Definition loop_susp_adjoint `{Funext} (A B : pType) - : (psusp A ->* B) <~> (A ->* loops B). + : (psusp A ->** B) <~>* (A ->** loops B). Proof. - refine (equiv_adjointify - (fun f => fmap loops f o* loop_susp_unit A) - (fun g => loop_susp_counit B o* fmap psusp g) _ _). - - intros g. apply path_pforall. - refine (pmap_prewhisker _ (fmap_comp loops _ _) @* _). - refine (pmap_compose_assoc _ _ _ @* _). - refine (pmap_postwhisker _ (loop_susp_unit_natural g)^* @* _). - refine ((pmap_compose_assoc _ _ _)^* @* _). - refine (pmap_prewhisker g (loop_susp_triangle1 B) @* _). - apply pmap_postcompose_idmap. - - intros f. apply path_pforall. - refine (pmap_postwhisker _ (fmap_comp psusp _ _) @* _). - refine ((pmap_compose_assoc _ _ _)^* @* _). - refine (pmap_prewhisker _ (loop_susp_counit_natural f)^* @* _). - refine (pmap_compose_assoc _ _ _ @* _). - refine (pmap_postwhisker f (loop_susp_triangle2 A) @* _). - apply pmap_precompose_idmap. + snrapply Build_pEquiv'. + - refine (equiv_adjointify + (fun f => fmap loops f o* loop_susp_unit A) + (fun g => loop_susp_counit B o* fmap psusp g) _ _). + + intros g. apply path_pforall. + refine (pmap_prewhisker _ (fmap_comp loops _ _) @* _). + refine (pmap_compose_assoc _ _ _ @* _). + refine (pmap_postwhisker _ (loop_susp_unit_natural g)^* @* _). + refine ((pmap_compose_assoc _ _ _)^* @* _). + refine (pmap_prewhisker g (loop_susp_triangle1 B) @* _). + apply pmap_postcompose_idmap. + + intros f. apply path_pforall. + refine (pmap_postwhisker _ (fmap_comp psusp _ _) @* _). + refine ((pmap_compose_assoc _ _ _)^* @* _). + refine (pmap_prewhisker _ (loop_susp_counit_natural f)^* @* _). + refine (pmap_compose_assoc _ _ _ @* _). + refine (pmap_postwhisker f (loop_susp_triangle2 A) @* _). + apply pmap_precompose_idmap. + - apply path_pforall. + unfold equiv_adjointify, equiv_fun. + nrapply (pmap_prewhisker _ fmap_loops_pconst @* _). + rapply cat_zero_l. Defined. (** And its naturality is easy. *) diff --git a/theories/Spaces/Circle.v b/theories/Spaces/Circle.v index 7d7f69d33bb..7b4db18e2e3 100644 --- a/theories/Spaces/Circle.v +++ b/theories/Spaces/Circle.v @@ -1,5 +1,6 @@ (* -*- mode: coq; mode: visual-line -*- *) Require Import Basics Types. +Require Import Pointed.Core Pointed.Loops Pointed.pEquiv. Require Import HSet. Require Import Spaces.Pos Spaces.Int. Require Import Colimits.Coeq. @@ -8,6 +9,7 @@ Require Import Cubical.DPath. (** * Theorems about the [Circle]. *) +Local Open Scope pointed_scope. Local Open Scope path_scope. Generalizable Variables X A B f g n. @@ -77,6 +79,8 @@ Defined. (** The [Circle] is pointed by [base]. *) Global Instance ispointed_Circle : IsPointed Circle := base. +Definition pCircle : pType := [Circle, base]. + (** ** The loop space of the [Circle] is the Integers [Int] This is the encode-decode style proof a la Licata-Shulman. *) @@ -257,9 +261,9 @@ Proof. srapply Circle_ind. + reflexivity. + unfold Circle_rec_uncurried; cbn. - rewrite transport_paths_FlFr. - rewrite Circle_rec_beta_loop. - rewrite concat_p1; apply concat_Vp. + apply transport_paths_FlFr'. + apply equiv_p1_1q. + apply Circle_rec_beta_loop. - intros [b p]; apply ap. apply Circle_rec_beta_loop. Defined. @@ -267,3 +271,15 @@ Defined. Definition equiv_Circle_rec `{Funext} (P : Type) : {b : P & b = b} <~> (Circle -> P) := Build_Equiv _ _ _ (isequiv_Circle_rec_uncurried P). + +(** A pointed version of the universal property of the circle. *) +Definition pmap_from_circle_loops `{Funext} (X : pType) + : (pCircle ->** X) <~>* loops X. +Proof. + snrapply Build_pEquiv'. + - refine (_ oE (issig_pmap _ _)^-1%equiv). + equiv_via { xp : { x : X & x = x } & xp.1 = pt }. + 2: make_equiv_contr_basedpaths. + exact ((equiv_functor_sigma_pb (equiv_Circle_rec X)^-1%equiv)). + - simpl. apply ap_const. +Defined. diff --git a/theories/Spaces/Spheres.v b/theories/Spaces/Spheres.v index d4b5ba22562..dd0c653cc44 100644 --- a/theories/Spaces/Spheres.v +++ b/theories/Spaces/Spheres.v @@ -1,5 +1,6 @@ (* -*- mode: coq; mode: visual-line -*- *) Require Import Basics Types. +Require Import WildCat.Equiv. Require Import NullHomotopy. Require Import Homotopy.Suspension. Require Import Pointed. @@ -53,6 +54,24 @@ Defined. Definition equiv_S0_Bool : Sphere 0 <~> Bool := Build_Equiv _ _ _ isequiv_S0_to_Bool. +Definition ispointed_bool : IsPointed Bool := true. + +Definition pBool := [Bool, true]. + +Definition pequiv_S0_Bool : psphere 0 <~>* pBool + := @Build_pEquiv' (psphere 0) pBool equiv_S0_Bool 1. + +(** In [pmap_from_psphere_iterated_loops] below, we'll use this universal property of [pBool]. *) +Definition pmap_from_bool `{Funext} (X : pType) + : (pBool ->** X) <~>* X. +Proof. + snrapply Build_pEquiv'. + - refine (_ oE (issig_pmap _ _)^-1%equiv). + refine (_ oE (equiv_functor_sigma_pb (equiv_bool_rec_uncurried X))^-1%equiv); cbn. + make_equiv_contr_basedpaths. + - reflexivity. +Defined. + (** *** [Sphere 1] *) Definition S1_to_Circle : (Sphere 1) -> Circle. Proof. @@ -287,3 +306,14 @@ Proof. apply (istrunc_allnullhomot n'). intro f. apply nullhomot_paths_from_susp, HX. Defined. + +(** Iterated loop spaces can be described using pointed maps from spheres. The [n = 0] case of this is stated using Bool in [pmap_from_bool] above, and the [n = 1] case of this is stated using [Circle] in [pmap_from_circle_loops] in Circle.v. *) +Definition pmap_from_psphere_iterated_loops `{Funext} (n : nat) (X : pType) + : (psphere n ->** X) <~>* iterated_loops n X. +Proof. + induction n as [|n IHn]; simpl. + - exact (pmap_from_bool X o*E pequiv_pequiv_precompose pequiv_S0_Bool^-1* ). + - refine (emap loops IHn o*E _). + refine (_ o*E loop_susp_adjoint (psphere n) _). + symmetry; apply equiv_loops_ppforall. +Defined. diff --git a/theories/Types/Bool.v b/theories/Types/Bool.v index ec4e620fd95..830a5b0987e 100644 --- a/theories/Types/Bool.v +++ b/theories/Types/Bool.v @@ -117,6 +117,9 @@ Section BoolForall. Defined. End BoolForall. +Definition equiv_bool_rec_uncurried `{Funext} (P : Type) : P * P <~> (Bool -> P) + := (equiv_bool_forall_prod (fun _ => P))^-1%equiv. + (** ** The type [Bool <~> Bool] is equivalent to [Bool]. *) (** The nonidentity equivalence is negation (the flip). *) From 44c5dff9ebaeb38820cd5ffbfd2ca993fdd48fb4 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Tue, 9 Jan 2024 12:37:03 -0500 Subject: [PATCH 2/2] Adjust to renaming of (p)equiv_pequiv_postcompose --- theories/Homotopy/HSpace/Moduli.v | 4 ++-- theories/Spaces/BAut.v | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/theories/Homotopy/HSpace/Moduli.v b/theories/Homotopy/HSpace/Moduli.v index fb0db5fc6d2..a3044277201 100644 --- a/theories/Homotopy/HSpace/Moduli.v +++ b/theories/Homotopy/HSpace/Moduli.v @@ -80,7 +80,7 @@ Lemma equiv_pmap_hspace `{Funext} {A : pType} (a : A) `{IsHSpace A} `{!IsEquiv (hspace_op a)} : (A ->* A) <~> (A ->* [A,a]). Proof. - apply equiv_pequiv_postcompose. + nrapply pequiv_pequiv_postcompose. rapply pequiv_hspace_left_op. Defined. @@ -131,7 +131,7 @@ Proof. refine (_ oE equiv_iscohhspace_psect A). refine (_ oE (equiv_pequiv_pslice_psect _ _ _ hspace_ev_trivialization^*)^-1%equiv). refine (_ oE equiv_psect_psnd (A:=[A ->* A, pmap_idmap])). - refine (equiv_pequiv_postcompose _); symmetry. + refine (pequiv_pequiv_postcompose _); symmetry. rapply pequiv_hspace_left_op. Defined. diff --git a/theories/Spaces/BAut.v b/theories/Spaces/BAut.v index 2c97dbf727e..8e763b29b4f 100644 --- a/theories/Spaces/BAut.v +++ b/theories/Spaces/BAut.v @@ -276,14 +276,14 @@ Section ClassifyingMaps. : (Y ->* pBAut@{u v} F) <~> { p : { q : pSlice Y & forall y:Y, merely (hfiber q.2 y <~> F) } & pfiber p.1.2 <~>* F } := (equiv_sigma_pfibration_O (subuniverse_merely_equiv F)) - oE equiv_pequiv_postcompose pequiv_pbaut_typeOp. + oE pequiv_pequiv_postcompose pequiv_pbaut_typeOp. (** When [Y] is connected, pointed maps into [pBAut F] correspond to maps into the universe sending the base point to [F]. *) Proposition equiv_pmap_pbaut_type_p `{Univalence} {Y : pType@{u}} {F : Type@{u}} `{IsConnected 0 Y} : (Y ->* pBAut F) <~> (Y ->* [Type@{u}, F]). Proof. - refine (_ oE equiv_pequiv_postcompose pequiv_pbaut_typeOp). + refine (_ oE pequiv_pequiv_postcompose pequiv_pbaut_typeOp). rapply equiv_pmap_typeO_type_connected. Defined.