From d4ab6e15efcb2d28fa9b5725d1e350b70fdeccce Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Tue, 28 Nov 2017 08:25:51 +0100 Subject: [PATCH] small changes in colimit --- colimit/pointed.hlean | 69 ++++++++++++++++++++++------------------- colimit/seq_colim.hlean | 8 +++++ colimit/sequence.hlean | 18 +++++++++-- move_to_lib.hlean | 27 ++++++++++++++++ 4 files changed, 88 insertions(+), 34 deletions(-) diff --git a/colimit/pointed.hlean b/colimit/pointed.hlean index 2477fd3..36c1c85 100644 --- a/colimit/pointed.hlean +++ b/colimit/pointed.hlean @@ -11,6 +11,9 @@ namespace seq_colim definition pseq_colim [constructor] {X : ℕ → Type*} (f : pseq_diagram X) : Type* := pointed.MK (seq_colim f) (@sι _ _ 0 pt) + variables {A A' : ℕ → Type*} {f : pseq_diagram A} {f' : pseq_diagram A'} + {τ : Πn, A n →* A' n} {H : Πn, τ (n+1) ∘* f n ~* f' n ∘* τ n} + definition inclusion_pt {X : ℕ → Type*} (f : pseq_diagram X) (n : ℕ) : inclusion f (Point (X n)) = Point (pseq_colim f) := begin @@ -162,47 +165,45 @@ namespace seq_colim theorem prep0_succ_lemma {A : ℕ → Type*} (f : pseq_diagram A) (n : ℕ) (p : rep0 (λn x, f n x) n pt = rep0 (λn x, f n x) n pt) (q : prep0 f n (Point (A 0)) = Point (A n)) - : loop_equiv_eq_closed (ap (@f n) q ⬝ respect_pt (@f n)) (ap (@f n) p) = Ω→(@f n) (loop_equiv_eq_closed q p) := by rewrite [▸*, con_inv, ↑ap1_gen, +ap_con, ap_inv, +con.assoc] - variables {A : ℕ → Type} (f : seq_diagram A) - definition succ_add_tr_rep {n : ℕ} (k : ℕ) (x : A n) - : transport A (succ_add n k) (rep f k (f x)) = rep f (succ k) x := - begin - induction k with k p, - reflexivity, - exact tr_ap A succ (succ_add n k) _ ⬝ (fn_tr_eq_tr_fn (succ_add n k) f _)⁻¹ ⬝ ap (@f _) p, - end + -- definition succ_add_tr_rep {A : ℕ → Type} (f : seq_diagram A) {n : ℕ} (k : ℕ) (x : A n) + -- : transport A (succ_add n k) (rep f k (f x)) = rep f (succ k) x := + -- begin + -- induction k with k p, + -- reflexivity, + -- exact tr_ap A succ (succ_add n k) _ ⬝ (fn_tr_eq_tr_fn (succ_add n k) f _)⁻¹ ⬝ ap (@f _) p, + -- end - definition succ_add_tr_rep_succ {n : ℕ} (k : ℕ) (x : A n) - : succ_add_tr_rep f (succ k) x = tr_ap A succ (succ_add n k) _ ⬝ - (fn_tr_eq_tr_fn (succ_add n k) f _)⁻¹ ⬝ ap (@f _) (succ_add_tr_rep f k x) := - by reflexivity + -- definition succ_add_tr_rep_succ {A : ℕ → Type} (f : seq_diagram A) {n : ℕ} (k : ℕ) (x : A n) + -- : succ_add_tr_rep f (succ k) x = tr_ap A succ (succ_add n k) _ ⬝ + -- (fn_tr_eq_tr_fn (succ_add n k) f _)⁻¹ ⬝ ap (@f _) (succ_add_tr_rep f k x) := + -- by reflexivity - definition code_glue_equiv [constructor] {n : ℕ} (k : ℕ) (x y : A n) - : rep f k (f x) = rep f k (f y) ≃ rep f (succ k) x = rep f (succ k) y := - begin - refine eq_equiv_fn_eq_of_equiv (equiv_ap A (succ_add n k)) _ _ ⬝e _, - apply eq_equiv_eq_closed, - exact succ_add_tr_rep f k x, - exact succ_add_tr_rep f k y - end + -- definition code_glue_equiv [constructor] {A : ℕ → Type} (f : seq_diagram A) {n : ℕ} (k : ℕ) (x y : A n) + -- : rep f k (f x) = rep f k (f y) ≃ rep f (succ k) x = rep f (succ k) y := + -- begin + -- refine eq_equiv_fn_eq_of_equiv (equiv_ap A (succ_add n k)) _ _ ⬝e _, + -- apply eq_equiv_eq_closed, + -- exact succ_add_tr_rep f k x, + -- exact succ_add_tr_rep f k y + -- end - theorem code_glue_equiv_ap {n : ℕ} {k : ℕ} {x y : A n} (p : rep f k (f x) = rep f k (f y)) - : code_glue_equiv f (succ k) x y (ap (@f _) p) = ap (@f _) (code_glue_equiv f k x y p) := - begin - rewrite [▸*, +ap_con, ap_inv, +succ_add_tr_rep_succ, con_inv, inv_con_inv_right, +con.assoc], - apply whisker_left, - rewrite [- +con.assoc], apply whisker_right, rewrite [- +ap_compose'], - note s := (eq_top_of_square (natural_square_tr - (λx, fn_tr_eq_tr_fn (succ_add n k) f x ⬝ (tr_ap A succ (succ_add n k) (f x))⁻¹) p))⁻¹ᵖ, - rewrite [inv_con_inv_right at s, -con.assoc at s], exact s - end + -- theorem code_glue_equiv_ap {n : ℕ} {k : ℕ} {x y : A n} (p : rep f k (f x) = rep f k (f y)) + -- : code_glue_equiv f (succ k) x y (ap (@f _) p) = ap (@f _) (code_glue_equiv f k x y p) := + -- begin + -- rewrite [▸*, +ap_con, ap_inv, +succ_add_tr_rep_succ, con_inv, inv_con_inv_right, +con.assoc], + -- apply whisker_left, + -- rewrite [- +con.assoc], apply whisker_right, rewrite [- +ap_compose'], + -- note s := (eq_top_of_square (natural_square_tr + -- (λx, fn_tr_eq_tr_fn (succ_add n k) f x ⬝ (tr_ap A succ (succ_add n k) (f x))⁻¹) p))⁻¹ᵖ, + -- rewrite [inv_con_inv_right at s, -con.assoc at s], exact s + -- end definition pseq_colim_loop {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) : - Ω (pseq_colim f) ≃* pseq_colim (λn, Ω→(f n)) := + Ω (pseq_colim f) ≃* pseq_colim (λn, Ω→ (f n)) := begin fapply pequiv_of_equiv, { refine !seq_colim_eq_equiv0 ⬝e _, @@ -216,6 +217,10 @@ namespace seq_colim pseq_colim_loop f ∘* Ω→ (pinclusion f n) ~* pinclusion (λn, Ω→(f n)) n := sorry + definition pseq_colim_loop_natural (n : ℕ) : psquare (pseq_colim_loop f) (pseq_colim_loop f') + (Ω→ (pseq_colim_functor τ H)) (pseq_colim_functor (λn, Ω→ (τ n)) (λn, ap1_psquare (H n))) := + sorry + definition pseq_diagram_pfiber {A A' : ℕ → Type*} {f : pseq_diagram A} {f' : pseq_diagram A'} (g : Πn, A n →* A' n) (p : Πn, g (succ n) ∘* f n ~* f' n ∘* g n) : pseq_diagram (λk, pfiber (g k)) := diff --git a/colimit/seq_colim.hlean b/colimit/seq_colim.hlean index 53551c0..1ddf46e 100644 --- a/colimit/seq_colim.hlean +++ b/colimit/seq_colim.hlean @@ -602,6 +602,7 @@ begin exact (g_star_path_right_step g e w k x @(g_star_path_right g e w k)).2 }} end + /- We now define the map back, and show using this induction principle that the composites are the identity -/ variable {P} @@ -742,6 +743,13 @@ begin intro n p, refine whisker_right _ (!lrep_irrel2⁻² ⬝ !ap_inv⁻¹) ⬝ !ap_con⁻¹ } end +-- definition seq_colim_eq_equiv0'_natural {a₀ a₁ : A 0} {a₀' a₁' : A' 0} (p₀ : τ a₀ = a₀') +-- (p₁ : τ a₁ = a₁') : +-- hsquare (seq_colim_eq_equiv0' f a₀ a₁) (seq_colim_eq_equiv0' f' a₀' a₁') +-- (pointed.ap1_gen (seq_colim_functor τ p) (ap (ι' f' 0) p₀) (ap (ι' f' 0) p₁)) +-- (seq_colim_functor (λn, pointed.ap1_gen (@τ _)) _) := +-- _ + definition seq_colim_eq_equiv0 (a₀ a₁ : A 0) : ι f a₀ = ι f a₁ ≃ seq_colim (id0_seq_diagram f a₀ a₁) := seq_colim_eq_equiv0' f a₀ a₁ ⬝e seq_colim_id_equiv_seq_colim_id0 f a₀ a₁ diff --git a/colimit/sequence.hlean b/colimit/sequence.hlean index 3ab11be..f126496 100644 --- a/colimit/sequence.hlean +++ b/colimit/sequence.hlean @@ -152,7 +152,7 @@ namespace seq_colim { apply pathover_ap, exact apo f IH} end - variable {f} + variables {f f'} definition is_trunc_fun_lrep (k : ℕ₋₂) (H : n ≤ m) (H2 : Πn, is_trunc_fun k (@f n)) : is_trunc_fun k (lrep f H) := begin induction H with m H IH, apply is_trunc_fun_id, exact is_trunc_fun_compose k (H2 m) IH end @@ -161,7 +161,21 @@ namespace seq_colim is_conn_fun k (lrep f H) := begin induction H with m H IH, apply is_conn_fun_id, exact is_conn_fun_compose k (H2 m) IH end - variable (f) + definition lrep_natural (τ : Π⦃n⦄, A n → A' n) (p : Π⦃n⦄ (a : A n), τ (f a) = f' (τ a)) + {n m : ℕ} (H : n ≤ m) (a : A n) : τ (lrep f H a) = lrep f' H (τ a) := + begin + induction H with m H IH, reflexivity, exact p (lrep f H a) ⬝ ap (@f' m) IH + end + + definition rep_natural (τ : Π⦃n⦄, A n → A' n) (p : Π⦃n⦄ (a : A n), τ (f a) = f' (τ a)) + {n : ℕ} (k : ℕ) (a : A n) : τ (rep f k a) = rep f' k (τ a) := + lrep_natural τ p _ a + + definition rep0_natural (τ : Π⦃n⦄, A n → A' n) (p : Π⦃n⦄ (a : A n), τ (f a) = f' (τ a)) + (k : ℕ) (a : A 0) : τ (rep0 f k a) = rep0 f' k (τ a) := + lrep_natural τ p _ a + + variables (f f') end generalized_lrep diff --git a/move_to_lib.hlean b/move_to_lib.hlean index 9e23f60..201fad4 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -732,6 +732,33 @@ by induction q'; reflexivity -- end --rexact @(ap pathover_pr1) _ idpo _, + definition sigma_functor_compose {A A' A'' : Type} {B : A → Type} {B' : A' → Type} + {B'' : A'' → Type} {f' : A' → A''} {f : A → A'} (g' : Πa, B' a → B'' (f' a)) + (g : Πa, B a → B' (f a)) (x : Σa, B a) : + sigma_functor f' g' (sigma_functor f g x) = sigma_functor (f' ∘ f) (λa, g' (f a) ∘ g a) x := + begin + reflexivity + end + + definition sigma_functor_homotopy {A A' : Type} {B : A → Type} {B' : A' → Type} + {f f' : A → A'} {g : Πa, B a → B' (f a)} {g' : Πa, B a → B' (f' a)} (h : f ~ f') + (k : Πa b, g a b =[h a] g' a b) (x : Σa, B a) : sigma_functor f g x = sigma_functor f' g' x := + sigma_eq (h x.1) (k x.1 x.2) + + variables {A₀₀ A₂₀ A₀₂ A₂₂ : Type} + {B₀₀ : A₀₀ → Type} {B₂₀ : A₂₀ → Type} {B₀₂ : A₀₂ → Type} {B₂₂ : A₂₂ → Type} + {f₁₀ : A₀₀ → A₂₀} {f₁₂ : A₀₂ → A₂₂} {f₀₁ : A₀₀ → A₀₂} {f₂₁ : A₂₀ → A₂₂} + {g₁₀ : Πa, B₀₀ a → B₂₀ (f₁₀ a)} {g₁₂ : Πa, B₀₂ a → B₂₂ (f₁₂ a)} + {g₀₁ : Πa, B₀₀ a → B₀₂ (f₀₁ a)} {g₂₁ : Πa, B₂₀ a → B₂₂ (f₂₁ a)} + + definition sigma_functor_hsquare (h : hsquare f₁₀ f₁₂ f₀₁ f₂₁) + (k : Πa (b : B₀₀ a), g₂₁ _ (g₁₀ _ b) =[h a] g₁₂ _ (g₀₁ _ b)) : + hsquare (sigma_functor f₁₀ g₁₀) (sigma_functor f₁₂ g₁₂) + (sigma_functor f₀₁ g₀₁) (sigma_functor f₂₁ g₂₁) := + λx, sigma_functor_compose g₂₁ g₁₀ x ⬝ + sigma_functor_homotopy h k x ⬝ + (sigma_functor_compose g₁₂ g₀₁ x)⁻¹ + end sigma open sigma namespace group