From 5ad44432376ea647a9afb25339f6a2086af5a8b9 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 14 Jun 2017 21:56:23 -0400 Subject: [PATCH] feat(pointed): rename pequiv.MK2 to pequiv.MK, it is the more natural constructor also move some definitions from pointed or equiv to pointed2 and define transitivity so that it computes --- hott/algebra/group_theory.hlean | 10 -- hott/homotopy/susp.hlean | 2 +- hott/types/equiv.hlean | 48 ------- hott/types/pointed.hlean | 221 ++++++++++---------------------- hott/types/pointed2.hlean | 135 ++++++++++++++++++- 5 files changed, 200 insertions(+), 216 deletions(-) diff --git a/hott/algebra/group_theory.hlean b/hott/algebra/group_theory.hlean index 339c64796..8d1d01c49 100644 --- a/hott/algebra/group_theory.hlean +++ b/hott/algebra/group_theory.hlean @@ -179,16 +179,6 @@ namespace group isomorphism_of_equiv (equiv_of_eq (ap Group.carrier φ)) begin intros, induction φ, reflexivity end - definition pequiv_of_isomorphism_of_eq {G₁ G₂ : Group} (p : G₁ = G₂) : - pequiv_of_isomorphism (isomorphism_of_eq p) = pequiv_of_eq (ap pType_of_Group p) := - begin - induction p, - apply pequiv_eq, - fapply phomotopy.mk, - { intro g, reflexivity }, - { apply is_prop.elim } - end - definition to_ginv [constructor] (φ : G₁ ≃g G₂) : G₂ →g G₁ := homomorphism.mk φ⁻¹ abstract begin diff --git a/hott/homotopy/susp.hlean b/hott/homotopy/susp.hlean index e998bb161..a059366a7 100644 --- a/hott/homotopy/susp.hlean +++ b/hott/homotopy/susp.hlean @@ -6,7 +6,7 @@ Authors: Floris van Doorn, Ulrik Buchholtz Declaration of suspension -/ -import hit.pushout types.pointed cubical.square .connectedness +import hit.pushout types.pointed2 cubical.square .connectedness open pushout unit eq equiv diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean index eedd82aac..e36a4181a 100644 --- a/hott/types/equiv.hlean +++ b/hott/types/equiv.hlean @@ -306,51 +306,3 @@ namespace equiv end end equiv - -namespace pointed - open equiv is_equiv pointed prod - definition pequiv.sigma_char {A B : Type*} : - (A ≃* B) ≃ Σ(f : A →* B), (Σ(g : B →* A), f ∘* g ~* pid B) × (Σ(h : B →* A), h ∘* f ~* pid A) := - begin - fapply equiv.MK, - { intro f, exact ⟨f, (⟨pequiv.to_pinv1 f, pequiv.pright_inv f⟩, - ⟨pequiv.to_pinv2 f, pequiv.pleft_inv f⟩)⟩, }, - { intro f, exact pequiv.mk' f.1 (pr1 f.2).1 (pr2 f.2).1 (pr1 f.2).2 (pr2 f.2).2 }, - { intro f, induction f with f v, induction v with hl hr, induction hl, induction hr, - reflexivity }, - { intro f, induction f, reflexivity } - end - - variables {A B : Type*} - definition is_contr_pright_inv (f : A ≃* B) : is_contr (Σ(g : B →* A), f ∘* g ~* pid B) := - begin - fapply is_trunc_equiv_closed, - { exact !fiber.sigma_char ⬝e sigma_equiv_sigma_right (λg, !pmap_eq_equiv) }, - fapply is_contr_fiber_of_is_equiv, - exact pequiv.to_is_equiv (pequiv_ppcompose_left f) - end - - definition is_contr_pleft_inv (f : A ≃* B) : is_contr (Σ(h : B →* A), h ∘* f ~* pid A) := - begin - fapply is_trunc_equiv_closed, - { exact !fiber.sigma_char ⬝e sigma_equiv_sigma_right (λg, !pmap_eq_equiv) }, - fapply is_contr_fiber_of_is_equiv, - exact pequiv.to_is_equiv (pequiv_ppcompose_right f) - end - - definition pequiv_eq_equiv (f g : A ≃* B) : (f = g) ≃ f ~* g := - have Π(f : A →* B), is_prop ((Σ(g : B →* A), f ∘* g ~* pid B) × (Σ(h : B →* A), h ∘* f ~* pid A)), - begin - intro f, apply is_prop_of_imp_is_contr, intro v, - let f' := pequiv.sigma_char⁻¹ᵉ ⟨f, v⟩, - apply is_trunc_prod, exact is_contr_pright_inv f', exact is_contr_pleft_inv f' - end, - calc (f = g) ≃ (pequiv.sigma_char f = pequiv.sigma_char g) - : eq_equiv_fn_eq pequiv.sigma_char f g - ... ≃ (f = g :> (A →* B)) : subtype_eq_equiv - ... ≃ (f ~* g) : pmap_eq_equiv f g - - definition pequiv_eq {f g : A ≃* B} (H : f ~* g) : f = g := - (pequiv_eq_equiv f g)⁻¹ᵉ H - -end pointed diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean index fd26f7ab9..08bee90bc 100644 --- a/hott/types/pointed.hlean +++ b/hott/types/pointed.hlean @@ -726,7 +726,7 @@ namespace pointed is_equiv (pequiv._trans_of_to_pmap f) := pequiv.to_is_equiv f - protected definition pequiv.MK2 [constructor] (f : A →* B) (g : B →* A) + protected definition pequiv.MK [constructor] (f : A →* B) (g : B →* A) (gf : g ∘* f ~* !pid) (fg : f ∘* g ~* !pid) : A ≃* B := pequiv.mk' f g g fg gf @@ -752,11 +752,11 @@ namespace pointed definition pequiv_of_equiv [constructor] (f : A ≃ B) (H : f pt = pt) : A ≃* B := pequiv.mk f _ H - protected definition pequiv.MK [constructor] (f : A →* B) (g : B → A) + protected definition pequiv.MK' [constructor] (f : A →* B) (g : B → A) (gf : Πa, g (f a) = a) (fg : Πb, f (g b) = b) : A ≃* B := pequiv.mk f (adjointify f g fg gf) (respect_pt f) - /- categorical properties of pointed equivalences -/ + /- reflexivity and symmetry (transitivity is below) -/ protected definition pequiv.refl [refl] [constructor] (A : Type*) : A ≃* A := pequiv.mk' (pid A) (pid A) (pid A) !pid_pcompose !pcompose_pid @@ -765,36 +765,26 @@ namespace pointed pequiv.refl A protected definition pequiv.symm [symm] [constructor] (f : A ≃* B) : B ≃* A := - pequiv.mk' (pequiv.to_pinv1 f) f f (pleft_inv' f) (pequiv.pright_inv f) - - protected definition pequiv.trans [trans] [constructor] (f : A ≃* B) (g : B ≃* C) : A ≃* C := - pequiv_of_pmap (g ∘* f) !is_equiv_compose - - definition pequiv_compose {A B C : Type*} (g : B ≃* C) (f : A ≃* B) : A ≃* C := - pequiv_of_pmap (g ∘* f) (is_equiv_compose g f) + pequiv.MK (to_pinv f) f (pequiv.pright_inv f) (pleft_inv' f) postfix `⁻¹ᵉ*`:(max + 1) := pequiv.symm - infix ` ⬝e* `:75 := pequiv.trans - infixr ` ∘*ᵉ `:60 := pequiv_compose + + definition pleft_inv (f : A ≃* B) : f⁻¹ᵉ* ∘* f ~* pid A := + pleft_inv' f + + definition pright_inv (f : A ≃* B) : f ∘* f⁻¹ᵉ* ~* pid B := + pequiv.pright_inv f definition to_pmap_pequiv_of_pmap {A B : Type*} (f : A →* B) (H : is_equiv f) : pequiv.to_pmap (pequiv_of_pmap f H) = f := by reflexivity - /- - A version of pequiv.MK with stronger conditions. - The advantage of defining a pointed equivalence with this definition is that there is a - pointed homotopy between the inverse of the resulting equivalence and the given pointed map g. - This is not the case when using `pequiv.MK` (if g is a pointed map), - that will only give an ordinary homotopy. - -/ - - definition to_pmap_pequiv_MK2 [constructor] (f : A →* B) (g : B →* A) - (gf : g ∘* f ~* !pid) (fg : f ∘* g ~* !pid) : pequiv.MK2 f g gf fg ~* f := + definition to_pmap_pequiv_MK [constructor] (f : A →* B) (g : B →* A) + (gf : g ∘* f ~* !pid) (fg : f ∘* g ~* !pid) : pequiv.MK f g gf fg ~* f := by reflexivity - definition to_pinv_pequiv_MK2 [constructor] (f : A →* B) (g : B →* A) - (gf : g ∘* f ~* !pid) (fg : f ∘* g ~* !pid) : to_pinv (pequiv.MK2 f g gf fg) ~* g := + definition to_pinv_pequiv_MK [constructor] (f : A →* B) (g : B →* A) + (gf : g ∘* f ~* !pid) (fg : f ∘* g ~* !pid) : to_pinv (pequiv.MK f g gf fg) ~* g := by reflexivity /- more on pointed equivalences -/ @@ -803,19 +793,12 @@ namespace pointed : B a ≃* B a' := pequiv_of_pmap (ptransport B p) !is_equiv_tr - definition to_pmap_pequiv_trans {A B C : Type*} (f : A ≃* B) (g : B ≃* C) - : pequiv.to_pmap (f ⬝e* g) = g ∘* f := - by reflexivity - - definition to_fun_pequiv_trans {X Y Z : Type*} (f : X ≃* Y) (g :Y ≃* Z) : f ⬝e* g ~ g ∘ f := - λx, idp - definition pequiv_change_fun [constructor] (f : A ≃* B) (f' : A →* B) (Heq : f ~ f') : A ≃* B := pequiv_of_pmap f' (is_equiv.homotopy_closed f Heq) definition pequiv_change_inv [constructor] (f : A ≃* B) (f' : B →* A) (Heq : to_pinv f ~ f') : A ≃* B := - pequiv.MK f f' (to_left_inv (equiv_change_inv f Heq)) (to_right_inv (equiv_change_inv f Heq)) + pequiv.MK' f f' (to_left_inv (equiv_change_inv f Heq)) (to_right_inv (equiv_change_inv f Heq)) definition pequiv_rect' (f : A ≃* B) (P : A → B → Type) (g : Πb, P (f⁻¹ b) b) (a : A) : P a (f a) := @@ -827,21 +810,12 @@ namespace pointed definition pequiv_of_eq [constructor] {A B : Type*} (p : A = B) : A ≃* B := pequiv_of_pmap (pcast p) !is_equiv_tr - definition peconcat_eq {A B C : Type*} (p : A ≃* B) (q : B = C) : A ≃* C := - p ⬝e* pequiv_of_eq q - - definition eq_peconcat {A B C : Type*} (p : A = B) (q : B ≃* C) : A ≃* C := - pequiv_of_eq p ⬝e* q - definition eq_of_pequiv {A B : Type*} (p : A ≃* B) : A = B := pType_eq (equiv_of_pequiv p) !respect_pt definition peap {A B : Type*} (F : Type* → Type*) (p : A ≃* B) : F A ≃* F B := pequiv_of_pmap (pcast (ap F (eq_of_pequiv p))) begin cases eq_of_pequiv p, apply is_equiv_id end - infix ` ⬝e*p `:75 := peconcat_eq - infix ` ⬝pe* `:75 := eq_peconcat - -- rename pequiv_of_eq_natural definition pequiv_of_eq_commute [constructor] {A : Type} {B C : A → Type*} (f : Πa, B a →* C a) {a₁ a₂ : A} (p : a₁ = a₂) : pequiv_of_eq (ap C p) ∘* f a₁ ~* f a₂ ∘* pequiv_of_eq (ap B p) := @@ -856,12 +830,6 @@ namespace pointed -/ /- computation rules of pointed homotopies, possibly combined with pointed equivalences -/ - definition pleft_inv (f : A ≃* B) : f⁻¹ᵉ* ∘* f ~* pid A := - pleft_inv' f - - definition pright_inv (f : A ≃* B) : f ∘* f⁻¹ᵉ* ~* pid B := - pequiv.pright_inv f - definition pcancel_left (f : B ≃* C) {g h : A →* B} (p : f ∘* g ~* f ∘* h) : g ~* h := begin refine _⁻¹* ⬝* pwhisker_left f⁻¹ᵉ* p ⬝* _: @@ -952,35 +920,6 @@ namespace pointed (p : pid B ~* f ∘* g) : g⁻¹ᵉ* ~* f := (phomotopy_pinv_of_phomotopy_pid' p⁻¹*)⁻¹* - definition pinv_pinv {A B : Type*} (f : A ≃* B) : (f⁻¹ᵉ*)⁻¹ᵉ* ~* f := - (phomotopy_pinv_of_phomotopy_pid (pleft_inv f))⁻¹* - - definition pinv2 {A B : Type*} {f f' : A ≃* B} (p : f ~* f') : f⁻¹ᵉ* ~* f'⁻¹ᵉ* := - phomotopy_pinv_of_phomotopy_pid (pinv_right_phomotopy_of_phomotopy (!pid_pcompose ⬝* p)⁻¹*) - - postfix [parsing_only] `⁻²*`:(max+10) := pinv2 - - definition trans_pinv {A B C : Type*} (f : A ≃* B) (g : B ≃* C) : - (f ⬝e* g)⁻¹ᵉ* ~* f⁻¹ᵉ* ∘* g⁻¹ᵉ* := - begin - refine (phomotopy_pinv_of_phomotopy_pid _)⁻¹*, - refine !passoc ⬝* _, - refine pwhisker_left _ (!passoc⁻¹* ⬝* pwhisker_right _ !pright_inv ⬝* !pid_pcompose) ⬝* _, - apply pright_inv - end - - definition pinv_trans_pinv_left {A B C : Type*} (f : B ≃* A) (g : B ≃* C) : - (f⁻¹ᵉ* ⬝e* g)⁻¹ᵉ* ~* f ∘* g⁻¹ᵉ* := - !trans_pinv ⬝* pwhisker_right _ !pinv_pinv - - definition pinv_trans_pinv_right {A B C : Type*} (f : A ≃* B) (g : C ≃* B) : - (f ⬝e* g⁻¹ᵉ*)⁻¹ᵉ* ~* f⁻¹ᵉ* ∘* g := - !trans_pinv ⬝* pwhisker_left _ !pinv_pinv - - definition pinv_trans_pinv_pinv {A B C : Type*} (f : B ≃* A) (g : C ≃* B) : - (f⁻¹ᵉ* ⬝e* g⁻¹ᵉ*)⁻¹ᵉ* ~* f ∘* g := - !trans_pinv ⬝* !pinv_pinv ◾* !pinv_pinv - definition pinv_pcompose_cancel_left {A B C : Type*} (g : B ≃* C) (f : A →* B) : g⁻¹ᵉ* ∘* (g ∘* f) ~* f := !passoc⁻¹* ⬝* pwhisker_right f !pleft_inv ⬝* !pid_pcompose @@ -997,11 +936,64 @@ namespace pointed (g ∘* f) ∘* f⁻¹ᵉ* ~* g := !passoc ⬝* pwhisker_left g !pright_inv ⬝* !pcompose_pid + definition pinv_pinv {A B : Type*} (f : A ≃* B) : (f⁻¹ᵉ*)⁻¹ᵉ* ~* f := + (phomotopy_pinv_of_phomotopy_pid (pleft_inv f))⁻¹* + + definition pinv2 {A B : Type*} {f f' : A ≃* B} (p : f ~* f') : f⁻¹ᵉ* ~* f'⁻¹ᵉ* := + phomotopy_pinv_of_phomotopy_pid (pinv_right_phomotopy_of_phomotopy (!pid_pcompose ⬝* p)⁻¹*) + + postfix [parsing_only] `⁻²*`:(max+10) := pinv2 + + protected definition pequiv.trans [trans] [constructor] (f : A ≃* B) (g : B ≃* C) : A ≃* C := + pequiv.MK (g ∘* f) (f⁻¹ᵉ* ∘* g⁻¹ᵉ*) + abstract !passoc ⬝* pwhisker_left _ (pinv_pcompose_cancel_left g f) ⬝* pleft_inv f end + abstract !passoc ⬝* pwhisker_left _ (pcompose_pinv_cancel_left f g⁻¹ᵉ*) ⬝* pright_inv g end + + definition pequiv_compose {A B C : Type*} (g : B ≃* C) (f : A ≃* B) : A ≃* C := + pequiv.trans f g + + infix ` ⬝e* `:75 := pequiv.trans + infixr ` ∘*ᵉ `:60 := pequiv_compose + + definition to_pmap_pequiv_trans {A B C : Type*} (f : A ≃* B) (g : B ≃* C) + : pequiv.to_pmap (f ⬝e* g) = g ∘* f := + by reflexivity + + definition to_fun_pequiv_trans {X Y Z : Type*} (f : X ≃* Y) (g :Y ≃* Z) : f ⬝e* g ~ g ∘ f := + λx, idp + + definition peconcat_eq {A B C : Type*} (p : A ≃* B) (q : B = C) : A ≃* C := + p ⬝e* pequiv_of_eq q + + definition eq_peconcat {A B C : Type*} (p : A = B) (q : B ≃* C) : A ≃* C := + pequiv_of_eq p ⬝e* q + + + infix ` ⬝e*p `:75 := peconcat_eq + infix ` ⬝pe* `:75 := eq_peconcat + + + definition trans_pinv {A B C : Type*} (f : A ≃* B) (g : B ≃* C) : + (f ⬝e* g)⁻¹ᵉ* ~* f⁻¹ᵉ* ∘* g⁻¹ᵉ* := + by reflexivity + + definition pinv_trans_pinv_left {A B C : Type*} (f : B ≃* A) (g : B ≃* C) : + (f⁻¹ᵉ* ⬝e* g)⁻¹ᵉ* ~* f ∘* g⁻¹ᵉ* := + by reflexivity + + definition pinv_trans_pinv_right {A B C : Type*} (f : A ≃* B) (g : C ≃* B) : + (f ⬝e* g⁻¹ᵉ*)⁻¹ᵉ* ~* f⁻¹ᵉ* ∘* g := + by reflexivity + + definition pinv_trans_pinv_pinv {A B C : Type*} (f : B ≃* A) (g : C ≃* B) : + (f⁻¹ᵉ* ⬝e* g⁻¹ᵉ*)⁻¹ᵉ* ~* f ∘* g := + by reflexivity + /- pointed equivalences between particular pointed types -/ -- TODO: remove is_equiv_apn, which is proven again here definition loopn_pequiv_loopn [constructor] (n : ℕ) (f : A ≃* B) : Ω[n] A ≃* Ω[n] B := - pequiv.MK2 (apn n f) (apn n f⁻¹ᵉ*) + pequiv.MK (apn n f) (apn n f⁻¹ᵉ*) abstract begin induction n with n IH, { apply pleft_inv}, @@ -1153,79 +1145,4 @@ namespace pointed apply apn_succ_phomotopy_in end - /- properties of ppmap, the pointed type of pointed maps -/ - definition pcompose_pconst [constructor] (f : B →* C) : f ∘* pconst A B ~* pconst A C := - phomotopy.mk (λa, respect_pt f) (idp_con _)⁻¹ - - definition pconst_pcompose [constructor] (f : A →* B) : pconst B C ∘* f ~* pconst A C := - phomotopy.mk (λa, rfl) (ap_constant _ _)⁻¹ - - definition ppcompose_left [constructor] (g : B →* C) : ppmap A B →* ppmap A C := - pmap.mk (pcompose g) (eq_of_phomotopy (pcompose_pconst g)) - - definition is_pequiv_ppcompose_left [instance] [constructor] (g : B →* C) [H : is_equiv g] : - is_equiv (@ppcompose_left A B C g) := - begin - fapply is_equiv.adjointify, - { exact (ppcompose_left (pequiv_of_pmap g H)⁻¹ᵉ*) }, - all_goals (intros f; esimp; apply eq_of_phomotopy), - { exact calc g ∘* ((pequiv_of_pmap g H)⁻¹ᵉ* ∘* f) - ~* (g ∘* (pequiv_of_pmap g H)⁻¹ᵉ*) ∘* f : passoc - ... ~* pid _ ∘* f : pwhisker_right f (pright_inv (pequiv_of_pmap g H)) - ... ~* f : pid_pcompose f }, - { exact calc (pequiv_of_pmap g H)⁻¹ᵉ* ∘* (g ∘* f) - ~* ((pequiv_of_pmap g H)⁻¹ᵉ* ∘* g) ∘* f : passoc - ... ~* pid _ ∘* f : pwhisker_right f (pleft_inv (pequiv_of_pmap g H)) - ... ~* f : pid_pcompose f } - end - - definition pequiv_ppcompose_left [constructor] (g : B ≃* C) : ppmap A B ≃* ppmap A C := - pequiv_of_pmap (ppcompose_left g) _ - - definition ppcompose_right [constructor] (f : A →* B) : ppmap B C →* ppmap A C := - pmap.mk (λg, g ∘* f) (eq_of_phomotopy (pconst_pcompose f)) - - definition pequiv_ppcompose_right [constructor] (f : A ≃* B) : ppmap B C ≃* ppmap A C := - begin - fapply pequiv.MK, - { exact ppcompose_right f }, - { exact ppcompose_right f⁻¹ᵉ* }, - { intro g, apply eq_of_phomotopy, refine !passoc ⬝* _, - refine pwhisker_left g !pright_inv ⬝* !pcompose_pid, }, - { intro g, apply eq_of_phomotopy, refine !passoc ⬝* _, - refine pwhisker_left g !pleft_inv ⬝* !pcompose_pid, }, - end - - definition loop_ppmap_commute (A B : Type*) : Ω(ppmap A B) ≃* (ppmap A (Ω B)) := - pequiv_of_equiv - (calc Ω(ppmap A B) ≃ (pconst A B ~* pconst A B) : pmap_eq_equiv _ _ - ... ≃ Σ(p : pconst A B ~ pconst A B), p pt ⬝ rfl = rfl : phomotopy.sigma_char - ... ≃ (A →* Ω B) : pmap.sigma_char) - (by reflexivity) - - definition papply [constructor] {A : Type*} (B : Type*) (a : A) : ppmap A B →* B := - pmap.mk (λ(f : A →* B), f a) idp - - definition papply_pcompose [constructor] {A : Type*} (B : Type*) (a : A) : ppmap A B →* B := - pmap.mk (λ(f : A →* B), f a) idp - - definition ppmap_pbool_pequiv [constructor] (B : Type*) : ppmap pbool B ≃* B := - begin - fapply pequiv.MK, - { exact papply B tt }, - { exact pbool_pmap }, - { intro f, fapply pmap_eq, - { intro b, cases b, exact !respect_pt⁻¹, reflexivity }, - { exact !con.left_inv⁻¹ }}, - { intro b, reflexivity }, - end - - definition papn_pt [constructor] (n : ℕ) (A B : Type*) : ppmap A B →* ppmap (Ω[n] A) (Ω[n] B) := - pmap.mk (λf, apn n f) (eq_of_phomotopy !apn_pconst) - - definition papn_fun [constructor] {n : ℕ} {A : Type*} (B : Type*) (p : Ω[n] A) : - ppmap A B →* Ω[n] B := - papply _ p ∘* papn_pt n A B - - end pointed diff --git a/hott/types/pointed2.hlean b/hott/types/pointed2.hlean index 80d04c164..c38b65ad7 100644 --- a/hott/types/pointed2.hlean +++ b/hott/types/pointed2.hlean @@ -15,10 +15,10 @@ Contains import algebra.homotopy_group eq2 -open pointed eq unit is_trunc trunc nat group is_equiv equiv sigma function +open pointed eq unit is_trunc trunc nat group is_equiv equiv sigma function bool namespace pointed - + variables {A B C : Type*} section psquare /- @@ -30,7 +30,7 @@ namespace pointed Then the following are operations on squares -/ - variables {A A' A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type*} + variables {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₃₂ : A₂₂ →* A₄₂} @@ -362,7 +362,7 @@ namespace pointed Squares of pointed homotopies -/ - variables {A B C : Type*} {f f' f₀₀ f₂₀ f₄₀ f₀₂ f₂₂ f₄₂ f₀₄ f₂₄ f₄₄ : A →* B} + variables {f f' f₀₀ f₂₀ f₄₀ f₀₂ f₂₂ f₄₂ f₀₄ f₂₄ f₄₄ : A →* B} {p₁₀ : f₀₀ ~* f₂₀} {p₃₀ : f₂₀ ~* f₄₀} {p₀₁ : f₀₀ ~* f₀₂} {p₂₁ : f₂₀ ~* f₂₂} {p₄₁ : f₄₀ ~* f₄₂} {p₁₂ : f₀₂ ~* f₂₂} {p₃₂ : f₂₂ ~* f₄₂} @@ -549,6 +549,76 @@ namespace pointed refine !phomotopy_of_eq_of_phomotopy ◾** idp ⬝ q, end + /- properties of ppmap, the pointed type of pointed maps -/ + definition pcompose_pconst [constructor] (f : B →* C) : f ∘* pconst A B ~* pconst A C := + phomotopy.mk (λa, respect_pt f) (idp_con _)⁻¹ + + definition pconst_pcompose [constructor] (f : A →* B) : pconst B C ∘* f ~* pconst A C := + phomotopy.mk (λa, rfl) (ap_constant _ _)⁻¹ + + definition ppcompose_left [constructor] (g : B →* C) : ppmap A B →* ppmap A C := + pmap.mk (pcompose g) (eq_of_phomotopy (pcompose_pconst g)) + + definition ppcompose_right [constructor] (f : A →* B) : ppmap B C →* ppmap A C := + pmap.mk (λg, g ∘* f) (eq_of_phomotopy (pconst_pcompose f)) + + /- TODO: give construction using pequiv.MK, which computes better (see comment for a start of the proof) -/ + definition pequiv_ppcompose_left [constructor] (g : B ≃* C) : ppmap A B ≃* ppmap A C := + pequiv.MK' (ppcompose_left g) (ppcompose_left g⁻¹ᵉ*) + begin intro f, apply eq_of_phomotopy, apply pinv_pcompose_cancel_left end + begin intro f, apply eq_of_phomotopy, apply pcompose_pinv_cancel_left end + -- pequiv.MK (ppcompose_left g) (ppcompose_left g⁻¹ᵉ*) + -- abstract begin + -- apply phomotopy_mk_ppmap (pinv_pcompose_cancel_left g), esimp, + -- refine !trans_refl ⬝ _, + -- refine _ ⬝ (!phomotopy_of_eq_con ⬝ (!phomotopy_of_eq_pcompose_left ⬝ + -- ap (pwhisker_left _) !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹, + + -- end end + -- abstract begin + -- exact sorry + -- end end + + definition pequiv_ppcompose_right [constructor] (f : A ≃* B) : ppmap B C ≃* ppmap A C := + begin + fapply pequiv.MK', + { exact ppcompose_right f }, + { exact ppcompose_right f⁻¹ᵉ* }, + { intro g, apply eq_of_phomotopy, apply pcompose_pinv_cancel_right }, + { intro g, apply eq_of_phomotopy, apply pinv_pcompose_cancel_right }, + end + + definition loop_ppmap_commute (A B : Type*) : Ω(ppmap A B) ≃* (ppmap A (Ω B)) := + pequiv_of_equiv + (calc Ω(ppmap A B) ≃ (pconst A B ~* pconst A B) : pmap_eq_equiv _ _ + ... ≃ Σ(p : pconst A B ~ pconst A B), p pt ⬝ rfl = rfl : phomotopy.sigma_char + ... ≃ (A →* Ω B) : pmap.sigma_char) + (by reflexivity) + + definition papply [constructor] {A : Type*} (B : Type*) (a : A) : ppmap A B →* B := + pmap.mk (λ(f : A →* B), f a) idp + + definition papply_pcompose [constructor] {A : Type*} (B : Type*) (a : A) : ppmap A B →* B := + pmap.mk (λ(f : A →* B), f a) idp + + definition ppmap_pbool_pequiv [constructor] (B : Type*) : ppmap pbool B ≃* B := + begin + fapply pequiv.MK', + { exact papply B tt }, + { exact pbool_pmap }, + { intro f, fapply pmap_eq, + { intro b, cases b, exact !respect_pt⁻¹, reflexivity }, + { exact !con.left_inv⁻¹ }}, + { intro b, reflexivity }, + end + + definition papn_pt [constructor] (n : ℕ) (A B : Type*) : ppmap A B →* ppmap (Ω[n] A) (Ω[n] B) := + pmap.mk (λf, apn n f) (eq_of_phomotopy !apn_pconst) + + definition papn_fun [constructor] {n : ℕ} {A : Type*} (B : Type*) (p : Ω[n] A) : + ppmap A B →* Ω[n] B := + papply _ p ∘* papn_pt n A B + definition pconst_pcompose_pconst (A B C : Type*) : pconst_pcompose (pconst A B) = pcompose_pconst (pconst B C) := idp @@ -688,7 +758,7 @@ namespace pointed section psquare - variables {A A' A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type*} + variables {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₃₂ : A₂₂ →* A₄₂} @@ -844,4 +914,59 @@ namespace pointed apply symm_trans_eq_of_eq_trans, exact (ap1_pcompose_pconst_right f)⁻¹ } end + open sigma.ops prod + definition pequiv.sigma_char {A B : Type*} : + (A ≃* B) ≃ Σ(f : A →* B), (Σ(g : B →* A), f ∘* g ~* pid B) × (Σ(h : B →* A), h ∘* f ~* pid A) := + begin + fapply equiv.MK, + { intro f, exact ⟨f, (⟨pequiv.to_pinv1 f, pequiv.pright_inv f⟩, + ⟨pequiv.to_pinv2 f, pequiv.pleft_inv f⟩)⟩, }, + { intro f, exact pequiv.mk' f.1 (pr1 f.2).1 (pr2 f.2).1 (pr1 f.2).2 (pr2 f.2).2 }, + { intro f, induction f with f v, induction v with hl hr, induction hl, induction hr, + reflexivity }, + { intro f, induction f, reflexivity } + end + + definition is_contr_pright_inv (f : A ≃* B) : is_contr (Σ(g : B →* A), f ∘* g ~* pid B) := + begin + fapply is_trunc_equiv_closed, + { exact !fiber.sigma_char ⬝e sigma_equiv_sigma_right (λg, !pmap_eq_equiv) }, + fapply is_contr_fiber_of_is_equiv, + exact pequiv.to_is_equiv (pequiv_ppcompose_left f) + end + + definition is_contr_pleft_inv (f : A ≃* B) : is_contr (Σ(h : B →* A), h ∘* f ~* pid A) := + begin + fapply is_trunc_equiv_closed, + { exact !fiber.sigma_char ⬝e sigma_equiv_sigma_right (λg, !pmap_eq_equiv) }, + fapply is_contr_fiber_of_is_equiv, + exact pequiv.to_is_equiv (pequiv_ppcompose_right f) + end + + definition pequiv_eq_equiv (f g : A ≃* B) : (f = g) ≃ f ~* g := + have Π(f : A →* B), is_prop ((Σ(g : B →* A), f ∘* g ~* pid B) × (Σ(h : B →* A), h ∘* f ~* pid A)), + begin + intro f, apply is_prop_of_imp_is_contr, intro v, + let f' := pequiv.sigma_char⁻¹ᵉ ⟨f, v⟩, + apply is_trunc_prod, exact is_contr_pright_inv f', exact is_contr_pleft_inv f' + end, + calc (f = g) ≃ (pequiv.sigma_char f = pequiv.sigma_char g) + : eq_equiv_fn_eq pequiv.sigma_char f g + ... ≃ (f = g :> (A →* B)) : subtype_eq_equiv + ... ≃ (f ~* g) : pmap_eq_equiv f g + + definition pequiv_eq {f g : A ≃* B} (H : f ~* g) : f = g := + (pequiv_eq_equiv f g)⁻¹ᵉ H + + open algebra + definition pequiv_of_isomorphism_of_eq {G₁ G₂ : Group} (p : G₁ = G₂) : + pequiv_of_isomorphism (isomorphism_of_eq p) = pequiv_of_eq (ap pType_of_Group p) := + begin + induction p, + apply pequiv_eq, + fapply phomotopy.mk, + { intro g, reflexivity }, + { apply is_prop.elim } + end + end pointed