From 743985e3d85d201ea5fa48ac0719069cfabc7055 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 8 Dec 2017 15:30:34 +0100 Subject: [PATCH] Work on pointed naturality of smash-C --- Notes/smash.tex | 32 ++-- algebra/quotient_group.hlean | 2 +- homotopy/EM.hlean | 15 +- homotopy/smash.hlean | 61 ++++--- homotopy/smash_adjoint.hlean | 66 +++++--- move_to_lib.hlean | 9 +- pointed.hlean | 305 ++++++++++++++++++++++++++++++++++- spectrum/basic.hlean | 2 +- spectrum/smash.hlean | 13 +- 9 files changed, 422 insertions(+), 83 deletions(-) diff --git a/Notes/smash.tex b/Notes/smash.tex index f66b0ae..d0dc55a 100644 --- a/Notes/smash.tex +++ b/Notes/smash.tex @@ -573,7 +573,7 @@ We define the pointed equivalences: \begin{thm}\label{thm:smash-functor-right} Given pointed types $A$, $B$ and $C$, the functorial action of the smash product induces a map $$({-})\smsh C:(A\pmap B)\pmap(A\smsh C\pmap B\smsh C)$$ -which is natural in $A$, $B$ and dinatural in $C$. +which is natural in $A$, pointed natural in $B$ and dinatural in $C$. \end{thm} The naturality and dinaturality means that the following squares commute for $f : A' \to A$ $g:B\to B'$ and $h:C\to C'$. \begin{center} @@ -614,8 +614,8 @@ fill the following square (after reducing out the applications of function exten \end{tikzcd} \end{center} The naturality in $B$ is almost the same: for the underlying homotopy we need to show -$(g \o k)\smsh C = g\smsh C \o k\smsh C$. For the pointedness we need to fill the following -square, which follows from \autoref{lem:smash-coh}. +$i:(g \o k)\smsh C = g\smsh C \o k\smsh C$. For the pointedness we need to fill the following +square, which follows from the left pentagon in \autoref{lem:smash-coh}. \begin{center} \begin{tikzcd} (g \o 0)\smsh C \arrow[r, equals]\arrow[dd,equals] & @@ -625,6 +625,14 @@ square, which follows from \autoref{lem:smash-coh}. 0 \end{tikzcd} \end{center} +To show that this naturality is pointed, we need to show that if $g=0$ then this homotopy is the same as the concatenation of the following pointed homotopies: +$$q:({-})\smsh C \circ (A \to 0)\sim ({-})\smsh C \circ 0 \sim 0 \sim 0 \circ ({-})\smsh C\sim 0\smsh B \circ ({-})\smsh C.$$ +To show that the underlying homotopies are the same, we need to show that $i(0,f,\idfunc[C],\idfunc[C])$ is equal to the following concatenation of pointed homotopies +$$q(f):(0\circ f)\smsh C\sim 0\smsh C \sim 0 \sim 0 \circ f\smsh C\sim 0\smsh B \circ f\smsh C,$$ +which is the right pentagons in \autoref{lem:smash-coh}. +To show that these pointed homotopies respect the basepoint in the same way, we need to show that (TODO) +``$R\mathrel\square(0\smsh C \circ t)\cdot q_0=L$ where $L$ and $R$ are the left and right pentagons applied to $0$ and $\square$ is whiskering.'' + The dinaturality in $C$ is a bit harder. For the underlying homotopy we need to show $B\smsh h\o k\smsh C=k\smsh C'\o A\smsh h$. This follows by applying interchange twice: $$B\smsh h\o k\smsh C\sim(\idfunc[B]\o k)\smsh(h\o\idfunc[C])\sim(k\o\idfunc[A])\smsh(\idfunc[C']\o h)\sim k\smsh C'\o A\smsh h.$$ @@ -692,10 +700,9 @@ Note: $\eta$ is also dinatural in $B$, but we don't need this. $\epsilon (x):C$ by induction on $x$. If $x\jdeq(f,b)$ we set $\epsilon(f,b)\defeq f(b)$. If $x$ is either $\auxl$ or $\auxr$ then we set $\epsilon (x)\defeq c_0:C$. If $x$ varies over $\gluel_f$ then we need to show that $f(b_0)=c_0$, which is true by $f_0$. If $x$ varies over $\gluer_b$ we - need to show that $0(b)=c_0$ which is true by reflexivity. The map $\epsilon$ defined as such is trivially a pointed map, - which defines the counit. + need to show that $0(b)=c_0$ which is true by reflexivity. Now $\epsilon_0\defeq 1:\epsilon(0_{B,C},b_0)=c_0$ shows that $\epsilon$ is pointed. - Now we need to show that the unit and counit are (di)natural. (TODO). + Now we need to show that the counit is natural in $B$ and pointed natural in $C$. Finally, we need to show the unit-counit laws. For the underlying homotopy of the first one, let $f:A\to B$. We need to show that $p_f:\epsilon\o\eta f\sim f$. We define $p_f(a)=1:\epsilon(f,a)=f(a)$. To show that $p_f$ is a pointed homotopy, we need to show that @@ -745,7 +752,7 @@ $$(A\pmap B\pmap C)\lpmap{({-})\smsh B}(A\smsh B\pmap (B\pmap C)\smsh B)\lpmap{A % \end{align*} \end{proof} \begin{lem}\label{lem:e-natural} - The function $e$ is natural in $A$, $B$ and $C$. + The function $e$ is natural in $A$, $B$ and pointed natural in $C$. \end{lem} \begin{proof} \textbf{Naturality of $e$ in $A$}. Suppose that $f:A'\pmap A$. Then the following diagram commutes. The left square commutes by naturality of $({-})\smsh B$ in the first argument and the right square commutes because composition on the left commutes with composition on the right. @@ -771,6 +778,7 @@ $$(A\pmap B\pmap C)\lpmap{({-})\smsh B}(A\smsh B\pmap (B\pmap C)\smsh B)\lpmap{A (A\smsh B\pmap C') \end{tikzcd} \end{center} +Pointed naturality: TODO. \textbf{Naturality of $e$ in $B$}. Suppose that $f:B'\pmap B$. Here the diagram is a bit more complicated, since $({-})\smsh B$ is dinatural (instead of natural) in $B$. Then we get the @@ -796,15 +804,7 @@ argument, the back square commutes because composition on the left commutes with inductive type to prove that. \end{rmk} -\begin{lem}\label{lem:e-pointed-natural} - The function $e$ is pointed natural in $C$. -\end{lem} - -\begin{proof} - (TODO) -\end{proof} - -\section{Symmetric monoidality} +\section{Symmetric monoid product} We aim to prove that the smash product is a (1-coherent) symmetric monoidal product [REF: Brunerie] for pointed types, i.e., that \[(\type^*,\, \bool,\, \smsh,\, \alpha,\, \lambda,\, \rho,\, \gamma)\] is a symmetric monoidal category, with the type of booleans $\bool$ (pointed in $0_\bool$) as unit, and for suitable instances of $\alpha$, $\lambda$, $\rho$ and $\gamma$ witnessing associativity, left- and right unitality and the braiding for $\smsh$ and satisfying appropriate coherence relations (associativity pentagon; unitors triangle; braiding-unitors triangle; associativity-braiding hexagon; double braiding). diff --git a/algebra/quotient_group.hlean b/algebra/quotient_group.hlean index 575b479..3acc798 100644 --- a/algebra/quotient_group.hlean +++ b/algebra/quotient_group.hlean @@ -723,7 +723,7 @@ namespace group (hψ : Πg, g ∈ S → ψ g ∈ T) (hφ : Πg, g ∈ R → φ g ∈ S) : quotient_ab_group_functor ψ hψ ∘g quotient_ab_group_functor φ hφ ~ quotient_ab_group_functor (ψ ∘g φ) (λg, proof hψ (φ g) qed ∘ hφ g) := - @quotient_group_functor_compose G H K R _ S _ T _ ψ φ hψ hφ + @quotient_group_functor_compose G H K R _ S _ T _ ψ φ hψ hφ definition quotient_ab_group_functor_gid : quotient_ab_group_functor (gid G) (λg, id) ~ gid (quotient_ab_group R) := diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean index 02fe3c8..d723a54 100644 --- a/homotopy/EM.hlean +++ b/homotopy/EM.hlean @@ -655,8 +655,21 @@ namespace EM definition cokernel {G H : AbGroup} (φ : G →g H) : AbGroup := quotient_ab_group (image φ) + /- todo: in algebra/quotient_group, do the first steps without assuming that N is normal, + then this is qg for (image φ) in H -/ + definition image_cosets {G H : Group} (φ : G →g H) : Set* := + sorry + + definition homotopy_group_EMadd1_functor1 {G H : AbGroup} (φ : G →g H) (n : ℕ) : + πg[n+1] (pfiber (EMadd1_functor φ (n+1))) ≃g cokernel φ := + sorry + + definition homotopy_group_EMadd1_functor2 {G H : AbGroup} (φ : G →g H) (n : ℕ) : + πg[n+1] (pfiber (EMadd1_functor φ n)) ≃g Kernel φ := + sorry + definition trunc_fiber_EM1_functor {G H : Group} (φ : G →g H) : - ptrunc 0 (pfiber (EM1_functor φ)) ≃* sorry := + ptrunc 0 (pfiber (EM1_functor φ)) ≃* image_cosets φ := sorry end EM diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean index 7e3334e..bd03efc 100644 --- a/homotopy/smash.hlean +++ b/homotopy/smash.hlean @@ -1,6 +1,6 @@ -- Authors: Floris van Doorn -import homotopy.smash types.pointed2 .pushout homotopy.red_susp +import homotopy.smash types.pointed2 .pushout homotopy.red_susp ..pointed open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc function red_susp unit @@ -536,14 +536,15 @@ namespace smash square (p₁ ⬝ p₁⁻¹) p₂⁻¹ p₂ idp := proof square_of_eq (con.right_inv p₁ ⬝ (con.right_inv p₂)⁻¹) qed - private definition my_cube_fillerl {A B C : Type} {g : B → C} {f : A → B} {a₁ a₂ : A} {b₀ : B} - {p : f ~ λa, b₀} {q : Πa, g (f a) = g b₀} (r : (λa, ap g (p a)) ~ q) : - cube (hrfl ⬝hp (r a₁)⁻¹) hrfl - (my_squarel (q a₁) (q a₂)) (aps g (my_squarel (p a₁) (p a₂))) - (hrfl ⬝hp (!ap_con ⬝ whisker_left _ !ap_inv ⬝ (r a₁) ◾ (r a₂)⁻²)⁻¹) - (hrfl ⬝hp (r a₂)⁻²⁻¹ ⬝hp !ap_inv⁻¹) := + private definition my_cube_fillerl {B C : Type} {g : B → C} {fa₁ fa₂ b₀ : B} + {pa₁ : fa₁ = b₀} {pa₂ : fa₂ = b₀} {qa₁ : g (fa₁) = g b₀} {qa₂ : g (fa₂) = g b₀} + (ra₁ : ap g (pa₁) = qa₁) (ra₂ : ap g (pa₂) = qa₂) : + cube (hrfl ⬝hp (ra₁)⁻¹) hrfl + (my_squarel (qa₁) (qa₂)) (aps g (my_squarel (pa₁) (pa₂))) + (hrfl ⬝hp (!ap_con ⬝ whisker_left _ !ap_inv ⬝ (ra₁) ◾ (ra₂)⁻²)⁻¹) + (hrfl ⬝hp (ra₂)⁻²⁻¹ ⬝hp !ap_inv⁻¹) := begin - induction r using homotopy.rec_on_idp, induction p using homotopy.rec_on_idp_left, exact idc + induction ra₂, induction ra₁, induction pa₂, induction pa₁, exact idc end private definition my_cube_fillerr {B C : Type} {g : B → C} {b₀ bl br : B} @@ -615,11 +616,11 @@ namespace smash refine !con.assoc ⬝ _, apply con_eq_of_eq_inv_con, refine whisker_right _ _ ⬝ _, rotate 1, rexact functor_gluer'2_same f' g' (g b₀), refine !inv_con_cancel_right ⬝ _, - exact sorry, -- TODO: FIX, the proof below should work (with some small changes) - -- refine _ ⬝ whisker_left _ _, - -- rotate 2, refine ap (whisker_left _) _, symmetry, exact !idp_con ⬝ !idp_con ⬝ !whisker_right_idp ⬝ !idp_con, - -- symmetry, apply whisker_left_idp - } + refine !whisker_left_idp⁻¹ ⬝ _, + refine !con_idp ⬝ _, + apply whisker_left, + apply ap (whisker_left idp), + exact (!idp_con ⬝ !idp_con ⬝ !whisker_right_idp ⬝ !idp_con)⁻¹ } end /- a version where the left maps are identities -/ @@ -725,7 +726,7 @@ namespace smash /- Using these lemmas we show that smash_functor_left is natural in all arguments -/ - definition smash_functor_left_natural_left (f : A' →* A) : + definition smash_functor_left_natural_left (B C : Type*) (f : A' →* A) : psquare (smash_functor_left A B C) (smash_functor_left A' B C) (ppcompose_right f) (ppcompose_right (f ∧→ pid C)) := begin @@ -739,7 +740,7 @@ namespace smash apply smash_functor_pcompose_pconst1_pid } end - definition smash_functor_left_natural_middle (f : B →* B') : + definition smash_functor_left_natural_middle (A C : Type*) (f : B →* B') : psquare (smash_functor_left A B C) (smash_functor_left A B' C) (ppcompose_left f) (ppcompose_left (f ∧→ pid C)) := begin @@ -753,7 +754,7 @@ namespace smash apply smash_functor_pcompose_pconst2_pid } end - definition smash_functor_left_natural_right (f : C →* C') : + definition smash_functor_left_natural_right (A B : Type*) (f : C →* C') : psquare (smash_functor_left A B C) (ppcompose_right (pid A ∧→ f)) (smash_functor_left A B C') (ppcompose_left (pid B ∧→ f)) := begin @@ -772,6 +773,18 @@ namespace smash refine idp ◾** !refl_trans ⬝ !trans_left_inv } end + definition smash_functor_left_natural_middle_phomotopy (A C : Type*) {f f' : B →* B'} + (p : f ~* f') : smash_functor_left_natural_middle A C f = + ppcompose_left_phomotopy p ⬝ph* smash_functor_left_natural_middle A C f' ⬝hp* + ppcompose_left_phomotopy (p ∧~ phomotopy.rfl) := + begin + induction p using phomotopy_rec_idp, + symmetry, + refine !ppcompose_left_phomotopy_refl ◾ph* idp ◾hp* + (ap ppcompose_left_phomotopy !smash_functor_phomotopy_refl ⬝ + !ppcompose_left_phomotopy_refl) ⬝ _, + exact !rfl_phomotopy_hconcat ⬝ !hconcat_phomotopy_rfl + end /- the following is not really used, but a symmetric version of the natural equivalence smash_functor_left -/ @@ -877,11 +890,11 @@ namespace smash refine !con.assoc ⬝ _, apply con_eq_of_eq_inv_con, refine whisker_right _ _ ⬝ _, rotate 1, rexact functor_gluel'2_same f' g (f a₀), refine !inv_con_cancel_right ⬝ _, - exact sorry, -- TODO: FIX, the proof below should work - -- refine _ ⬝ whisker_left _ _, - -- rotate 2, refine ap (whisker_left _) _, symmetry, exact !idp_con ⬝ !idp_con ⬝ !whisker_right_idp ⬝ !idp_con, - -- symmetry, apply whisker_left_idp - } + refine !whisker_left_idp⁻¹ ⬝ _, + refine !con_idp ⬝ _, + apply whisker_left, + apply ap (whisker_left idp), + exact (!idp_con ⬝ !idp_con ⬝ !whisker_right_idp ⬝ !idp_con)⁻¹ } end /- a version where the left maps are identities -/ @@ -985,7 +998,7 @@ namespace smash smash_functor_pcompose_pconst3 (pid A) (pid A) g /- Using these lemmas we show that smash_functor_right is natural in all arguments -/ - definition smash_functor_right_natural_right (f : C →* C') : + definition smash_functor_right_natural_right (A B : Type*) (f : C →* C') : psquare (smash_functor_right A B C) (smash_functor_right A B C') (ppcompose_left f) (ppcompose_left (pid A ∧→ f)) := begin @@ -999,7 +1012,7 @@ namespace smash apply smash_functor_pcompose_pconst4_pid } end - definition smash_functor_right_natural_middle (f : B' →* B) : + definition smash_functor_right_natural_middle (A C : Type*) (f : B' →* B) : psquare (smash_functor_right A B C) (smash_functor_right A B' C) (ppcompose_right f) (ppcompose_right (pid A ∧→ f)) := begin @@ -1013,7 +1026,7 @@ namespace smash apply smash_functor_pcompose_pconst3_pid } end - definition smash_functor_right_natural_left (f : A →* A') : + definition smash_functor_right_natural_left (B C : Type*) (f : A →* A') : psquare (smash_functor_right A B C) (ppcompose_right (f ∧→ (pid B))) (smash_functor_right A' B C) (ppcompose_left (f ∧→ (pid C))) := begin diff --git a/homotopy/smash_adjoint.hlean b/homotopy/smash_adjoint.hlean index 8bd2d9d..1a47c44 100644 --- a/homotopy/smash_adjoint.hlean +++ b/homotopy/smash_adjoint.hlean @@ -53,8 +53,10 @@ namespace smash end definition smash_pmap_unit_pt_natural [constructor] (B : Type*) (f : A →* A') : - smash_functor_pid_pinr' B f pt ⬝* pwhisker_left (smash_functor f (pid B)) (smash_pmap_unit_pt A B) ⬝* - pcompose_pconst (f ∧→ (pid B)) = pinr_phomotopy (respect_pt f) ⬝* smash_pmap_unit_pt A' B := + smash_functor_pid_pinr' B f pt ⬝* + pwhisker_left (smash_functor f (pid B)) (smash_pmap_unit_pt A B) ⬝* + pcompose_pconst (f ∧→ (pid B)) = + pinr_phomotopy (respect_pt f) ⬝* smash_pmap_unit_pt A' B := begin induction f with f f₀, induction A' with A' a₀', esimp at *, induction f₀, refine _ ⬝ !refl_trans⁻¹, @@ -147,7 +149,7 @@ namespace smash refine _ ⬝ (ap_is_constant respect_pt _)⁻¹, refine !idp_con⁻¹ } end - definition smash_pmap_counit_natural_left (g : B →* B') : + definition smash_pmap_counit_natural_left (C : Type*) (g : B →* B') : psquare (pid (ppmap B' C) ∧→ g) (smash_pmap_counit B C) (ppcompose_right g ∧→ pid B) (smash_pmap_counit B' C) := begin @@ -336,20 +338,20 @@ namespace smash definition smash_pelim_natural_left (B C : Type*) (f : A' →* A) : psquare (smash_pelim A B C) (smash_pelim A' B C) (ppcompose_right f) (ppcompose_right (f ∧→ pid B)) := - smash_functor_left_natural_left f ⬝h* !ppcompose_left_ppcompose_right + smash_functor_left_natural_left (ppmap B C) B f ⬝h* !ppcompose_left_ppcompose_right definition smash_pelim_natural_middle (A C : Type*) (f : B' →* B) : psquare (smash_pelim A B C) (smash_pelim A B' C) (ppcompose_left (ppcompose_right f)) (ppcompose_right (pid A ∧→ f)) := pwhisker_tl _ !ppcompose_left_ppcompose_right ⬝* (!smash_functor_left_natural_right⁻¹* ⬝pv* - smash_functor_left_natural_middle (ppcompose_right f) ⬝h* + smash_functor_left_natural_middle _ _ (ppcompose_right f) ⬝h* ppcompose_left_psquare !smash_pmap_counit_natural_left) - definition smash_pelim_natural_right (f : C →* C') : + definition smash_pelim_natural_right (A B : Type*) (f : C →* C') : psquare (smash_pelim A B C) (smash_pelim A B C') (ppcompose_left (ppcompose_left f)) (ppcompose_left f) := - smash_functor_left_natural_middle (ppcompose_left f) ⬝h* + smash_functor_left_natural_middle _ _ (ppcompose_left f) ⬝h* ppcompose_left_psquare (smash_pmap_counit_natural_right _ f) definition smash_pelim_natural_lm (C : Type*) (f : A' →* A) (g : B' →* B) : @@ -393,28 +395,29 @@ namespace smash (smash_adjoint_pmap A B C')⁻¹ᵉ* (ppcompose_left f ∘* g) := smash_elim_natural_right f g - definition smash_adjoint_pmap_inv_natural_right [constructor] {A B C C' : Type*} (f : C →* C') : - ppcompose_left f ∘* smash_adjoint_pmap_inv A B C ~* - smash_adjoint_pmap_inv A B C' ∘* ppcompose_left (ppcompose_left f) := - smash_pelim_natural_right f + definition smash_adjoint_pmap_inv_natural_right [constructor] (A B : Type*) (f : C →* C') : + psquare (smash_adjoint_pmap_inv A B C) (smash_adjoint_pmap_inv A B C') + (ppcompose_left (ppcompose_left f)) (ppcompose_left f) := + smash_pelim_natural_right A B f - definition smash_adjoint_pmap_natural_right [constructor] {A B C C' : Type*} (f : C →* C') : - ppcompose_left (ppcompose_left f) ∘* smash_adjoint_pmap A B C ~* - smash_adjoint_pmap A B C' ∘* ppcompose_left f := - (smash_adjoint_pmap_inv_natural_right f)⁻¹ʰ* + definition smash_adjoint_pmap_natural_right [constructor] (A B : Type*) (f : C →* C') : + psquare (smash_adjoint_pmap A B C) (smash_adjoint_pmap A B C') + (ppcompose_left f) (ppcompose_left (ppcompose_left f)) := + (smash_adjoint_pmap_inv_natural_right A B f)⁻¹ʰ* definition smash_adjoint_pmap_natural_lm (C : Type*) (f : A →* A') (g : B →* B') : psquare (smash_adjoint_pmap A' B' C) (smash_adjoint_pmap A B C) (ppcompose_right (f ∧→ g)) (ppcompose_left (ppcompose_right g) ∘* ppcompose_right f) := (smash_pelim_natural_lm C f g)⁻¹ʰ* + /- some naturalities we skipped, but are now easier to prove -/ definition smash_elim_inv_natural_middle (f : B' →* B) (g : A ∧ B →* C) : ppcompose_right f ∘* smash_elim_inv g ~* smash_elim_inv (g ∘* pid A ∧→ f) := !pcompose_pid⁻¹* ⬝* !passoc ⬝* phomotopy_of_eq (smash_adjoint_pmap_natural_lm C (pid A) f g) definition smash_pmap_unit_natural_left (f : B →* B') : - ppcompose_left (pid A ∧→ f) ∘* smash_pmap_unit A B ~* - ppcompose_right f ∘* smash_pmap_unit A B' := + psquare (smash_pmap_unit A B) (ppcompose_right f) + (smash_pmap_unit A B') (ppcompose_left (pid A ∧→ f)) := begin refine pwhisker_left _ !smash_pelim_inv_pid⁻¹* ⬝* _ ⬝* pwhisker_left _ !smash_pelim_inv_pid, refine !smash_elim_inv_natural_right ⬝* _ ⬝* !smash_elim_inv_natural_middle⁻¹*, @@ -461,7 +464,17 @@ namespace smash definition smash_assoc_elim_natural_right_pt (f : X →* X') (g : A ∧ (B ∧ C) →* X) : f ∘* smash_assoc_elim_pequiv A B C X g ~* smash_assoc_elim_pequiv A B C X' (f ∘* g) := - phomotopy_of_eq (smash_assoc_elim_natural_right A B C f g) + begin + refine !smash_adjoint_pmap_inv_natural_right_pt ⬝* _, + apply smash_elim_phomotopy, + refine !smash_adjoint_pmap_inv_natural_right_pt ⬝* _, + apply smash_elim_phomotopy, + refine !passoc⁻¹* ⬝* _, + refine pwhisker_right _ !smash_adjoint_pmap_natural_right ⬝* _, + refine !passoc ⬝* _, + apply pwhisker_left, + refine !smash_adjoint_pmap_natural_right_pt + end definition smash_assoc_elim_inv_natural_right_pt (f : X →* X') (g : (A ∧ B) ∧ C →* X) : f ∘* (smash_assoc_elim_pequiv A B C X)⁻¹ᵉ* g ~* @@ -517,9 +530,9 @@ namespace smash definition smash_assoc_elim_right_natural_right (A B C D : Type*) (f : X →* X') : psquare (smash_assoc_elim_right_pequiv A B C D X) (smash_assoc_elim_right_pequiv A B C D X') (ppcompose_left f) (ppcompose_left f) := - smash_adjoint_pmap_natural_right f ⬝h* + smash_adjoint_pmap_natural_right (A ∧ (B ∧ C)) D f ⬝h* smash_assoc_elim_natural_right A B C (ppcompose_left f) ⬝h* - smash_adjoint_pmap_inv_natural_right f + smash_adjoint_pmap_inv_natural_right ((A ∧ B) ∧ C) D f definition smash_assoc_smash_functor (A B C D : Type*) : smash_assoc A B C ∧→ pid D ~* !smash_assoc_elim_right_pequiv (pid _) := @@ -534,7 +547,7 @@ namespace smash definition ppcompose_right_smash_assoc (A B C X : Type*) : ppcompose_right (smash_assoc A B C) ~* smash_assoc_elim_pequiv A B C X := - sorry -- one hole left + sorry definition smash_functor_smash_assoc (A B C D : Type*) : pid A ∧→ smash_assoc B C D ~* !smash_assoc_elim_left_pequiv (pid _) := @@ -543,7 +556,7 @@ namespace smash refine pap (!smash_adjoint_pmap_inv ∘* ppcompose_left _) !smash_pelim_inv_pid ⬝* _, refine pap !smash_adjoint_pmap_inv (pwhisker_right _ !ppcompose_right_smash_assoc⁻¹* ⬝* !smash_pmap_unit_natural_left⁻¹*) ⬝* _, - refine phomotopy_of_eq (smash_adjoint_pmap_inv_natural_right (pid A ∧→ smash_assoc B C D) + refine phomotopy_of_eq (smash_adjoint_pmap_inv_natural_right _ _ (pid A ∧→ smash_assoc B C D) !smash_pmap_unit)⁻¹ ⬝* _, refine pwhisker_left _ _ ⬝* !pcompose_pid, apply smash_pmap_unit_counit @@ -589,10 +602,10 @@ namespace smash definition smash_susp_elim_natural_right (A B : Type*) (f : X →* X') : psquare (smash_susp_elim_pequiv A B X) (smash_susp_elim_pequiv A B X') (ppcompose_left f) (ppcompose_left f) := - smash_adjoint_pmap_natural_right f ⬝h* + smash_adjoint_pmap_natural_right (⅀ A) B f ⬝h* susp_adjoint_loop_natural_right (ppcompose_left f) ⬝h* ppcompose_left_psquare (loop_pmap_commute_natural_right B f) ⬝h* - (smash_adjoint_pmap_natural_right (Ω→ f))⁻¹ʰ* ⬝h* + (smash_adjoint_pmap_natural_right A B (Ω→ f))⁻¹ʰ* ⬝h* (susp_adjoint_loop_natural_right f)⁻¹ʰ* definition smash_susp_elim_natural_left (X : Type*) (f : A' →* A) (g : B' →* B) : @@ -640,6 +653,11 @@ namespace smash ... ≃* ⅀(B ∧ A) : susp_smash B A ... ≃* ⅀(A ∧ B) : susp_pequiv (smash_comm B A) + + definition smash_susp_natural (f : A →* A') (g : B →* B') : + psquare (smash_susp A B) (smash_susp A' B') (f ∧→ ⅀→g) (⅀→ (f ∧→ g)) := + sorry + definition susp_smash_move (A B : Type*) : ⅀ A ∧ B ≃* A ∧ ⅀ B := susp_smash A B ⬝e* (smash_susp A B)⁻¹ᵉ* diff --git a/move_to_lib.hlean b/move_to_lib.hlean index 201fad4..538ae7e 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -932,6 +932,9 @@ namespace is_conn definition is_conn_zero_pointed {A : Type*} (p : Πa a' : A, ∥ a = a' ∥) : is_conn 0 A := is_conn_zero (tr pt) p + definition is_conn_zero_pointed' {A : Type*} (p : Πa : A, ∥ a = pt ∥) : is_conn 0 A := + is_conn_zero_pointed (λa a', tconcat (p a) (tinverse (p a'))) + definition is_conn_fiber (n : ℕ₋₂) {A B : Type} (f : A → B) (b : B) [is_conn n A] [is_conn (n.+1) B] : is_conn n (fiber f b) := is_conn_equiv_closed_rev _ !fiber.sigma_char _ @@ -951,10 +954,8 @@ namespace misc pType.mk (Σ(a : A), merely (pt = a)) ⟨pt, tr idp⟩ lemma is_conn_component [instance] (A : Type*) : is_conn 0 (component A) := - is_contr.mk (tr pt) - begin - intro x, induction x with x, induction x with a p, induction p with p, induction p, reflexivity - end + is_conn_zero_pointed' + begin intro x, induction x with a p, induction p with p, induction p, exact tidp end definition component_incl [constructor] (A : Type*) : component A →* A := pmap.mk pr1 idp diff --git a/pointed.hlean b/pointed.hlean index 7ee1e98..ee9240b 100644 --- a/pointed.hlean +++ b/pointed.hlean @@ -8,6 +8,43 @@ open pointed eq equiv function is_equiv unit is_trunc trunc nat algebra sigma gr namespace pointed + definition phomotopy_mk_eq {A B : Type*} {f g : A →* B} {h k : f ~ g} + {h₀ : h pt ⬝ respect_pt g = respect_pt f} {k₀ : k pt ⬝ respect_pt g = respect_pt f} (p : h ~ k) + (q : whisker_right (respect_pt g) (p pt) ⬝ k₀ = h₀) : phomotopy.mk h h₀ = phomotopy.mk k k₀ := + phomotopy_eq p (idp ◾ to_right_inv !eq_con_inv_equiv_con_eq _ ⬝ + q ⬝ (to_right_inv !eq_con_inv_equiv_con_eq _)⁻¹) + + + section phsquare + /- + Squares of pointed homotopies + -/ + + variables {A : Type*} {P : A → Type} {p₀ : P pt} + {f f' f₀₀ f₂₀ f₄₀ f₀₂ f₂₂ f₄₂ f₀₄ f₂₄ f₄₄ : ppi P p₀} + {p₁₀ : f₀₀ ~* f₂₀} {p₃₀ : f₂₀ ~* f₄₀} + {p₀₁ : f₀₀ ~* f₀₂} {p₂₁ : f₂₀ ~* f₂₂} {p₄₁ : f₄₀ ~* f₄₂} + {p₁₂ : f₀₂ ~* f₂₂} {p₃₂ : f₂₂ ~* f₄₂} + {p₀₃ : f₀₂ ~* f₀₄} {p₂₃ : f₂₂ ~* f₂₄} {p₄₃ : f₄₂ ~* f₄₄} + {p₁₄ : f₀₄ ~* f₂₄} {p₃₄ : f₂₄ ~* f₄₄} + + definition phtranspose (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : phsquare p₀₁ p₂₁ p₁₀ p₁₂ := + p⁻¹ + + definition eq_top_of_phsquare (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : p₁₀ = p₀₁ ⬝* p₁₂ ⬝* p₂₁⁻¹* := + eq_trans_symm_of_trans_eq p + + definition eq_bot_of_phsquare (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : p₁₂ = p₀₁⁻¹* ⬝* p₁₀ ⬝* p₂₁ := + eq_symm_trans_of_trans_eq p⁻¹ ⬝ !trans_assoc⁻¹ + + definition eq_left_of_phsquare (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : p₀₁ = p₁₀ ⬝* p₂₁ ⬝* p₁₂⁻¹* := + eq_top_of_phsquare (phtranspose p) + + definition eq_right_of_phsquare (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : p₂₁ = p₁₀⁻¹* ⬝* p₀₁ ⬝* p₁₂ := + eq_bot_of_phsquare (phtranspose p) + + end phsquare + -- /- the pointed type of (unpointed) dependent maps -/ -- definition pupi [constructor] {A : Type} (P : A → Type*) : Type* := -- pointed.mk' (Πa, P a) @@ -33,12 +70,32 @@ namespace pointed -- apply equiv_eq_closed_right, exact !idp_con⁻¹ } -- end + + /- todo: make type argument explicit in ppcompose_left and ppcompose_left_* -/ + /- todo: delete papply_pcompose -/ + /- todo: pmap_pbool_equiv is a special case of ppmap_pbool_pequiv. -/ + definition ppcompose_left_pid [constructor] (A B : Type*) : ppcompose_left (pid B) ~* pid (ppmap A B) := phomotopy_mk_ppmap (λf, pid_pcompose f) (!trans_refl ⬝ !phomotopy_of_eq_of_phomotopy⁻¹) definition ppcompose_right_pid [constructor] (A B : Type*) : ppcompose_right (pid A) ~* pid (ppmap A B) := phomotopy_mk_ppmap (λf, pcompose_pid f) (!trans_refl ⬝ !phomotopy_of_eq_of_phomotopy⁻¹) + section + variables {A A' : Type*} {P : A → Type} {P' : A' → Type} {p₀ : P pt} {p₀' : P' pt} {k l : ppi P p₀} + definition phomotopy_of_eq_inv (p : k = l) : + phomotopy_of_eq p⁻¹ = (phomotopy_of_eq p)⁻¹* := + begin induction p, exact !refl_symm⁻¹ end + + /- todo: replace regular pap -/ + definition pap' (f : ppi P p₀ → ppi P' p₀') (p : k ~* l) : f k ~* f l := + by induction p using phomotopy_rec_idp; reflexivity + + definition phomotopy_of_eq_ap (f : ppi P p₀ → ppi P' p₀') (p : k = l) : + phomotopy_of_eq (ap f p) = pap' f (phomotopy_of_eq p) := + begin induction p, exact !phomotopy_rec_idp_refl⁻¹ end + end + /- remove some duplicates: loop_ppmap_commute, loop_ppmap_pequiv, loop_ppmap_pequiv', pfunext -/ definition pfunext (X Y : Type*) : ppmap X (Ω Y) ≃* Ω (ppmap X Y) := (loop_ppmap_commute X Y)⁻¹ᵉ* @@ -147,13 +204,69 @@ namespace pointed /- Homotopy between a function and its eta expansion -/ - definition pmap_eta {X Y : Type*} (f : X →* Y) : f ~* pmap.mk f (respect_pt f) := + definition pmap_eta [constructor] {X Y : Type*} (f : X →* Y) : f ~* pmap.mk f (respect_pt f) := begin fapply phomotopy.mk, reflexivity, esimp, exact !idp_con end + definition papply_point [constructor] (A B : Type*) : papply B pt ~* pconst (ppmap A B) B := + phomotopy.mk (λf, respect_pt f) idp + + definition pmap_swap_map [constructor] {A B C : Type*} (f : A →* ppmap B C) : + ppmap B (ppmap A C) := + begin + fapply pmap.mk, + { intro b, exact papply C b ∘* f }, + { apply eq_of_phomotopy, exact pwhisker_right f (papply_point B C) ⬝* !pconst_pcompose } + end + + definition pmap_swap_map_pconst (A B C : Type*) : + pmap_swap_map (pconst A (ppmap B C)) ~* pconst B (ppmap A C) := + begin + fapply phomotopy_mk_ppmap, + { intro b, reflexivity }, + { refine !refl_trans ⬝ !phomotopy_of_eq_of_phomotopy⁻¹ } + end + + definition papply_pmap_swap_map [constructor] {A B C : Type*} (f : A →* ppmap B C) (a : A) : + papply C a ∘* pmap_swap_map f ~* f a := + begin + fapply phomotopy.mk, + { intro b, reflexivity }, + { exact !idp_con ⬝ !ap_eq_of_phomotopy⁻¹ } + end + + definition pmap_swap_map_pmap_swap_map {A B C : Type*} (f : A →* ppmap B C) : + pmap_swap_map (pmap_swap_map f) ~* f := + begin + fapply phomotopy_mk_ppmap, + { exact papply_pmap_swap_map f }, + { refine _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹, + fapply phomotopy_mk_eq, intro b, exact !idp_con, + refine !whisker_right_idp ◾ (!idp_con ◾ idp) ⬝ _ ⬝ !idp_con⁻¹ ◾ idp, + symmetry, exact sorry } + end + + definition pmap_swap [constructor] (A B C : Type*) : ppmap A (ppmap B C) →* ppmap B (ppmap A C) := + begin + fapply pmap.mk, + { exact pmap_swap_map }, + { exact eq_of_phomotopy (pmap_swap_map_pconst A B C) } + end + + definition pmap_swap_pequiv [constructor] (A B C : Type*) : + ppmap A (ppmap B C) ≃* ppmap B (ppmap A C) := + begin + fapply pequiv_of_pmap, + { exact pmap_swap A B C }, + fapply adjointify, + { exact pmap_swap B A C }, + { intro f, apply eq_of_phomotopy, exact pmap_swap_map_pmap_swap_map f }, + { intro f, apply eq_of_phomotopy, exact pmap_swap_map_pmap_swap_map f } + end + -- this should replace pnatural_square definition pnatural_square2 {A B : Type} (X : B → Type*) (Y : B → Type*) {f g : A → B} (h : Πa, X (f a) →* Y (g a)) {a a' : A} (p : a = a') : @@ -176,10 +289,39 @@ namespace pointed section psquare variables {A A' A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type*} {f₁₀ f₁₀' : A₀₀ →* A₂₀} {f₃₀ : A₂₀ →* A₄₀} - {f₀₁ f₀₁' : A₀₀ →* A₀₂} {f₂₁ f₂₁' : A₂₀ →* A₂₂} {f₄₁ : A₄₀ →* A₄₂} + {f₀₁ f₀₁' : A₀₀ →* A₀₂} {f₂₁ f₂₁' : A₂₀ →* A₂₂} {f₄₁ f₄₁' : A₄₀ →* A₄₂} {f₁₂ f₁₂' : A₀₂ →* A₂₂} {f₃₂ : A₂₂ →* A₄₂} {f₀₃ : A₀₂ →* A₀₄} {f₂₃ : A₂₂ →* A₂₄} {f₄₃ : A₄₂ →* A₄₄} - {f₁₄ : A₀₄ →* A₂₄} {f₃₄ : A₂₄ →* A₄₄} + {f₁₄ f₁₄' : A₀₄ →* A₂₄} {f₃₄ : A₂₄ →* A₄₄} + + definition phconst_square (f₀₁ : A₀₀ →* A₀₂) (f₂₁ : A₂₀ →* A₂₂) : + psquare (pconst A₀₀ A₂₀) (pconst A₀₂ A₂₂) f₀₁ f₂₁ := + !pcompose_pconst ⬝* !pconst_pcompose⁻¹* + + definition pvconst_square (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) : + psquare f₁₀ f₁₂ (pconst A₀₀ A₀₂) (pconst A₂₀ A₂₂) := + !pconst_pcompose ⬝* !pcompose_pconst⁻¹* + + definition pvconst_square_pcompose (f₃₀ : A₂₀ →* A₄₀) (f₁₀ : A₀₀ →* A₂₀) + (f₃₂ : A₂₂ →* A₄₂) (f₁₂ : A₀₂ →* A₂₂) : + pvconst_square (f₃₀ ∘* f₁₀) (f₃₂ ∘* f₁₂) = pvconst_square f₁₀ f₁₂ ⬝h* pvconst_square f₃₀ f₃₂ := + begin + refine eq_right_of_phsquare !passoc_pconst_left ◾** !passoc_pconst_right⁻¹⁻²** ⬝ idp ◾** + (!trans_symm ⬝ !trans_symm ◾** idp) ⬝ !trans_assoc⁻¹ ⬝ _ ◾** idp, + refine !trans_assoc⁻¹ ⬝ _ ◾** !pwhisker_left_symm⁻¹ ⬝ !trans_assoc ⬝ + idp ◾** !pwhisker_left_trans⁻¹, + apply trans_symm_eq_of_eq_trans, + refine _ ⬝ idp ◾** !passoc_pconst_middle⁻¹ ⬝ !trans_assoc⁻¹ ⬝ !trans_assoc⁻¹, + refine _ ◾** idp ⬝ !trans_assoc, + refine idp ◾** _ ⬝ !trans_assoc⁻¹, + refine ap (pwhisker_right f₁₀) _ ⬝ !pwhisker_right_trans, + refine !trans_refl⁻¹ ⬝ idp ◾** !trans_left_inv⁻¹ ⬝ !trans_assoc⁻¹, + end + + definition phconst_square_pcompose (f₀₃ : A₀₂ →* A₀₄) (f₁₀ : A₀₀ →* A₂₀) + (f₂₃ : A₂₂ →* A₂₄) (f₂₁ : A₂₀ →* A₂₂) : + phconst_square (f₀₃ ∘* f₀₁) (f₂₃ ∘* f₁₂) = phconst_square f₀₁ f₁₂ ⬝v* phconst_square f₀₃ f₂₃ := + sorry definition ptranspose (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : psquare f₀₁ f₂₁ f₁₀ f₁₂ := p⁻¹* @@ -187,9 +329,94 @@ namespace pointed definition hsquare_of_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : hsquare f₁₀ f₁₂ f₀₁ f₂₁ := p - definition homotopy_group_functor_hsquare (n : ℕ) (h : psquare f₁₀ f₁₂ f₀₁ f₂₁) : - psquare (π→[n] f₁₀) (π→[n] f₁₂) - (π→[n] f₀₁) (π→[n] f₂₁) := + definition rfl_phomotopy_hconcat (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : phomotopy.rfl ⬝ph* p = p := + idp ◾** (ap (pwhisker_left f₁₂) !refl_symm ⬝ !pwhisker_left_refl) ⬝ !trans_refl + + definition hconcat_phomotopy_rfl (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : p ⬝hp* phomotopy.rfl = p := + !pwhisker_right_refl ◾** idp ⬝ !refl_trans + + definition rfl_phomotopy_vconcat (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : phomotopy.rfl ⬝pv* p = p := + !pwhisker_left_refl ◾** idp ⬝ !refl_trans + + definition vconcat_phomotopy_rfl (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : p ⬝vp* phomotopy.rfl = p := + idp ◾** (ap (pwhisker_right f₀₁) !refl_symm ⬝ !pwhisker_right_refl) ⬝ !trans_refl + + definition phomotopy_hconcat_phconcat (p : f₀₁' ~* f₀₁) (q : psquare f₁₀ f₁₂ f₀₁ f₂₁) + (r : psquare f₃₀ f₃₂ f₂₁ f₄₁) : (p ⬝ph* q) ⬝h* r = p ⬝ph* (q ⬝h* r) := + begin + induction p using phomotopy_rec_idp, + exact !refl_phomotopy_hconcat ◾h* idp ⬝ !refl_phomotopy_hconcat⁻¹ + end + + definition phconcat_hconcat_phomotopy (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) + (q : psquare f₃₀ f₃₂ f₂₁ f₄₁) (r : f₄₁' ~* f₄₁) : (p ⬝h* q) ⬝hp* r = p ⬝h* (q ⬝hp* r) := + begin + induction r using phomotopy_rec_idp, + exact !hconcat_phomotopy_rfl ⬝ idp ◾h* !hconcat_phomotopy_rfl⁻¹ + end + + definition phomotopy_hconcat_phomotopy (p : f₀₁' ~* f₀₁) (q : psquare f₁₀ f₁₂ f₀₁ f₂₁) + (r : f₂₁' ~* f₂₁) : (p ⬝ph* q) ⬝hp* r = p ⬝ph* (q ⬝hp* r) := + begin + induction r using phomotopy_rec_idp, + exact !hconcat_phomotopy_rfl ⬝ idp ◾ph* !hconcat_phomotopy_rfl⁻¹ + end + + definition hconcat_phomotopy_phconcat (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) + (q : f₂₁' ~* f₂₁) (r : psquare f₃₀ f₃₂ f₂₁' f₄₁) : (p ⬝hp* q) ⬝h* r = p ⬝h* (q⁻¹* ⬝ph* r) := + begin + induction q using phomotopy_rec_idp, + exact !hconcat_phomotopy_rfl ◾h* idp ⬝ idp ◾h* (!refl_symm ◾ph* idp ⬝ !refl_phomotopy_hconcat)⁻¹ + end + + definition phconcat_phomotopy_hconcat (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) + (q : f₂₁ ~* f₂₁') (r : psquare f₃₀ f₃₂ f₂₁' f₄₁) : p ⬝h* (q ⬝ph* r) = (p ⬝hp* q⁻¹*) ⬝h* r := + begin + induction q using phomotopy_rec_idp, + exact idp ◾h* !refl_phomotopy_hconcat ⬝ (idp ◾hp* !refl_symm ⬝ !hconcat_phomotopy_rfl)⁻¹ ◾h* idp + end + + definition hconcat_phomotopy_hconcat_cancel (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) + (q : f₂₁' ~* f₂₁) (r : psquare f₃₀ f₃₂ f₂₁ f₄₁) : (p ⬝hp* q) ⬝h* (q ⬝ph* r) = p ⬝h* r := + begin + induction q using phomotopy_rec_idp, + exact !hconcat_phomotopy_rfl ◾h* !refl_phomotopy_hconcat + end + + definition phomotopy_hconcat_phinverse {f₁₀ : A₀₀ ≃* A₂₀} {f₁₂ : A₀₂ ≃* A₂₂} + (p : f₀₁' ~* f₀₁) (q : psquare f₁₀ f₁₂ f₀₁ f₂₁) : (p ⬝ph* q)⁻¹ʰ* = q⁻¹ʰ* ⬝hp* p := + begin + induction p using phomotopy_rec_idp, + exact !refl_phomotopy_hconcat⁻²ʰ* ⬝ !hconcat_phomotopy_rfl⁻¹ + end + + definition hconcat_phomotopy_phinverse {f₁₀ : A₀₀ ≃* A₂₀} {f₁₂ : A₀₂ ≃* A₂₂} + (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : f₂₁' ~* f₂₁) : (p ⬝hp* q)⁻¹ʰ* = q ⬝ph* p⁻¹ʰ* := + begin + induction q using phomotopy_rec_idp, + exact !hconcat_phomotopy_rfl⁻²ʰ* ⬝ !refl_phomotopy_hconcat⁻¹ + end + + definition pvconst_square_phinverse (f₁₀ : A₀₀ ≃* A₂₀) (f₁₂ : A₀₂ ≃* A₂₂) : + (pvconst_square f₁₀ f₁₂)⁻¹ʰ* = pvconst_square f₁₀⁻¹ᵉ* f₁₂⁻¹ᵉ* := + begin + exact sorry + end + + definition ppcompose_left_phomotopy_hconcat (A : Type*) (p : f₀₁' ~* f₀₁) + (q : psquare f₁₀ f₁₂ f₀₁ f₂₁) : ppcompose_left_psquare (p ⬝ph* q) = + @ppcompose_left_phomotopy A _ _ _ _ p ⬝ph* ppcompose_left_psquare q := + sorry --used + + definition ppcompose_left_hconcat_phomotopy (A : Type*) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) + (q : f₂₁' ~* f₂₁) : ppcompose_left_psquare (p ⬝hp* q) = + ppcompose_left_psquare p ⬝hp* @ppcompose_left_phomotopy A _ _ _ _ q := + sorry + + definition ppcompose_left_pvconst_square (A : Type*) (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) : + ppcompose_left_psquare (pvconst_square f₁₀ f₁₂) = + !ppcompose_left_pconst ⬝ph* pvconst_square (ppcompose_left f₁₀) (@ppcompose_left A _ _ f₁₂) ⬝hp* + !ppcompose_left_pconst := sorry end psquare @@ -282,6 +509,72 @@ namespace pointed A →* pointed.MK B (f pt) := pmap.mk f idp + definition papply_natural_right [constructor] {A B B' : Type*} (f : B →* B') (a : A) : + psquare (papply B a) (papply B' a) (ppcompose_left f) f := + begin + fapply phomotopy.mk, + { intro g, reflexivity }, + { refine !idp_con ⬝ !ap_eq_of_phomotopy ⬝ !idp_con⁻¹ } + end + + -- definition foo {A B : Type} {f : A → B} {a₀ a₁ a₂ : A} {b₀ b₁ b₂ : B} + -- {p₀ : a₀ = a₀} {p₁ : a₀ = a₀} (q₀ : ap f p₀ = idp) (q₁ : ap f p₁ = idp) : + -- whisker_right (ap f p₁) (idp_con (ap f p₀⁻¹) ⬝ !ap_inv ⬝ q₀⁻²)⁻¹ ⬝ !con.assoc ⬝ + -- whisker_left idp (con_eq_of_eq_con_inv (eq_con_inv_of_con_eq _)) ⬝ _ + -- = !idp_con ⬝ q₁ := + -- _ + +/- +whisker_right + (ap (λ f, pppi.to_fun f a) + (eq_of_phomotopy (pcompose_pconst (pconst B B')))) + (idp_con + (ap (λ y, pppi.to_fun y a) + (eq_of_phomotopy + (pconst_pcompose (ppi_const (λ a, B))))⁻¹) ⬝ ap_inv + (λ y, pppi.to_fun y a) + (eq_of_phomotopy + (pconst_pcompose (ppi_const (λ a, B)))) ⬝ inverse2 + (ap_eq_of_phomotopy (pconst_pcompose (ppi_const (λ a, B))) + a))⁻¹ ⬝ (con.assoc + (ppi.to_fun (pvconst_square (papply B a) (papply B' a)) + (ppi_const (λ a, B))) + (ap (λ f, pppi.to_fun f a) + (eq_of_phomotopy (pconst_pcompose (ppi_const (λ a, B))))⁻¹) + (ap (λ f, pppi.to_fun f a) + (eq_of_phomotopy + (pcompose_pconst (pconst B B')))) ⬝ whisker_left + (ppi.to_fun (pvconst_square (papply B a) (papply B' a)) + (ppi_const (λ a, B))) + (con_eq_of_eq_con_inv + (eq_con_inv_of_con_eq + (pwhisker_left_1 B' (ppmap A B) (ppmap A B') (papply B' a) + (pconst (ppmap A B) (ppmap A B')) + (ppcompose_left (pconst B B')) + (ppcompose_left_pconst A B B')⁻¹*))) ⬝ respect_pt + (pvconst_square (papply B a) (papply B' a))) = idp_con + (ap (λ f, pppi.to_fun f a) + (eq_of_phomotopy + (pcompose_pconst (pconst B B')))) ⬝ ap_eq_of_phomotopy + (pcompose_pconst (pconst B B')) + a +-/ + + + + definition papply_natural_right_pconst {A : Type*} (B B' : Type*) (a : A) : + papply_natural_right (pconst B B') a = !ppcompose_left_pconst ⬝ph* !pvconst_square := + begin + fapply phomotopy_mk_eq, + { intro g, symmetry, refine !idp_con ⬝ !ap_inv ⬝ !ap_eq_of_phomotopy⁻² }, + { + + esimp [pvconst_square], + --esimp [inv_con_eq_of_eq_con, pwhisker_left_1] + exact sorry } + end + + /- TODO: computation rule -/ open pi definition fiberwise_pointed_map_rec {A : Type} {B : A → Type*} diff --git a/spectrum/basic.hlean b/spectrum/basic.hlean index 21e73ec..001338a 100644 --- a/spectrum/basic.hlean +++ b/spectrum/basic.hlean @@ -749,7 +749,7 @@ namespace spectrum begin intro k, note sq1 := homotopy_group_homomorphism_psquare (k+2) (ptranspose (smap.glue_square f (-n - 2 +[ℤ] k))), - note sq2 := homotopy_group_functor_hsquare (k+2) (ap1_psquare (ptransport_natural E F f (add.assoc (-n - 2) k 1))), + note sq2 := homotopy_group_functor_psquare (k+2) (ap1_psquare (ptransport_natural E F f (add.assoc (-n - 2) k 1))), note sq3 := (homotopy_group_succ_in_natural (k+2) (f (-n - 2 +[ℤ] (k+1))))⁻¹ʰᵗʸʰ, note sq4 := hsquare_of_psquare sq2, note rect := sq1 ⬝htyh sq4 ⬝htyh sq3, diff --git a/spectrum/smash.hlean b/spectrum/smash.hlean index 1d9ab4a..c986aa5 100644 --- a/spectrum/smash.hlean +++ b/spectrum/smash.hlean @@ -14,7 +14,8 @@ prespectrum.mk (λ z, X ∧ Y z) begin exact !glue end -definition smash_prespectrum_fun {X X' : Type*} {Y Y' : prespectrum} (f : X →* X') (g : Y →ₛ Y') : smash_prespectrum X Y →ₛ smash_prespectrum X' Y' := +definition smash_prespectrum_fun {X X' : Type*} {Y Y' : prespectrum} (f : X →* X') (g : Y →ₛ Y') : + smash_prespectrum X Y →ₛ smash_prespectrum X' Y' := smap.mk (λn, smash_functor f (g n)) begin intro n, refine susp_to_loop_psquare _ _ _ _ _, @@ -22,12 +23,12 @@ smap.mk (λn, smash_functor f (g n)) begin refine vconcat_phomotopy _ (smash_functor_split f (g (S n))), refine phomotopy_vconcat (smash_functor_split f (susp_functor (g n))) _, refine phconcat _ _, - let glue_adjoint := susp_pelim (Y n) (Y (S n)) (glue Y n), - exact pid X' ∧→ glue_adjoint, - exact smash_functor_psquare (pvrefl f) (phrefl glue_adjoint), - refine smash_functor_psquare (phrefl (pid X')) _, + let glue_adjoint := susp_pelim (Y' n) (Y' (S n)) (glue Y' n), + exact pid X ∧→ glue_adjoint, + refine smash_functor_psquare (phrefl (pid X)) _, refine loop_to_susp_square _ _ _ _ _, - exact smap.glue_square g n + exact smap.glue_square g n, + exact smash_functor_psquare (pvrefl f) (phrefl glue_adjoint) end /- smash of a spectrum and a type -/