From dcb35008e1474a0abebe632b1dced120e5f8c009 Mon Sep 17 00:00:00 2001 From: Ulrik Buchholtz Date: Sat, 23 Jan 2016 14:15:59 -0500 Subject: [PATCH] feat(hott/homotopy): general connectivity elimination and the wedge connectivity lemma --- hott/book.md | 6 +- hott/homotopy/circle.hlean | 26 ++++++++ hott/homotopy/connectedness.hlean | 100 ++++++++++++++++++++++++++---- hott/homotopy/wedge.hlean | 63 ++++++++++++++++--- hott/init/path.hlean | 18 ++++-- hott/types/fiber.hlean | 23 +++++++ 6 files changed, 208 insertions(+), 28 deletions(-) diff --git a/hott/book.md b/hott/book.md index 5e0380c3a..371698ef8 100644 --- a/hott/book.md +++ b/hott/book.md @@ -22,7 +22,7 @@ The rows indicate the chapters, the columns the sections. | Ch 5 | - | . | ½ | - | - | . | . | ½ | | | | | | | | | Ch 6 | . | + | + | + | + | ½ | ½ | + | ¾ | ¼ | ¾ | + | . | | | | Ch 7 | + | + | + | - | ¾ | - | - | | | | | | | | | -| Ch 8 | ¾ | ¾ | - | - | - | - | - | - | - | - | | | | | | +| Ch 8 | ¾ | ¾ | - | - | ¼ | ¼ | - | - | - | - | | | | | | | Ch 9 | ¾ | + | + | ½ | ¾ | ½ | - | - | - | | | | | | | | Ch 10 | - | - | - | - | - | | | | | | | | | | | | Ch 11 | - | - | - | - | - | - | | | | | | | | | | @@ -145,8 +145,8 @@ Unless otherwise noted, the files are in the folder [homotopy](homotopy/homotopy - 8.2 (Connectedness of suspensions): [homotopy.connectedness](homotopy/connectedness.hlean) (different proof) - 8.3 (πk≤n of an n-connected space and π_{k fiber (λs : (Πb, P b), (λa, s (f a))) t), + { apply equiv.trans !fiber.sigma_char, + assert e' : Πr : g ~ h, + ((λa, r (f a)) = apd10 (p ⬝ q⁻¹)) + ≃ (ap (λv, (λa, v (f a))) (eq_of_homotopy r) ⬝ q = p), + { intro r, + refine equiv.trans _ (eq_con_inv_equiv_con_eq q p + (ap (λv a, v (f a)) (eq_of_homotopy r))), + rewrite [-(ap (λv a, v (f a)) (apd10_eq_of_homotopy r))], + rewrite [-(apd10_ap_precompose_dependent f (eq_of_homotopy r))], + apply equiv.symm, + apply eq_equiv_fn_eq (@apd10 A (λa, P (f a)) (λa, g (f a)) (λa, h (f a))) }, + apply equiv.trans (sigma.sigma_equiv_sigma_id e'), clear e', + apply equiv.trans (equiv.symm (sigma.sigma_equiv_sigma_left + eq_equiv_homotopy)), + apply equiv.symm, apply equiv.trans !fiber_eq_equiv, + apply sigma.sigma_equiv_sigma_id, intro r, + apply eq_equiv_eq_symm }, + apply @is_trunc_equiv_closed _ _ k e, clear e, + apply IH (λb : B, trunctype.mk (g b = h b) + (@is_trunc_eq (P b) (n +2+ k) (trunctype.struct (P b)) + (g b) (h b))) } + end + end + section universe variables u v parameters {n : trunc_index} {A : Type.{u}} {B : Type.{v}} {h : A → B} @@ -113,6 +153,44 @@ namespace homotopy end + -- as special case we get elimination principles for pointed connected types + namespace is_conn + open pointed Pointed unit + section + parameters {n : trunc_index} {A : Type*} + [H : is_conn n .+1 A] (P : A → n -Type) + + include H + protected definition rec : is_equiv (λs : Πa : A, P a, s (Point A)) := + @is_equiv_compose + (Πa : A, P a) (unit → P (Point A)) (P (Point A)) + (λs x, s (Point A)) (λf, f unit.star) + (is_conn_map.rec (is_conn_map_from_unit n A (Point A)) P) + (to_is_equiv (unit.unit_imp_equiv (P (Point A)))) + + protected definition elim : P (Point A) → (Πa : A, P a) := + @is_equiv.inv _ _ (λs, s (Point A)) rec + + protected definition elim_β (p : P (Point A)) : elim p (Point A) = p := + @is_equiv.right_inv _ _ (λs, s (Point A)) rec p + end + + section + parameters {n k : trunc_index} {A : Type*} + [H : is_conn n .+1 A] (P : A → (n +2+ k)-Type) + + include H + proposition elim_general (p : P (Point A)) + : is_trunc k (fiber (λs : (Πa : A, P a), s (Point A)) p) := + @is_trunc_equiv_closed + (fiber (λs x, s (Point A)) (λx, p)) + (fiber (λs, s (Point A)) p) + k + (equiv.symm (fiber.equiv_postcompose (to_fun (unit.unit_imp_equiv (P (Point A)))))) + (is_conn_map.elim_general (is_conn_map_from_unit n A (Point A)) P (λx, p)) + end + end is_conn + -- Lemma 7.5.2 definition minus_one_conn_of_surjective {A B : Type} (f : A → B) : is_surjective f → is_conn_map -1 f := diff --git a/hott/homotopy/wedge.hlean b/hott/homotopy/wedge.hlean index 179ef4880..2eb6b95d4 100644 --- a/hott/homotopy/wedge.hlean +++ b/hott/homotopy/wedge.hlean @@ -1,22 +1,19 @@ /- Copyright (c) 2016 Jakob von Raumer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jakob von Raumer +Authors: Jakob von Raumer, Ulrik Buchholtz The Wedge Sum of Two Pointed Types -/ -import hit.pointed_pushout +import hit.pointed_pushout .connectedness open eq pushout pointed Pointed +definition Wedge (A B : Type*) : Type* := Pushout (pconst Unit A) (pconst Unit B) + namespace wedge - section - variables (A B : Type*) - - definition Wedge : Type* := Pushout (pconst Unit A) (pconst Unit B) - -- TODO maybe find a cleaner proof - protected definition unit : A ≃* Wedge Unit A := + protected definition unit (A : Type*) : A ≃* Wedge Unit A := begin fconstructor, { fapply pmap.mk, intro a, apply pinr a, apply respect_pt }, @@ -30,6 +27,52 @@ namespace wedge apply con.left_inv, intro a, reflexivity }, end - - end end wedge + +open trunc is_trunc function homotopy +namespace wedge_extension +section + -- The wedge connectivity lemma (Lemma 8.6.2) + parameters {A B : Type*} (n m : trunc_index) + [cA : is_conn n .+2 A] [cB : is_conn m .+2 B] + (P : A → B → (m .+1 +2+ n .+1)-Type) + (f : Πa : A, P a (Point B)) + (g : Πb : B, P (Point A) b) + (p : f (Point A) = g (Point B)) + + include cA cB + private definition Q (a : A) : (n .+1)-Type := + trunctype.mk + (fiber (λs : (Πb : B, P a b), s (Point B)) (f a)) + (is_conn.elim_general (P a) (f a)) + + private definition Q_sec : Πa : A, Q a := + is_conn.elim Q (fiber.mk g p⁻¹) + + protected definition ext : Π(a : A)(b : B), P a b := + λa, fiber.point (Q_sec a) + + protected definition β_left (a : A) : ext a (Point B) = f a := + fiber.point_eq (Q_sec a) + + private definition coh_aux : Σq : ext (Point A) = g, + β_left (Point A) = ap (λs : (Πb : B, P (Point A) b), s (Point B)) q ⬝ p⁻¹ := + equiv.to_fun (fiber.fiber_eq_equiv (Q_sec (Point A)) (fiber.mk g p⁻¹)) + (is_conn.elim_β Q (fiber.mk g p⁻¹)) + + protected definition β_right (b : B) : ext (Point A) b = g b := + apd10 (sigma.pr1 coh_aux) b + + private definition lem : β_left (Point A) = β_right (Point B) ⬝ p⁻¹ := + begin + unfold β_right, unfold β_left, + krewrite (apd10_eq_ap_eval (sigma.pr1 coh_aux) (Point B)), + exact sigma.pr2 coh_aux, + end + + protected definition coh + : (β_left (Point A))⁻¹ ⬝ β_right (Point B) = p := + by rewrite [lem,con_inv,inv_inv,con.assoc,con.left_inv] + +end +end wedge_extension diff --git a/hott/init/path.hlean b/hott/init/path.hlean index f3b3be710..bece16eb6 100644 --- a/hott/init/path.hlean +++ b/hott/init/path.hlean @@ -233,6 +233,11 @@ namespace eq definition apd10' [unfold 6] {f g : Πx, P x} (a : A) (H : f = g) : f a = g a := eq.rec_on H idp + --apd10 is also ap evaluation + definition apd10_eq_ap_eval {f g : Πx, P x} (H : f = g) (a : A) + : apd10 H a = ap (λs : Πx, P x, s a) H := + eq.rec_on H idp + definition ap10 [reducible] [unfold 5] {f g : A → B} (H : f = g) : f ~ g := apd10 H definition ap11 {f g : A → B} (H : f = g) {x y : A} (p : x = y) : f x = g y := @@ -525,12 +530,17 @@ namespace eq ap (λh, h ∘ f) p = transport (λh : B → C, g ∘ f = h ∘ f) p idp := eq.rec_on p idp - definition apd10_ap_precompose (f : A → B) (g g' : B → C) (p : g = g') (a : A) : - apd10 (ap (λh : B → C, h ∘ f) p) a = apd10 p (f a) := + definition apd10_ap_precompose (f : A → B) (g g' : B → C) (p : g = g') : + apd10 (ap (λh : B → C, h ∘ f) p) = λa, apd10 p (f a) := eq.rec_on p idp - definition apd10_ap_postcompose (f : B → C) (g g' : A → B) (p : g = g') (a : A) : - apd10 (ap (λh : A → B, f ∘ h) p) a = ap f (apd10 p a) := + definition apd10_ap_precompose_dependent {C : B → Type} + (f : A → B) {g g' : Πb : B, C b} (p : g = g') + : apd10 (ap (λ(h : (Πb : B, C b))(a : A), h (f a)) p) = λa, apd10 p (f a) := + eq.rec_on p idp + + definition apd10_ap_postcompose (f : B → C) (g g' : A → B) (p : g = g') : + apd10 (ap (λh : A → B, f ∘ h) p) = λa, ap f (apd10 p a) := eq.rec_on p idp -- A special case of [tr_compose] which seems to come up a lot. diff --git a/hott/types/fiber.hlean b/hott/types/fiber.hlean index 24a9f8e6c..5b686faab 100644 --- a/hott/types/fiber.hlean +++ b/hott/types/fiber.hlean @@ -68,8 +68,31 @@ namespace fiber definition is_trunc_fun [reducible] (n : trunc_index) (f : A → B) := Π(b : B), is_trunc n (fiber f b) + definition is_contr_fun [reducible] (f : A → B) := is_trunc_fun -2 f + -- pre and post composition with equivalences + open function + protected definition equiv_postcompose {B' : Type} (g : B → B') [H : is_equiv g] + : fiber (g ∘ f) (g b) ≃ fiber f b := + calc + fiber (g ∘ f) (g b) ≃ Σa : A, g (f a) = g b : fiber.sigma_char + ... ≃ Σa : A, f a = b : begin + apply sigma_equiv_sigma_id, intro a, + apply equiv.symm, apply eq_equiv_fn_eq + end + ... ≃ fiber f b : fiber.sigma_char + + protected definition equiv_precompose {A' : Type} (g : A' → A) [H : is_equiv g] + : fiber (f ∘ g) b ≃ fiber f b := + calc + fiber (f ∘ g) b ≃ Σa' : A', f (g a') = b : fiber.sigma_char + ... ≃ Σa : A, f a = b : begin + apply sigma_equiv_sigma (equiv.mk g H), + intro a', apply erfl + end + ... ≃ fiber f b : fiber.sigma_char + end fiber open unit is_trunc