From 25ae0e9dce8bab1d78770e6919f16272ef48c9d4 Mon Sep 17 00:00:00 2001 From: Ulrik Buchholtz Date: Sun, 6 Nov 2016 11:01:14 +0100 Subject: [PATCH] truncation level of pointed maps given connectivity of domain and truncation level of codomain --- pointed_pi.hlean | 179 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 179 insertions(+) create mode 100644 pointed_pi.hlean diff --git a/pointed_pi.hlean b/pointed_pi.hlean new file mode 100644 index 0000000..7b895d7 --- /dev/null +++ b/pointed_pi.hlean @@ -0,0 +1,179 @@ +/- +Copyright (c) 2016 Ulrik Buchholtz. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Ulrik Buchholtz +-/ + +import move_to_lib + +open eq pointed equiv sigma + +/- + The goal of this file is to give the truncation level + of the type of pointed maps, giving the connectivity of + the domain and the truncation level of the codomain. + This is is_trunc_pmap at the end. + + First we define the type of dependent pointed maps + as a tool, because these appear in the more general + statement is_trunc_ppi (the generality needed for induction). + + Unfortunately, some of these names (ppi) and notations (Π*) + clash with those in types.pi in the pi namespace. +-/ + +namespace pointed + + -- needs another name! (one more p?) + structure ppi (A : Type*) (P : A → Type*) := + (to_fun : Π a : A, P a) + (resp_pt : to_fun (Point A) = Point (P (Point A))) + + attribute ppi.to_fun [coercion] + + abbreviation ppi_resp_pt [unfold 3] := @ppi.resp_pt + + definition pointed_ppi [instance] [constructor] {A : Type*} + (P : A → Type*) : pointed (ppi A P) := + pointed.mk (ppi.mk (λ a, pt) idp) + + definition pppi [constructor] {A : Type*} (P : A → Type*) : Type* := + pointed.mk' (ppi A P) + + notation `Π*` binders `, ` r:(scoped P, pppi P) := r + + structure ppi_homotopy {A : Type*} {P : A → Type*} (f g : Π*(a : A), P a) := + (homotopy : f ~ g) + (homotopy_pt : homotopy pt ⬝ ppi_resp_pt g = ppi_resp_pt f) + + variables {A : Type*} {P : A → Type*} {f g : Π*(a : A), P a} + + infix ` ~~* `:50 := ppi_homotopy + abbreviation ppi_to_homotopy_pt [unfold 5] := @ppi_homotopy.homotopy_pt + abbreviation ppi_to_homotopy [coercion] [unfold 5] (p : f ~~* g) : Πa, f a = g a := + ppi_homotopy.homotopy p + + definition ppi_equiv_pmap (A B : Type*) : (Π*(a : A), B) ≃ (A →* B) := + begin + fapply equiv.MK, + { intro f, induction f with f p, exact pmap.mk f p }, + { intro f, induction f with f p, exact ppi.mk f p }, + { intro f, induction f with f p, reflexivity }, + { intro f, induction f with f p, reflexivity } + end + + definition ppi.sigma_char [constructor] {A : Type*} (P : A → Type*) + : (Π*(a : A), P a) ≃ Σ(f : (Π (a : A), P a)), f pt = pt := + begin + fapply equiv.MK : intros f, + { exact ⟨ f , ppi_resp_pt f ⟩ }, + all_goals cases f with f p, + { exact ppi.mk f p }, + all_goals reflexivity + end + + -- the same as pmap_eq + definition ppi_eq (h : f ~ g) : ppi_resp_pt f = h pt ⬝ ppi_resp_pt g → f = g := + begin + cases f with f p, cases g with g q, intro r, + esimp at *, + fapply apd011 ppi.mk, + { apply eq_of_homotopy h }, + { esimp, apply concato_eq, apply pathover_eq_Fl, apply inv_con_eq_of_eq_con, + rewrite [ap_eq_apd10, apd10_eq_of_homotopy], exact r } + end + + variables (f g) + + definition ppi_homotopy.sigma_char [constructor] + : (f ~~* g) ≃ Σ(p : f ~ g), p pt ⬝ ppi_resp_pt g = ppi_resp_pt f := + begin + fapply equiv.MK : intros h, + { exact ⟨h , ppi_to_homotopy_pt h⟩ }, + all_goals cases h with h p, + { exact ppi_homotopy.mk h p }, + all_goals reflexivity + end + + -- the same as pmap_eq_equiv + definition ppi_eq_equiv : (f = g) ≃ (f ~~* g) := + calc (f = g) ≃ ppi.sigma_char P f = ppi.sigma_char P g + : eq_equiv_fn_eq (ppi.sigma_char P) f g + ... ≃ Σ(p : ppi.to_fun f = ppi.to_fun g), + pathover (λh, h pt = pt) (ppi_resp_pt f) p (ppi_resp_pt g) + : sigma_eq_equiv _ _ + ... ≃ Σ(p : ppi.to_fun f = ppi.to_fun g), + ppi_resp_pt f = ap (λh, h pt) p ⬝ ppi_resp_pt g + : sigma_equiv_sigma_right + (λp, pathover_eq_equiv_Fl p (ppi_resp_pt f) (ppi_resp_pt g)) + ... ≃ Σ(p : ppi.to_fun f = ppi.to_fun g), + ppi_resp_pt f = apd10 p pt ⬝ ppi_resp_pt g + : sigma_equiv_sigma_right + (λp, equiv_eq_closed_right _ (whisker_right (ap_eq_apd10 p _) _)) + ... ≃ Σ(p : f ~ g), ppi_resp_pt f = p pt ⬝ ppi_resp_pt g + : sigma_equiv_sigma_left' eq_equiv_homotopy + ... ≃ Σ(p : f ~ g), p pt ⬝ ppi_resp_pt g = ppi_resp_pt f + : sigma_equiv_sigma_right (λp, eq_equiv_eq_symm _ _) + ... ≃ (f ~~* g) : ppi_homotopy.sigma_char f g + + definition ppi_loop_equiv_lemma (p : f ~ f) + : (p pt ⬝ ppi_resp_pt f = ppi_resp_pt f) ≃ (p pt = idp) := + calc (p pt ⬝ ppi_resp_pt f = ppi_resp_pt f) + ≃ (p pt ⬝ ppi_resp_pt f = idp ⬝ ppi_resp_pt f) + : equiv_eq_closed_right (p pt ⬝ ppi_resp_pt f) (inverse (idp_con (ppi_resp_pt f))) + ... ≃ (p pt = idp) + : eq_equiv_con_eq_con_right + + definition ppi_loop_equiv : (f = f) ≃ Π*(a : A), Ω (pType.mk (P a) (f a)) := + calc (f = f) ≃ (f ~~* f) + : ppi_eq_equiv + ... ≃ Σ(p : f ~ f), p pt ⬝ ppi_resp_pt f = ppi_resp_pt f + : ppi_homotopy.sigma_char f f + ... ≃ Σ(p : f ~ f), p pt = idp + : sigma_equiv_sigma_right + (λ p, ppi_loop_equiv_lemma f p) + ... ≃ Π*(a : A), pType.mk (f a = f a) idp + : ppi.sigma_char + ... ≃ Π*(a : A), Ω (pType.mk (P a) (f a)) + : erfl + +end pointed open pointed + +open is_trunc is_conn +section + variables (A : Type*) (n : ℕ₋₂) [H : is_conn (n.+1) A] + include H + + definition is_contr_ppi_match (P : A → (n.+1)-Type*) + : is_contr (Π*(a : A), P a) := + begin + apply is_contr.mk pt, + intro f, induction f with f p, + fapply ppi_eq, + { apply is_conn.elim n, esimp, exact p⁻¹ }, + { krewrite (is_conn.elim_β n), apply inverse, apply con.left_inv } + end + + definition is_trunc_ppi (k : ℕ₋₂) (P : A → (n.+1+2+k)-Type*) + : is_trunc k.+1 (Π*(a : A), P a) := + begin + induction k with k IH, + { apply is_prop_of_imp_is_contr, intro f, + apply is_contr_ppi_match }, + { apply is_trunc_succ_of_is_trunc_loop + (trunc_index.succ_le_succ (trunc_index.minus_two_le k)), + intro f, + apply @is_trunc_equiv_closed_rev _ _ k.+1 + (ppi_loop_equiv f), + apply IH, intro a, + apply ptrunctype.mk (Ω (pType.mk (P a) (f a))), + { apply is_trunc_loop, exact is_trunc_ptrunctype (P a) }, + { exact pt } } + end + + definition is_trunc_pmap (k : ℕ₋₂) (B : (n.+1+2+k)-Type*) + : is_trunc k.+1 (A →* B) := + @is_trunc_equiv_closed _ _ k.+1 (ppi_equiv_pmap A B) + (is_trunc_ppi A n k (λ a, B)) + +end