diff --git a/cohomology/projective_space.hlean b/cohomology/projective_space.hlean index c2272f5..14b691f 100644 --- a/cohomology/projective_space.hlean +++ b/cohomology/projective_space.hlean @@ -119,7 +119,7 @@ namespace temp refine @(is_trunc_equiv_closed _ _) (fEinf (- 1) 0 dec_star), apply equiv_of_isomorphism, refine Einf_isomorphism fserre 0 _ _, - intro r H, --apply is_contr_fD2, change (- 1) - (- 1) >[ℤ] (- 0) - (r + 1), + intro r H, exact sorry, exact sorry --apply is_contr_fD2, change (- 1) - (- 1) >[ℤ] (- 0) - (r + 1), -- apply is_contr_fD, change (-0) - (r + 1) >[ℤ] 0, --exact sub_nat_lt 0 r, -- intro r H, apply is_contr_fD, change 0 + (r + 1) >[ℤ] 0, diff --git a/colimit/local_ext.hlean b/colimit/local_ext.hlean new file mode 100644 index 0000000..f5dab2b --- /dev/null +++ b/colimit/local_ext.hlean @@ -0,0 +1,83 @@ +/- +Copyright (c) 2016 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Floris van Doorn, Egbert Rijke +-/ + +import hit.two_quotient .seq_colim + +open eq prod sum two_quotient sigma function relation e_closure nat seq_colim + +namespace localization +section quasi_local_extension + + universe variables u v w + parameters {A : Type.{u}} {P : A → Type.{v}} {Q : A → Type.{w}} (F : Πa, P a → Q a) + definition is_local [class] (Y : Type) : Type := + Π(a : A), is_equiv (λg, g ∘ F a : (Q a → Y) → (P a → Y)) + + + + section + parameter (X : Type.{max u v w}) + local abbreviation Y := X + Σa, (P a → X) × Q a + + -- do we want to remove the contractible pairs? + inductive qleR : Y → Y → Type := + | J : Π{a : A} (f : P a → X) (p : P a), qleR (inr ⟨a, (f, F a p)⟩) (inl (f p)) + | k : Π{a : A} (g : Q a → X) (q : Q a), qleR (inl (g q)) (inr ⟨a, (g ∘ F a, q)⟩) + + inductive qleQ : Π⦃y₁ y₂ : Y⦄, e_closure qleR y₁ y₂ → e_closure qleR y₁ y₂ → Type := + | K : Π{a : A} (g : Q a → X) (p : P a), qleQ [qleR.k g (F a p)] [qleR.J (g ∘ F a) p]⁻¹ʳ + + definition one_step_localization : Type := two_quotient qleR qleQ + definition incl : X → one_step_localization := incl0 _ _ ∘ inl + + end + variables (X : Type.{max u v w}) {Z : Type} + + definition n_step_localization : ℕ → Type := + nat.rec X (λn Y, localization.one_step_localization F Y) + + definition incln (n : ℕ) : + n_step_localization X n → n_step_localization X (succ n) := + localization.incl F (n_step_localization X n) + + -- localization if P and Q consist of ω-compact types + definition localization : Type := seq_colim (incln X) + definition incll : X → localization X := ι' _ 0 + + protected definition rec {P : localization X → Type} [Πz, is_local (P z)] + (H : Πx, P (incll X x)) (z : localization X) : P z := + begin + exact sorry + end + + definition extend {Y Z : Type} (f : Y → Z) [is_local Z] (x : one_step_localization Y) : Z := + begin + induction x, + { induction a, + { exact f a}, + { induction a with a v, induction v with f q, exact sorry}}, + { exact sorry}, + { exact sorry} + end + + protected definition elim {Y : Type} [is_local Y] + (H : X → Y) (z : localization X) : Y := + begin + induction z with n x n x, + { induction n with n IH, + { exact H x}, + induction x, + { induction a, + { exact IH a}, + { induction a with a v, induction v with f q, exact sorry}}, + { exact sorry}, + exact sorry}, + exact sorry + end + + +end quasi_local_extension +end localization diff --git a/colimit/omega_compact.hlean b/colimit/omega_compact.hlean new file mode 100644 index 0000000..3f98581 --- /dev/null +++ b/colimit/omega_compact.hlean @@ -0,0 +1,162 @@ +/- +Copyright (c) 2015 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Floris van Doorn, Egbert Rijke +-/ + +import .seq_colim types.unit + +open eq nat is_equiv equiv is_trunc pi unit function prod unit sigma sigma.ops sum prod trunc fin + algebra + +namespace seq_colim + + universe variable u + variables {A : ℕ → Type.{u}} (f : seq_diagram A) + variables {n : ℕ} (a : A n) + + definition arrow_colim_of_colim_arrow [unfold 4] {X : Type} + (g : seq_colim (seq_diagram_arrow_left f X)) (x : X) : seq_colim f := + begin induction g with n g n g, exact ι f (g x), exact glue f (g x) end + + definition omega_compact [class] (X : Type) : Type := + Π⦃A : ℕ → Type⦄ (f : seq_diagram A), + is_equiv (arrow_colim_of_colim_arrow f : + seq_colim (seq_diagram_arrow_left f X) → (X → seq_colim f)) + + definition equiv_of_omega_compact [unfold 4] (X : Type) [H : omega_compact X] + {A : ℕ → Type} (f : seq_diagram A) : + seq_colim (seq_diagram_arrow_left f X) ≃ (X → seq_colim f) := + equiv.mk _ (H f) + + definition omega_compact_of_equiv [unfold 4] (X : Type) + (H : Π⦃A : ℕ → Type⦄ (f : seq_diagram A), + seq_colim (seq_diagram_arrow_left f X) ≃ (X → seq_colim f)) + (p : Π⦃A : ℕ → Type⦄ (f : seq_diagram A) {n : ℕ} (g : X → A n) (x : X), + H f (ι _ g) x = ι _ (g x)) + (q : Π⦃A : ℕ → Type⦄ (f : seq_diagram A) {n : ℕ} (g : X → A n) (x : X), + square (p f (@f n ∘ g) x) (p f g x) (ap (λg, H f g x) + (glue (seq_diagram_arrow_left f X) g)) (glue f (g x))) + : omega_compact X := + λA f, is_equiv_of_equiv_of_homotopy (H f) + begin + intro g, apply eq_of_homotopy, intro x, + induction g with n g n g, + { exact p f g x }, + { apply eq_pathover, refine _ ⬝hp !elim_glue⁻¹, exact q f g x } + end + + local attribute is_contr_seq_colim [instance] + definition is_contr_empty_arrow [instance] (X : Type) : is_contr (empty → X) := + by apply is_trunc_pi; contradiction + + definition omega_compact_empty [instance] [constructor] : omega_compact empty := + begin + intro A f, + fapply adjointify, + { intro g, exact ι' _ 0 empty.elim}, + { intro g, apply eq_of_homotopy, contradiction}, + { intro h, apply is_prop.elim} + end + + definition omega_compact_unit' [instance] [constructor] : omega_compact unit := + begin + intro A f, + fapply adjointify, + { intro g, induction g ⋆, + { exact ι _ (λx, a)}, + { apply glue}}, + { intro g, apply eq_of_homotopy, intro u, induction u, + induction g ⋆, + { reflexivity}, + { esimp, apply eq_pathover_id_right, apply hdeg_square, + refine ap_compose (λx, arrow_colim_of_colim_arrow f x ⋆) _ _ ⬝ _, + refine ap02 _ !elim_glue ⬝ _, apply elim_glue}}, + { intro h, induction h with n h n h, + { esimp, apply ap (ι' _ n), apply unit_arrow_eq}, + { esimp, apply eq_pathover_id_right, + refine ap_compose' (seq_colim.elim _ _ _) _ _ ⬝ph _, + refine ap02 _ !elim_glue ⬝ph _, + refine !elim_glue ⬝ph _, + refine _ ⬝pv natural_square_tr (@glue _ (seq_diagram_arrow_left f unit) n) (unit_arrow_eq h), + refine _ ⬝ (ap_compose (ι' _ _) _ _)⁻¹, + apply ap02, unfold [seq_diagram_arrow_left], + apply unit_arrow_eq_compose}} + end + + -- The following is a start of a different proof that unit is omega-compact, + -- which proves first that the types are equivalent + definition omega_compact_unit [instance] [constructor] : omega_compact unit := + begin + fapply omega_compact_of_equiv, + { intro A f, refine _ ⬝e !arrow_unit_left⁻¹ᵉ, fapply seq_colim_equiv, + { intro n, apply arrow_unit_left }, + intro n f, reflexivity }, + { intros, induction x, reflexivity }, + { intros, induction x, esimp, apply hdeg_square, exact !elim_glue ⬝ !idp_con }, + end + + local attribute equiv_of_omega_compact [constructor] + definition omega_compact_prod [instance] [constructor] {X Y : Type} [omega_compact.{_ u} X] + [omega_compact.{u u} Y] : omega_compact.{_ u} (X × Y) := + begin + fapply omega_compact_of_equiv, + { intro A f, + exact calc + seq_colim (seq_diagram_arrow_left f (X × Y)) + ≃ seq_colim (seq_diagram_arrow_left (seq_diagram_arrow_left f Y) X) : + begin + apply seq_colim_equiv (λn, !imp_imp_equiv_prod_imp⁻¹ᵉ), + intro n f, reflexivity + end + ... ≃ (X → seq_colim (seq_diagram_arrow_left f Y)) : !equiv_of_omega_compact + ... ≃ (X → Y → seq_colim f) : arrow_equiv_arrow_right _ !equiv_of_omega_compact + ... ≃ (X × Y → seq_colim f) : imp_imp_equiv_prod_imp }, + { intros, induction x with x y, reflexivity }, + { intros, induction x with x y, apply hdeg_square, + refine ap_compose (λz, arrow_colim_of_colim_arrow f z y) _ _ ⬝ _, + refine ap02 _ (ap_compose (λz, arrow_colim_of_colim_arrow _ z x) _ _) ⬝ _, + refine ap02 _ (ap02 _ !elim_glue) ⬝ _, refine ap02 _ (ap02 _ !idp_con) ⬝ _, esimp, + refine ap02 _ !elim_glue ⬝ _, apply elim_glue } + end + +definition not_omega_compact_nat : ¬(omega_compact.{0 0} ℕ) := +assume H, +let e := equiv_of_omega_compact ℕ seq_diagram_fin ⬝e + arrow_equiv_arrow_right _ seq_colim_fin_equiv in +begin +-- check_expr e, + have Πx, ∥ Σn, Πm, e x m < n ∥, + begin + intro f, induction f using seq_colim.rec_prop with n f, + refine tr ⟨n, _⟩, intro m, exact is_lt (f m) + end, + induction this (e⁻¹ᵉ id) with x, induction x with n H2, + apply lt.irrefl n, + refine lt_of_le_of_lt (le_of_eq _) (H2 n), + exact ap10 (right_inv e id)⁻¹ n +end + +exit + print seq_diagram_over + definition seq_colim_over_equiv {X : Type} {A : X → ℕ → Type} (g : Π⦃x n⦄, A x n → A x (succ n)) + (x : X) + : @seq_colim_over _ (constant_seq X) _ _ ≃ seq_colim (@g x) := + begin + + end + + definition seq_colim_pi_equiv {X : Type} {A : X → ℕ → Type} (g : Π⦃x n⦄, A x n → A x (succ n)) + [omega_compact X] : (Πx, seq_colim (@g x)) ≃ seq_colim (seq_diagram_pi g) := + -- calc +-- (Πx, seq_colim (@g x)) ≃ Πx, seq_colim (@g x) + begin + refine !pi_equiv_arrow_sigma ⬝e _, + refine sigma_equiv_sigma_left (arrow_equiv_arrow_right X (sigma_equiv_sigma_left (seq_colim_constant_seq X)⁻¹ᵉ)) ⬝e _, + exact sigma_equiv_sigma_left (arrow_equiv_arrow_right X _) ⬝e _, + end + + set_option pp.universes true + print seq_diagram_arrow_left + +end seq_colim diff --git a/colimit/omega_compact_sum.hlean b/colimit/omega_compact_sum.hlean new file mode 100644 index 0000000..0f993a4 --- /dev/null +++ b/colimit/omega_compact_sum.hlean @@ -0,0 +1,158 @@ +import .omega_compact ..homotopy.fwedge + +open eq nat seq_colim is_trunc equiv is_equiv trunc sigma sum pi function algebra sigma.ops + +variables {A A' : ℕ → Type} (f : seq_diagram A) (f' : seq_diagram A') {n : ℕ} (a : A n) +universe variable u + +definition kshift_up (k : ℕ) (x : seq_colim f) : seq_colim (kshift_diag f k) := +begin + induction x with n a n a, + { apply ι' (kshift_diag f k) n, exact lrep f (le_add_left n k) a }, + { exact ap (ι _) (lrep_f f _ a ⬝ lrep_irrel f _ _ a ⬝ !f_lrep⁻¹) ⬝ !glue } +end + +definition kshift_down [unfold 4] (k : ℕ) (x : seq_colim (kshift_diag f k)) : seq_colim f := +begin + induction x with n a n a, + { exact ι' f (k + n) a }, + { exact glue f a } +end + +definition kshift_equiv_eq_kshift_up (k : ℕ) (a : A n) : kshift_equiv f k (ι f a) = kshift_up f k (ι f a) := +begin + induction k with k p, + { exact ap (ι _) !lrep_eq_transport⁻¹ }, + { exact sorry } +end + +definition kshift_equiv2 [constructor] (k : ℕ) : seq_colim f ≃ seq_colim (kshift_diag f k) := +begin + refine equiv_change_fun (kshift_equiv f k) _, + exact kshift_up f k, + intro x, induction x with n a n a, + { exact kshift_equiv_eq_kshift_up f k a }, + { exact sorry } +end + +definition kshift_equiv_inv_eq_kshift_down (k : ℕ) (a : A (k + n)) : + kshift_equiv_inv f k (ι' (kshift_diag f k) n a) = kshift_down f k (ι' (kshift_diag f k) n a) := +begin + induction k with k p, + { exact apd011 (ι' _) _ !pathover_tr⁻¹ᵒ }, + { exact sorry } +end + +definition kshift_equiv_inv2 [constructor] (k : ℕ) : seq_colim (kshift_diag f k) ≃ seq_colim f := +begin + refine equiv_change_fun (equiv_change_inv (kshift_equiv_inv f k) _) _, + { exact kshift_up f k }, + { intro x, induction x with n a n a, + { exact kshift_equiv_eq_kshift_up f k a }, + { exact sorry }}, + { exact kshift_down f k }, + { intro x, induction x with n a n a, + { exact !kshift_equiv_inv_eq_kshift_down }, + { exact sorry }} +end + +definition seq_colim_over_weakened_sequence [unfold 5] (x : seq_colim f) : + seq_colim_over (weakened_sequence f f') x ≃ seq_colim f' := +begin + induction x with n a n a, + { exact kshift_equiv_inv2 f' n }, + { apply equiv_pathover_inv, apply arrow_pathover_constant_left, intro x, + apply pathover_of_tr_eq, refine !seq_colim_over_glue ⬝ _, exact sorry } +end + +definition seq_colim_prod' [constructor] : seq_colim (seq_diagram_prod f f') ≃ seq_colim f × seq_colim f' := +calc + seq_colim (seq_diagram_prod f f') ≃ seq_colim (seq_diagram_sigma (weakened_sequence f f')) : + by exact seq_colim_equiv (λn, !sigma.equiv_prod⁻¹ᵉ) (λn a, idp) + ... ≃ Σ(x : seq_colim f), seq_colim_over (weakened_sequence f f') x : + by exact (sigma_seq_colim_over_equiv _ (weakened_sequence f f'))⁻¹ᵉ + ... ≃ Σ(x : seq_colim f), seq_colim f' : + by exact sigma_equiv_sigma_right (seq_colim_over_weakened_sequence f f') + ... ≃ seq_colim f × seq_colim f' : + by exact sigma.equiv_prod (seq_colim f) (seq_colim f') + +open prod prod.ops +example {a' : A' n} : seq_colim_prod' f f' (ι _ (a, a')) = (ι f a, ι f' a') := idp + +definition seq_colim_prod_inv {a' : A' n} : (seq_colim_prod' f f')⁻¹ᵉ (ι f a, ι f' a') = (ι _ (a, a')) := +begin + exact sorry +end + +definition prod_seq_colim_of_seq_colim_prod (x : seq_colim (seq_diagram_prod f f')) : + seq_colim f × seq_colim f' := +begin + induction x with n x n x, + { exact (ι f x.1, ι f' x.2) }, + { exact prod_eq (glue f x.1) (glue f' x.2) } +end + +definition seq_colim_prod [constructor] : + seq_colim (seq_diagram_prod f f') ≃ seq_colim f × seq_colim f' := +begin + refine equiv_change_fun (seq_colim_prod' f f') _, + exact prod_seq_colim_of_seq_colim_prod f f', + intro x, induction x with n x n x, + { reflexivity }, + { induction x with a a', apply eq_pathover, apply hdeg_square, esimp, + refine _ ⬝ !elim_glue⁻¹, + refine ap_compose ((sigma.equiv_prod (seq_colim f) (seq_colim f') ∘ + sigma_equiv_sigma_right (seq_colim_over_weakened_sequence f f')) ∘ + sigma_colim_of_colim_sigma (weakened_sequence f f')) _ _ ⬝ _, + refine ap02 _ (!elim_glue ⬝ !idp_con) ⬝ _, + refine !ap_compose ⬝ _, refine ap02 _ !elim_glue ⬝ _, + refine !ap_compose ⬝ _, esimp, refine ap02 _ !ap_sigma_functor_id_sigma_eq ⬝ _, + apply eq_of_fn_eq_fn (prod_eq_equiv _ _), apply pair_eq, + { exact !ap_compose'⁻¹ ⬝ !sigma_eq_pr1 ⬝ !prod_eq_pr1⁻¹ }, + { refine !ap_compose'⁻¹ ⬝ _ ⬝ !prod_eq_pr2⁻¹, esimp, + refine !sigma_eq_pr2_constant ⬝ _, + refine !eq_of_pathover_apo ⬝ _, exact sorry }} +end + + local attribute equiv_of_omega_compact [constructor] + + definition omega_compact_sum [instance] [constructor] {X Y : Type} [omega_compact.{_ u} X] + [omega_compact.{u u} Y] : omega_compact.{_ u} (X ⊎ Y) := + begin + fapply omega_compact_of_equiv, + { intro A f, + exact calc + seq_colim (seq_diagram_arrow_left f (X ⊎ Y)) + ≃ seq_colim (seq_diagram_prod (seq_diagram_arrow_left f X) (seq_diagram_arrow_left f Y)) : + by exact seq_colim_equiv (λn, !imp_prod_imp_equiv_sum_imp⁻¹ᵉ) (λn f, idp) + ... ≃ seq_colim (seq_diagram_arrow_left f X) × seq_colim (seq_diagram_arrow_left f Y) : + by apply seq_colim_prod + ... ≃ (X → seq_colim f) × (Y → seq_colim f) : + by exact prod_equiv_prod (equiv_of_omega_compact X f) (equiv_of_omega_compact Y f) + ... ≃ ((X ⊎ Y) → seq_colim f) : + by exact !imp_prod_imp_equiv_sum_imp }, + { intros, induction x with x y: reflexivity }, + { intros, induction x with x y: apply hdeg_square, + { refine ap_compose (((λz, arrow_colim_of_colim_arrow f z _) ∘ pr1) ∘ + seq_colim_prod _ _) _ _ ⬝ _, refine ap02 _ (!elim_glue ⬝ !idp_con) ⬝ _, + refine !ap_compose ⬝ _, refine ap02 _ !elim_glue ⬝ _, + refine !ap_compose ⬝ _, refine ap02 _ !prod_eq_pr1 ⬝ !elim_glue }, + { refine ap_compose (((λz, arrow_colim_of_colim_arrow f z _) ∘ pr2) ∘ + seq_colim_prod _ _) _ _ ⬝ _, refine ap02 _ (!elim_glue ⬝ !idp_con) ⬝ _, + refine !ap_compose ⬝ _, refine ap02 _ !elim_glue ⬝ _, + refine !ap_compose ⬝ _, refine ap02 _ !prod_eq_pr2 ⬝ !elim_glue }}, + end + +open wedge pointed circle + +/- needs fwedge! -/ +definition seq_diagram_fwedge (X : Type*) : seq_diagram (λn, @fwedge (A n) (λa, X)) := +sorry f + +definition seq_colim_fwedge_equiv (X : Type*) [is_trunc 1 X] : + seq_colim (seq_diagram_fwedge f X) ≃ @fwedge (seq_colim f) (λn, X) := +sorry + +definition not_omega_compact_fwedge_nat_circle : ¬(omega_compact.{0 0} (@fwedge ℕ (λn, S¹*))) := +assume H, +sorry diff --git a/colimit/pointed.hlean b/colimit/pointed.hlean new file mode 100644 index 0000000..76fbe32 --- /dev/null +++ b/colimit/pointed.hlean @@ -0,0 +1,257 @@ +/- pointed sequential colimits -/ + +-- authors: Floris van Doorn, Egbert Rijke, Stefano Piceghello + +import .seq_colim types.fin homotopy.chain_complex types.pointed2 +open seq_colim pointed algebra eq is_trunc nat is_equiv equiv sigma sigma.ops chain_complex fiber + +namespace seq_colim + + definition pseq_diagram [reducible] (A : ℕ → Type*) : Type := Πn, A n →* A (succ n) + definition pseq_colim [constructor] {X : ℕ → Type*} (f : pseq_diagram X) : Type* := + pointed.MK (seq_colim f) (@sι _ _ 0 pt) + + definition inclusion_pt {X : ℕ → Type*} (f : pseq_diagram X) (n : ℕ) + : inclusion f (Point (X n)) = Point (pseq_colim f) := + begin + induction n with n p, + reflexivity, + exact (ap (sι f) (respect_pt _))⁻¹ᵖ ⬝ (!glue ⬝ p) + end + + definition pinclusion [constructor] {X : ℕ → Type*} (f : pseq_diagram X) (n : ℕ) + : X n →* pseq_colim f := + pmap.mk (inclusion f) (inclusion_pt f n) + + definition pshift_equiv [constructor] {A : ℕ → Type*} (f : Πn, A n →* A (succ n)) : + pseq_colim f ≃* pseq_colim (λn, f (n+1)) := + begin + fapply pequiv_of_equiv, + { apply shift_equiv }, + { exact ap (ι _) (respect_pt (f 0)) } + end + + definition pshift_equiv_pinclusion {A : ℕ → Type*} (f : Πn, A n →* A (succ n)) (n : ℕ) : + psquare (pinclusion f n) (pinclusion (λn, f (n+1)) n) (f n) (pshift_equiv f) := + phomotopy.mk homotopy.rfl begin + refine !idp_con ⬝ _, esimp, + induction n with n IH, + { esimp[inclusion_pt], esimp[shift_diag], exact !idp_con⁻¹ }, + { esimp[inclusion_pt], refine !con_inv_cancel_left ⬝ _, + rewrite ap_con, rewrite ap_con, + refine _ ⬝ whisker_right _ !con.assoc, + refine _ ⬝ (con.assoc (_ ⬝ _) _ _)⁻¹, + xrewrite [-IH], + esimp[shift_up], rewrite [elim_glue, ap_inv, -ap_compose'], esimp, + rewrite [-+con.assoc], apply whisker_right, + rewrite con.assoc, apply !eq_inv_con_of_con_eq, + symmetry, exact eq_of_square !natural_square + } + end + + definition pseq_colim_functor [constructor] {A A' : ℕ → Type*} {f : pseq_diagram A} + {f' : pseq_diagram A'} (g : Πn, A n →* A' n) + (p : Π⦃n⦄, g (n+1) ∘* f n ~ f' n ∘* g n) : pseq_colim f →* pseq_colim f' := + pmap.mk (seq_colim_functor g p) (ap (ι _) (respect_pt (g _))) + + definition pseq_colim_pequiv' [constructor] {A A' : ℕ → Type*} {f : pseq_diagram A} + {f' : pseq_diagram A'} (g : Πn, A n ≃* A' n) + (p : Π⦃n⦄, g (n+1) ∘* f n ~ f' n ∘* g n) : pseq_colim @f ≃* pseq_colim @f' := + pequiv_of_equiv (seq_colim_equiv g p) (ap (ι _) (respect_pt (g _))) + + definition pseq_colim_pequiv [constructor] {A A' : ℕ → Type*} {f : pseq_diagram A} + {f' : pseq_diagram A'} (g : Πn, A n ≃* A' n) + (p : Πn, g (n+1) ∘* f n ~* f' n ∘* g n) : pseq_colim @f ≃* pseq_colim @f' := + pseq_colim_pequiv' g (λn, @p n) + + -- definition seq_colim_equiv_constant [constructor] {A : ℕ → Type*} {f f' : pseq_diagram A} + -- (p : Π⦃n⦄ (a : A n), f n a = f' n a) : seq_colim f ≃ seq_colim f' := + -- seq_colim_equiv (λn, erfl) p + + definition pseq_colim_equiv_constant' [constructor] {A : ℕ → Type*} {f f' : pseq_diagram A} + (p : Π⦃n⦄, f n ~ f' n) : pseq_colim @f ≃* pseq_colim @f' := + pseq_colim_pequiv' (λn, pequiv.rfl) p + + definition pseq_colim_equiv_constant [constructor] {A : ℕ → Type*} {f f' : pseq_diagram A} + (p : Πn, f n ~* f' n) : pseq_colim @f ≃* pseq_colim @f' := + pseq_colim_pequiv (λn, pequiv.rfl) (λn, !pid_pcompose ⬝* p n ⬝* !pcompose_pid⁻¹*) + + definition pseq_colim_pequiv_pinclusion {A A' : ℕ → Type*} {f : Πn, A n →* A (n+1)} + {f' : Πn, A' n →* A' (n+1)} (g : Πn, A n ≃* A' n) + (p : Π⦃n⦄, g (n+1) ∘* f n ~* f' n ∘* g n) (n : ℕ) : + psquare (pinclusion f n) (pinclusion f' n) (g n) (pseq_colim_pequiv g p) := + phomotopy.mk homotopy.rfl begin + esimp, refine !idp_con ⬝ _, + induction n with n IH, + { esimp[inclusion_pt], exact !idp_con⁻¹ }, + { esimp[inclusion_pt], rewrite [+ap_con, -+ap_inv, +con.assoc, +seq_colim_functor_glue], + xrewrite[-IH], + rewrite[-+ap_compose', -+con.assoc], + apply whisker_right, esimp, + rewrite[(eq_con_inv_of_con_eq (to_homotopy_pt (@p _)))], + rewrite[ap_con], esimp, + rewrite[-+con.assoc, ap_con, -ap_compose', +ap_inv], + rewrite[-+con.assoc], + refine _ ⬝ whisker_right _ (whisker_right _ (whisker_right _ (whisker_right _ !con.left_inv⁻¹))), + rewrite[idp_con, +con.assoc], apply whisker_left, + rewrite[ap_con, -ap_compose', con_inv, +con.assoc], apply whisker_left, + refine eq_inv_con_of_con_eq _, + symmetry, exact eq_of_square !natural_square + } + end + + definition seq_colim_equiv_constant_pinclusion {A : ℕ → Type*} {f f' : pseq_diagram A} + (p : Πn, f n ~* f' n) (n : ℕ) : + pseq_colim_equiv_constant p ∘* pinclusion f n ~* pinclusion f' n := + begin + transitivity pinclusion f' n ∘* !pid, + refine phomotopy_of_psquare !pseq_colim_pequiv_pinclusion, + exact !pcompose_pid + end + + definition pseq_colim.elim' [constructor] {A : ℕ → Type*} {B : Type*} {f : pseq_diagram A} + (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f n ~ g n) : pseq_colim f →* B := + begin + fapply pmap.mk, + { intro x, induction x with n a n a, + { exact g n a }, + { exact p n a }}, + { esimp, apply respect_pt } + end + + definition pseq_colim.elim [constructor] {A : ℕ → Type*} {B : Type*} {f : pseq_diagram A} + (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f n ~* g n) : pseq_colim @f →* B := + pseq_colim.elim' g p + + definition pseq_colim.elim_pinclusion {A : ℕ → Type*} {B : Type*} {f : pseq_diagram A} + (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f n ~* g n) (n : ℕ) : + pseq_colim.elim g p ∘* pinclusion f n ~* g n := + begin + refine phomotopy.mk phomotopy.rfl _, + refine !idp_con ⬝ _, + esimp, + induction n with n IH, + { esimp, esimp[inclusion_pt], exact !idp_con⁻¹ }, + { esimp, esimp[inclusion_pt], + rewrite ap_con, rewrite ap_con, + rewrite elim_glue, + rewrite [-ap_inv], + rewrite [-ap_compose'], esimp, + rewrite [(eq_con_inv_of_con_eq (!to_homotopy_pt))], + rewrite [IH], + rewrite [con_inv], + rewrite [-+con.assoc], + refine _ ⬝ whisker_right _ !con.assoc⁻¹, + rewrite [con.left_inv], esimp, + refine _ ⬝ !con.assoc⁻¹, + rewrite [con.left_inv], esimp, + rewrite [ap_inv], + rewrite [-con.assoc], + refine !idp_con⁻¹ ⬝ whisker_right _ !con.left_inv⁻¹, + } + end + + definition prep0 [constructor] {A : ℕ → Type*} (f : pseq_diagram A) (k : ℕ) : A 0 →* A k := + pmap.mk (rep0 (λn x, f n x) k) + begin induction k with k p, reflexivity, exact ap (@f k) p ⬝ !respect_pt end + + definition respect_pt_prep0_succ {A : ℕ → Type*} (f : pseq_diagram A) (k : ℕ) + : respect_pt (prep0 f (succ k)) = ap (@f k) (respect_pt (prep0 f k)) ⬝ respect_pt (f k) := + by reflexivity + + 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_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 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 + + 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)) := + begin + fapply pequiv_of_equiv, + { refine !seq_colim_eq_equiv0 ⬝e _, + fapply seq_colim_equiv, + { intro n, exact loop_equiv_eq_closed (respect_pt (prep0 f n)) }, + { intro n p, apply prep0_succ_lemma }}, + { reflexivity } + end + + definition pseq_colim_loop_pinclusion {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) (n : ℕ) : + pseq_colim_loop f ∘* Ω→ (pinclusion f n) ~* pinclusion (λn, Ω→(f n)) 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)) := + λk, pfiber_functor (f k) (f' k) (p k) + +/- Two issues when going to the pointed version: + - seq_diagram_fiber τ p a for a : A n at position k lives over (A (n + k)), so for a : A 0 you get A (0 + k), but we need A k + - in seq_diagram_fiber the fibers are taken in rep f ..., but in the pointed version over the basepoint of A n +-/ +definition pfiber_pseq_colim_functor {A A' : ℕ → Type*} {f : pseq_diagram A} + {f' : pseq_diagram A'} (τ : Πn, A n →* A' n) + (p : Π⦃n⦄, τ (n+1) ∘* f n ~* f' n ∘* τ n) : pfiber (pseq_colim_functor τ p) ≃* + pseq_colim (pseq_diagram_pfiber τ p) := +begin + fapply pequiv_of_equiv, + { refine fiber_seq_colim_functor0 τ p pt ⬝e _, fapply seq_colim_equiv, intro n, esimp, + repeat exact sorry }, exact sorry +end + + + -- open succ_str + -- definition pseq_colim_succ_str_change_index' {N : succ_str} {B : N → Type*} (n : N) (m : ℕ) + -- (h : Πn, B n →* B (S n)) : + -- pseq_colim (λk, h (n +' (m + succ k))) ≃* pseq_colim (λk, h (S n +' (m + k))) := + -- sorry + + -- definition pseq_colim_succ_str_change_index {N : succ_str} {B : ℕ → N → Type*} (n : N) + -- (h : Π(k : ℕ) n, B k n →* B k (S n)) : + -- pseq_colim (λk, h k (n +' succ k)) ≃* pseq_colim (λk, h k (S n +' k)) := + -- sorry + + -- definition pseq_colim_index_eq_general {N : succ_str} (B : N → Type*) (f g : ℕ → N) (p : f ~ g) + -- (pf : Πn, S (f n) = f (n+1)) (pg : Πn, S (g n) = g (n+1)) (h : Πn, B n →* B (S n)) : + -- @pseq_colim (λn, B (f n)) (λn, ptransport B (pf n) ∘* h (f n)) ≃* + -- @pseq_colim (λn, B (g n)) (λn, ptransport B (pg n) ∘* h (g n)) := + -- sorry + + +end seq_colim diff --git a/colimit/pushout.hlean b/colimit/pushout.hlean new file mode 100644 index 0000000..2c390ce --- /dev/null +++ b/colimit/pushout.hlean @@ -0,0 +1,216 @@ +/- + Suppose we have three sequences A = (Aₙ, fₙ)ₙ, B = (Bₙ, gₙ)ₙ, C = (Cₙ, hₙ)ₙ with natural + transformations like this: B ← A → C. We can take pushouts pointwise and then take the colimit, + or we can take the colimit of each and then pushout. By the 3x3 lemma these are equivalent. + + Authors: Floris van Doorn +-/ + +import .seq_colim ..homotopy.pushout ..homotopy.three_by_three +open eq nat seq_colim is_trunc equiv is_equiv trunc sigma sum pi function algebra sigma.ops + +section +variables {A B : ℕ → Type} {f : seq_diagram A} {g : seq_diagram B} (i : Π⦃n⦄, A n → B n) + (p : Π⦃n⦄ (a : A n), i (f a) = g (i a)) (a a' : Σn, A n) + + +definition total_seq_rel [constructor] (f : seq_diagram A) : + (Σ(a a' : Σn, A n), seq_rel f a a') ≃ Σn, A n := +begin + fapply equiv.MK, + { intro x, exact x.2.1 }, + { intro x, induction x with n a, exact ⟨⟨n+1, f a⟩, ⟨n, a⟩, seq_rel.Rmk f a⟩ }, + { intro x, induction x with n a, reflexivity }, + { intro x, induction x with a x, induction x with a' r, induction r with n a, reflexivity } +end + +definition pr1_total_seq_rel_inv (x : Σn, A n) : + ((total_seq_rel f)⁻¹ᵉ x).1 = sigma_functor succ f x := +begin induction x with n a, reflexivity end + +definition pr2_total_seq_rel_inv (x : Σn, A n) : ((total_seq_rel f)⁻¹ᵉ x).2.1 = x := +to_right_inv (total_seq_rel f) x + +include p +definition seq_rel_functor [unfold 9] : seq_rel f a a' → seq_rel g (total i a) (total i a') := +begin + intro r, induction r with n a, + exact transport (λx, seq_rel g ⟨_, x⟩ _) (p a)⁻¹ (seq_rel.Rmk g (i a)) +end + +open pushout + +definition total_seq_rel_natural [unfold 7] : + hsquare (sigma_functor2 (total i) (seq_rel_functor i p)) (total i) + (total_seq_rel f) (total_seq_rel g) := +homotopy.rfl + +end + + +section +open pushout sigma.ops quotient + +parameters {A B C : ℕ → Type} {f : seq_diagram A} {g : seq_diagram B} {h : seq_diagram C} + (i : Π⦃n⦄, A n → B n) (j : Π⦃n⦄, A n → C n) + (p : Π⦃n⦄ (a : A n), i (f a) = g (i a)) (q : Π⦃n⦄ (a : A n), j (f a) = h (j a)) + + +definition seq_diagram_pushout : seq_diagram (λn, pushout (@i n) (@j n)) := +λn, pushout.functor (@f n) (@g n) (@h n) (@p n)⁻¹ʰᵗʸ (@q n)⁻¹ʰᵗʸ + +local abbreviation sA := Σn, A n +local abbreviation sB := Σn, B n +local abbreviation sC := Σn, C n +local abbreviation si : sA → sB := total i +local abbreviation sj : sA → sC := total j +local abbreviation rA := Σ(x y : sA), seq_rel f x y +local abbreviation rB := Σ(x y : sB), seq_rel g x y +local abbreviation rC := Σ(x y : sC), seq_rel h x y +set_option pp.abbreviations false +local abbreviation ri : rA → rB := sigma_functor2 (total i) (seq_rel_functor i p) +local abbreviation rj : rA → rC := sigma_functor2 (total j) (seq_rel_functor j q) + +definition pushout_seq_colim_span [constructor] : three_by_three_span := +@three_by_three_span.mk + sB (rB ⊎ rB) rB sA (rA ⊎ rA) rA sC (rC ⊎ rC) rC + (sum.rec pr1 (λx, x.2.1)) (sum.rec id id) + (sum.rec pr1 (λx, x.2.1)) (sum.rec id id) + (sum.rec pr1 (λx, x.2.1)) (sum.rec id id) + (total i) (total j) (ri +→ ri) (rj +→ rj) ri rj + begin intro x, induction x: reflexivity end + begin intro x, induction x: reflexivity end + begin intro x, induction x: reflexivity end + begin intro x, induction x: reflexivity end + +definition ua_equiv_ap {A : Type} (P : A → Type) {a b : A} (p : a = b) : + ua (equiv_ap P p) = ap P p := +begin induction p, apply ua_refl end + +definition pushout_elim_type_eta {TL BL TR : Type} {f : TL → BL} {g : TL → TR} + (P : pushout f g → Type) (x : pushout f g) : + P x ≃ pushout.elim_type (P ∘ inl) (P ∘ inr) (λa, equiv_ap P (glue a)) x := +begin + induction x, + { reflexivity }, + { reflexivity }, + { apply equiv_pathover_inv, apply arrow_pathover_left, intro y, + apply pathover_of_tr_eq, symmetry, exact ap10 !elim_type_glue y } +end + +definition pushout_flattening' {TL BL TR : Type} {f : TL → BL} {g : TL → TR} + (P : pushout f g → Type) : sigma P ≃ + @pushout (sigma (P ∘ inl ∘ f)) (sigma (P ∘ inl)) (sigma (P ∘ inr)) + (sigma_functor f (λa, id)) (sigma_functor g (λa, transport P (glue a))) := +sigma_equiv_sigma_right (pushout_elim_type_eta P) ⬝e +pushout.flattening _ _ (P ∘ inl) (P ∘ inr) (λa, equiv_ap P (glue a)) + +definition equiv_ap011 {A B : Type} (P : A → B → Type) {a a' : A} {b b' : B} + (p : a = a') (q : b = b') : P a b ≃ P a' b' := +equiv_ap (P a) q ⬝e equiv_ap (λa, P a b') p + +definition tr_tr_eq_tr_tr [unfold 8 9] {A B : Type} (P : A → B → Type) {a a' : A} {b b' : B} + (p : a = a') (q : b = b') (x : P a b) : + transport (P a') q (transport (λa, P a b) p x) = transport (λa, P a b') p (transport (P a) q x) := +by induction p; induction q; reflexivity + +definition pushout_total_seq_rel : + pushout (sigma_functor2 (total i) (seq_rel_functor i p)) + (sigma_functor2 (total j) (seq_rel_functor j q)) ≃ + Σ(x : Σ ⦃n : ℕ⦄, pushout (@i n) (@j n)), sigma (seq_rel seq_diagram_pushout x) := +pushout.equiv _ _ _ _ (total_seq_rel f) (total_seq_rel g) (total_seq_rel h) + homotopy.rfl homotopy.rfl ⬝e +pushout_sigma_equiv_sigma_pushout i j ⬝e +(total_seq_rel seq_diagram_pushout)⁻¹ᵉ + +definition pr1_pushout_total_seq_rel : + hsquare pushout_total_seq_rel (pushout_sigma_equiv_sigma_pushout i j) + (pushout.functor pr1 pr1 pr1 homotopy.rfl homotopy.rfl) pr1 := +begin + intro x, refine !pr1_total_seq_rel_inv ⬝ _, esimp, + refine !pushout_sigma_equiv_sigma_pushout_natural⁻¹ ⬝ _, + apply ap sigma_pushout_of_pushout_sigma, + refine !pushout_functor_compose⁻¹ ⬝ _, + fapply pushout_functor_homotopy, + { intro v, induction v with a v, induction v with a' r, induction r, reflexivity }, + { intro v, induction v with a v, induction v with a' r, induction r, reflexivity }, + { intro v, induction v with a v, induction v with a' r, induction r, reflexivity }, + { intro v, induction v with a v, induction v with a' r, induction r, esimp, generalize p a, + generalize i (f a), intro x r, cases r, reflexivity }, + { intro v, induction v with a v, induction v with a' r, induction r, esimp, generalize q a, + generalize j (f a), intro x r, cases r, reflexivity }, +end + +definition pr2_pushout_total_seq_rel : + hsquare pushout_total_seq_rel (pushout_sigma_equiv_sigma_pushout i j) + (pushout.functor (λx, x.2.1) (λx, x.2.1) (λx, x.2.1) homotopy.rfl homotopy.rfl) + (λx, x.2.1) := +begin + intro x, apply pr2_total_seq_rel_inv, +end + +/- this result depends on the 3x3 lemma, which is currently not formalized in Lean -/ +definition pushout_seq_colim_equiv [constructor] : + pushout (seq_colim_functor i p) (seq_colim_functor j q) ≃ seq_colim seq_diagram_pushout := +have e1 : + pushout (seq_colim_functor i p) (seq_colim_functor j q) ≃ pushout2hv pushout_seq_colim_span, from +pushout.equiv _ _ _ _ !quotient_equiv_pushout !quotient_equiv_pushout !quotient_equiv_pushout + begin + refine _ ⬝hty quotient_equiv_pushout_natural (total i) (seq_rel_functor i p), + intro x, apply ap pushout_quotient_of_quotient, + induction x, + { induction a with n a, reflexivity }, + { induction H, apply eq_pathover, apply hdeg_square, + refine !elim_glue ⬝ _ ⬝ !elim_eq_of_rel⁻¹, + unfold [seq_colim.glue, seq_rel_functor], + symmetry, + refine fn_tr_eq_tr_fn (p a)⁻¹ _ _ ⬝ eq_transport_Fl (p a)⁻¹ _ ⬝ _, + apply whisker_right, exact !ap_inv⁻² ⬝ !inv_inv } + end + begin + refine _ ⬝hty quotient_equiv_pushout_natural (total j) (seq_rel_functor j q), + intro x, apply ap pushout_quotient_of_quotient, + induction x, + { induction a with n a, reflexivity }, + { induction H, apply eq_pathover, apply hdeg_square, + refine !elim_glue ⬝ _ ⬝ !elim_eq_of_rel⁻¹, + unfold [seq_colim.glue, seq_rel_functor], + symmetry, + refine fn_tr_eq_tr_fn (q a)⁻¹ _ _ ⬝ eq_transport_Fl (q a)⁻¹ _ ⬝ _, + apply whisker_right, exact !ap_inv⁻² ⬝ !inv_inv } + end, +have e2 : pushout2vh pushout_seq_colim_span ≃ pushout_quotient (seq_rel seq_diagram_pushout), from +pushout.equiv _ _ _ _ + (!pushout_sum_equiv_sum_pushout ⬝e sum_equiv_sum pushout_total_seq_rel pushout_total_seq_rel) + (pushout_sigma_equiv_sigma_pushout i j) + pushout_total_seq_rel + begin + intro x, symmetry, + refine sum_rec_hsquare pr1_pushout_total_seq_rel pr2_pushout_total_seq_rel + (!pushout_sum_equiv_sum_pushout x) ⬝ ap (pushout_sigma_equiv_sigma_pushout i j) _, + refine sum_rec_pushout_sum_equiv_sum_pushout _ _ _ _ x ⬝ _, + apply pushout_functor_homotopy_constant: intro x; induction x: reflexivity + end + begin + intro x, symmetry, + refine !sum_rec_sum_functor ⬝ _, + refine sum_rec_same_compose + ((total_seq_rel seq_diagram_pushout)⁻¹ᵉ ∘ pushout_sigma_equiv_sigma_pushout i j) _ _ ⬝ _, + apply ap (to_fun (total_seq_rel seq_diagram_pushout)⁻¹ᵉ ∘ to_fun + (pushout_sigma_equiv_sigma_pushout i j)), + refine !sum_rec_pushout_sum_equiv_sum_pushout ⬝ _, + refine _ ⬝ !pushout_functor_compose, + fapply pushout_functor_homotopy, + { intro x, induction x: reflexivity }, + { intro x, induction x: reflexivity }, + { intro x, induction x: reflexivity }, + { intro x, induction x: exact (!idp_con ⬝ !ap_id ⬝ !inv_inv)⁻¹ }, + { intro x, induction x: exact (!idp_con ⬝ !ap_id ⬝ !inv_inv)⁻¹ } + end, +e1 ⬝e three_by_three pushout_seq_colim_span ⬝e e2 ⬝e (quotient_equiv_pushout _)⁻¹ᵉ + +definition seq_colim_pushout_equiv [constructor] : seq_colim seq_diagram_pushout ≃ + pushout (seq_colim_functor i p) (seq_colim_functor j q) := +pushout_seq_colim_equiv⁻¹ᵉ + +end diff --git a/colimit/seq_colim.hlean b/colimit/seq_colim.hlean new file mode 100644 index 0000000..22e4700 --- /dev/null +++ b/colimit/seq_colim.hlean @@ -0,0 +1,900 @@ +/- +Copyright (c) 2015 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Floris van Doorn, Egbert Rijke +-/ +import hit.colimit .sequence cubical.squareover types.arrow types.equiv + cubical.pathover2 + +open eq nat sigma sigma.ops quotient equiv pi is_trunc is_equiv fiber function trunc + +namespace seq_colim + +-- note: this clashes with the abbreviation defined in namespace "colimit" +abbreviation ι [constructor] := @inclusion +abbreviation ι' [constructor] [parsing_only] {A} (f n) := @inclusion A f n + +variables {A A' A'' : ℕ → Type} (f : seq_diagram A) (f' : seq_diagram A') (f'' : seq_diagram A'') + +definition lrep_glue {n m : ℕ} (H : n ≤ m) (a : A n) : ι f (lrep f H a) = ι f a := +begin + induction H with m H p, + { reflexivity }, + { exact glue f (lrep f H a) ⬝ p } +end + +-- probably not needed +-- definition rep0_back_glue [is_equiseq f] (k : ℕ) (a : A k) : ι f (rep0_back f k a) = ι f a := +-- begin +-- exact sorry +-- end + +definition colim_back [unfold 4] [H : is_equiseq f] : seq_colim f → A 0 := +begin + intro x, + induction x with k a k a, + { exact lrep_back f (zero_le k) a}, + rexact ap (lrep_back f (zero_le k)) (left_inv (@f k) a), +end + +set_option pp.binder_types true + +section +local attribute is_equiv_lrep [instance] --[priority 500] +definition is_equiv_ι (H : is_equiseq f) : is_equiv (ι' f 0) := +begin + fapply adjointify, + { exact colim_back f}, + { intro x, induction x with k a k a, + { esimp, + refine (lrep_glue f (zero_le k) (lrep_back f (zero_le k) a))⁻¹ ⬝ _, + exact ap (ι f) (right_inv (lrep f (zero_le k)) a)}, + apply eq_pathover_id_right, + refine (ap_compose (ι f) (colim_back f) _) ⬝ph _, + refine ap02 _ _ ⬝ph _, rotate 1, + { rexact elim_glue f _ _ a}, + refine _ ⬝pv ((natural_square (lrep_glue f (zero_le k)) + (ap (lrep_back f (zero_le k)) (left_inv (@f k) a)))⁻¹ʰ ⬝h _), + { exact (glue f (lrep f (zero_le k) (lrep_back f (zero_le (succ k)) (f a))))⁻¹ ⬝ + ap (ι f) (right_inv (lrep f (zero_le (succ k))) (f a))}, + { rewrite [-con.assoc, -con_inv]}, + refine !ap_compose⁻¹ ⬝ ap_compose (ι f) _ _ ⬝ph _, + refine dconcat (aps (ι' f k) (natural_square (right_inv (lrep f (zero_le k))) + (left_inv (@f _) a))) _, + apply move_top_of_left, apply move_left_of_bot, + refine ap02 _ (whisker_left _ (adj (@f _) a)) ⬝pv _, + rewrite [-+ap_con, -ap_compose', ap_id], + apply natural_square_tr}, + intro a, + reflexivity, +end +end + +section +variables {n : ℕ} (a : A n) + +definition rep_glue (k : ℕ) (a : A n) : ι f (rep f k a) = ι f a := +begin + induction k with k IH, + { reflexivity}, + { exact glue f (rep f k a) ⬝ IH} +end + +/- functorial action and equivalences -/ +section functor +variables {f f' f''} +variables (τ τ₂ : Π⦃n⦄, A n → A' n) (p : Π⦃n⦄ (a : A n), τ (f a) = f' (τ a)) + (p₂ : Π⦃n⦄ (a : A n), τ₂ (f a) = f' (τ₂ a)) + (τ' : Π⦃n⦄, A' n → A'' n) (p' : Π⦃n⦄ (a' : A' n), τ' (f' a') = f'' (τ' a')) +include p +definition seq_colim_functor [unfold 7] : seq_colim f → seq_colim f' := +begin + intro x, induction x with n a n a, + { exact ι f' (τ a)}, + { exact ap (ι f') (p a) ⬝ glue f' (τ a)} +end +omit p + +theorem seq_colim_functor_glue {n : ℕ} (a : A n) + : ap (seq_colim_functor τ p) (glue f a) = ap (ι f') (p a) ⬝ glue f' (τ a) := +!elim_glue + +definition seq_colim_functor_compose [constructor] (x : seq_colim f) : + seq_colim_functor (λn x, τ' (τ x)) (λn, hvconcat (@p n) (@p' n)) x = + seq_colim_functor τ' p' (seq_colim_functor τ p x) := +begin + induction x, reflexivity, + apply eq_pathover, apply hdeg_square, + refine !seq_colim_functor_glue ⬝ _ ⬝ (ap_compose (seq_colim_functor _ _) _ _)⁻¹, + refine _ ⬝ (ap02 _ proof !seq_colim_functor_glue qed ⬝ !ap_con)⁻¹, + refine _ ⬝ (proof !ap_compose'⁻¹ ⬝ ap_compose (ι f'') _ _ qed ◾ proof !seq_colim_functor_glue qed)⁻¹, + exact whisker_right _ !ap_con ⬝ !con.assoc +end + +variable (f) +definition seq_colim_functor_id [constructor] (x : seq_colim f) : + seq_colim_functor (λn, id) (λn, homotopy.rfl) x = + x := +begin + induction x, reflexivity, + apply eq_pathover, apply hdeg_square, + exact !seq_colim_functor_glue ⬝ !idp_con ⬝ !ap_id⁻¹, +end +variables {f τ τ₂ p p₂} + +definition seq_colim_functor_homotopy [constructor] (q : τ ~2 τ₂) + (r : Π⦃n⦄ (a : A n), square (q (n+1) (f a)) (ap (@f' n) (q n a)) (p a) (p₂ a)) + (x : seq_colim f) : + seq_colim_functor τ p x = seq_colim_functor τ₂ p₂ x := +begin + induction x, + exact ap (ι f') (q n a), + apply eq_pathover, + refine !seq_colim_functor_glue ⬝ph _ ⬝hp !seq_colim_functor_glue⁻¹, + refine aps (ι f') (r a) ⬝v !ap_compose⁻¹ ⬝pv natural_square_tr (glue f') (q n a), +end +variables (τ τ₂ p p₂) + +definition is_equiv_seq_colim_functor [constructor] [H : Πn, is_equiv (@τ n)] + : is_equiv (seq_colim_functor @τ p) := +adjointify _ (seq_colim_functor (λn, (@τ _)⁻¹) (λn a, inv_commute' τ f f' p a)) + abstract begin + intro x, + refine !seq_colim_functor_compose⁻¹ ⬝ seq_colim_functor_homotopy _ _ x ⬝ !seq_colim_functor_id, + { intro n a, exact right_inv (@τ n) a }, + { intro n a, + refine whisker_right _ !ap_inv_commute' ⬝ !inv_con_cancel_right ⬝ whisker_left _ !ap_inv ⬝ph _, + apply whisker_bl, apply whisker_tl, exact ids } + end end + abstract begin + intro x, + refine !seq_colim_functor_compose⁻¹ ⬝ seq_colim_functor_homotopy _ _ x ⬝ !seq_colim_functor_id, + { intro n a, exact left_inv (@τ n) a }, + { intro n a, + esimp [hvconcat], + refine whisker_left _ (!inv_commute'_fn ⬝ !con.assoc) ⬝ !con_inv_cancel_left ⬝ph _, + apply whisker_bl, apply whisker_tl, exact ids } + end end + +definition seq_colim_equiv [constructor] (τ : Π{n}, A n ≃ A' n) + (p : Π⦃n⦄ (a : A n), τ (f a) = f' (τ a)) : seq_colim f ≃ seq_colim f' := +equiv.mk _ (is_equiv_seq_colim_functor @τ p) + +definition seq_colim_rec_unc [unfold 4] {P : seq_colim f → Type} + (v : Σ(Pincl : Π ⦃n : ℕ⦄ (a : A n), P (ι f a)), + Π ⦃n : ℕ⦄ (a : A n), Pincl (f a) =[glue f a] Pincl a) + : Π(x : seq_colim f), P x := +by induction v with Pincl Pglue; exact seq_colim.rec f Pincl Pglue + +definition is_equiv_seq_colim_rec (P : seq_colim f → Type) : + is_equiv (seq_colim_rec_unc : + (Σ(Pincl : Π ⦃n : ℕ⦄ (a : A n), P (ι f a)), + Π ⦃n : ℕ⦄ (a : A n), Pincl (f a) =[glue f a] Pincl a) + → (Π (aa : seq_colim f), P aa)) := +begin + fapply adjointify, + { intro s, exact ⟨λn a, s (ι f a), λn a, apd s (glue f a)⟩}, + { intro s, apply eq_of_homotopy, intro x, induction x, + { reflexivity}, + { apply eq_pathover_dep, esimp, apply hdeg_squareover, apply rec_glue}}, + { intro v, induction v with Pincl Pglue, fapply ap (sigma.mk _), + apply eq_of_homotopy2, intros n a, apply rec_glue}, +end + +/- universal property -/ +definition equiv_seq_colim_rec (P : seq_colim f → Type) : + (Σ(Pincl : Π ⦃n : ℕ⦄ (a : A n), P (ι f a)), + Π ⦃n : ℕ⦄ (a : A n), Pincl (f a) =[glue f a] Pincl a) ≃ (Π (aa : seq_colim f), P aa) := +equiv.mk _ !is_equiv_seq_colim_rec + +end functor + +definition shift_up [unfold 3] (x : seq_colim f) : seq_colim (shift_diag f) := +begin + induction x, + { exact ι' (shift_diag f) n (f a)}, + { exact glue (shift_diag f) (f a)} +end + +definition shift_down [unfold 3] (x : seq_colim (shift_diag f)) : seq_colim f := +begin + induction x, + { exact ι' f (n+1) a}, + { exact glue f a} +end + +-- definition kshift_up' (k : ℕ) (x : seq_colim f) : seq_colim (kshift_diag' f k) := +-- begin +-- induction x, +-- { apply ι' _ n, exact rep f k a}, +-- { exact sorry} +-- end + +-- definition kshift_down' (k : ℕ) (x : seq_colim (kshift_diag' f k)) : seq_colim f := +-- begin +-- induction x, +-- { exact ι f a}, +-- { esimp, exact sorry} +-- end + +end + +definition shift_equiv [constructor] : seq_colim f ≃ seq_colim (shift_diag f) := +equiv.MK (shift_up f) + (shift_down f) + abstract begin + intro x, induction x, + { exact glue _ a }, + { apply eq_pathover, + rewrite [▸*, ap_id, ap_compose (shift_up f) (shift_down f), ↑shift_down, + elim_glue], + apply square_of_eq, apply whisker_right, exact !elim_glue⁻¹ } + end end + abstract begin + intro x, induction x, + { exact glue _ a }, + { apply eq_pathover, + rewrite [▸*, ap_id, ap_compose (shift_down f) (shift_up f), ↑shift_up, + elim_glue], + apply square_of_eq, apply whisker_right, exact !elim_glue⁻¹ } + end end + +-- definition kshift_equiv [constructor] (k : ℕ) +-- : seq_colim A ≃ @seq_colim (λn, A (k + n)) (kshift_diag A k) := +-- equiv.MK (kshift_up k) +-- (kshift_down k) +-- abstract begin +-- intro a, exact sorry, +-- -- induction a, +-- -- { esimp, exact glue a}, +-- -- { apply eq_pathover, +-- -- rewrite [▸*, ap_id, ap_compose shift_up shift_down, ↑shift_down, +-- -- @elim_glue (λk, A (succ k)) _, ↑shift_up], +-- -- apply square_of_eq, apply whisker_right, exact !elim_glue⁻¹} +-- end end +-- abstract begin +-- intro a, exact sorry +-- -- induction a, +-- -- { exact glue a}, +-- -- { apply eq_pathover, +-- -- rewrite [▸*, ap_id, ap_compose shift_down shift_up, ↑shift_up, +-- -- @elim_glue A _, ↑shift_down], +-- -- apply square_of_eq, apply whisker_right, exact !elim_glue⁻¹} +-- end end + +-- definition kshift_equiv' [constructor] (k : ℕ) : seq_colim f ≃ seq_colim (kshift_diag' f k) := +-- equiv.MK (kshift_up' f k) +-- (kshift_down' f k) +-- abstract begin +-- intro a, exact sorry, +-- -- induction a, +-- -- { esimp, exact glue a}, +-- -- { apply eq_pathover, +-- -- rewrite [▸*, ap_id, ap_compose shift_up shift_down, ↑shift_down, +-- -- @elim_glue (λk, A (succ k)) _, ↑shift_up], +-- -- apply square_of_eq, apply whisker_right, exact !elim_glue⁻¹} +-- end end +-- abstract begin +-- intro a, exact sorry +-- -- induction a, +-- -- { exact glue a}, +-- -- { apply eq_pathover, +-- -- rewrite [▸*, ap_id, ap_compose shift_down shift_up, ↑shift_up, +-- -- @elim_glue A _, ↑shift_down], +-- -- apply square_of_eq, apply whisker_right, exact !elim_glue⁻¹} +-- end end + +/- todo: define functions back and forth explicitly -/ + +definition kshift'_equiv (k : ℕ) : seq_colim f ≃ seq_colim (kshift_diag' f k) := +begin + induction k with k IH, + { reflexivity }, + { exact IH ⬝e shift_equiv (kshift_diag' f k) ⬝e + seq_colim_equiv (λn, equiv_ap A (succ_add n k)) + (λn a, proof !tr_inv_tr ⬝ !transport_lemma⁻¹ qed) } +end + +definition kshift_equiv_inv (k : ℕ) : seq_colim (kshift_diag f k) ≃ seq_colim f := +begin + induction k with k IH, + { exact seq_colim_equiv (λn, equiv_ap A (nat.zero_add n)) (λn a, !transport_lemma2) }, + { exact seq_colim_equiv (λn, equiv_ap A (succ_add k n)) + (λn a, transport_lemma2 (succ_add k n) f a) ⬝e + (shift_equiv (kshift_diag f k))⁻¹ᵉ ⬝e IH } +end + +definition kshift_equiv [constructor] (k : ℕ) : seq_colim f ≃ seq_colim (kshift_diag f k) := +(kshift_equiv_inv f k)⁻¹ᵉ + +-- definition kshift_equiv2 [constructor] (k : ℕ) : seq_colim f ≃ seq_colim (kshift_diag f k) := +-- begin +-- refine equiv_change_fun (kshift_equiv f k) _, + +-- end + +variable {f} +definition equiv_of_is_equiseq [constructor] (H : is_equiseq f) : seq_colim f ≃ A 0 := +(equiv.mk _ (is_equiv_ι _ H))⁻¹ᵉ + +definition seq_colim_constant_seq [constructor] (X : Type) : seq_colim (constant_seq X) ≃ X := +equiv_of_is_equiseq (λn, !is_equiv_id) + +variable (f) +definition is_contr_seq_colim {A : ℕ → Type} (f : seq_diagram A) + [Πk, is_contr (A k)] : is_contr (seq_colim f) := +begin + apply @is_trunc_is_equiv_closed (A 0), + apply is_equiv_ι, intro n, apply is_equiv_of_is_contr +end + +/- colimits of dependent sequences, sigma's commute with colimits -/ + +section over + +universe variable v +variables {P : Π⦃n⦄, A n → Type.{v}} (g : seq_diagram_over f P) {n : ℕ} {a : A n} +variable {f} + +definition rep_f_equiv_natural {k : ℕ} (p : P (rep f k (f a))) : + transporto P (rep_f f (succ k) a) (g p) = g (transporto P (rep_f f k a) p) := +(fn_tro_eq_tro_fn2 (rep_f f k a) g p)⁻¹ + +variable (a) +definition over_f_equiv [constructor] : + seq_colim (seq_diagram_of_over g (f a)) ≃ seq_colim (shift_diag (seq_diagram_of_over g a)) := +seq_colim_equiv (rep_f_equiv f P a) (λk p, rep_f_equiv_natural g p) + +definition seq_colim_over_equiv : + seq_colim (seq_diagram_of_over g (f a)) ≃ seq_colim (seq_diagram_of_over g a) := +over_f_equiv g a ⬝e (shift_equiv (seq_diagram_of_over g a))⁻¹ᵉ + +definition seq_colim_over_equiv_glue {k : ℕ} (x : P (rep f k (f a))) : + ap (seq_colim_over_equiv g a) (glue (seq_diagram_of_over g (f a)) x) = + ap (ι' (seq_diagram_of_over g a) (k+2)) (rep_f_equiv_natural g x) ⬝ + glue (seq_diagram_of_over g a) (rep_f f k a ▸o x) := +begin + refine ap_compose (shift_down (seq_diagram_of_over g a)) _ _ ⬝ _, + exact ap02 _ !elim_glue ⬝ !ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_glue +end + +variable {a} + +include g +definition seq_colim_over [unfold 5] (x : seq_colim f) : Type.{v} := +begin + refine seq_colim.elim_type f _ _ x, + { intro n a, exact seq_colim (seq_diagram_of_over g a)}, + { intro n a, exact seq_colim_over_equiv g a } +end +omit g + +definition ιo [constructor] (p : P a) : seq_colim_over g (ι f a) := +ι' _ 0 p + +-- Warning: the order of addition has changed in rep_rep +-- definition rep_equiv_rep_rep (l : ℕ) +-- : @seq_colim (λk, P (rep (k + l) a)) (kshift_diag' _ _) ≃ +-- @seq_colim (λk, P (rep k (rep l a))) (seq_diagram_of_over P (rep l a)) := +-- seq_colim_equiv (λk, rep_rep_equiv P a k l) abstract (λk p, +-- begin +-- esimp, +-- rewrite [+cast_apd011], +-- refine _ ⬝ (fn_tro_eq_tro_fn (rep_f k a)⁻¹ᵒ g p)⁻¹ᵖ, +-- rewrite [↑rep_f,↓rep_f k a], +-- refine !pathover_ap_invo_tro ⬝ _, +-- rewrite [apo_invo,apo_tro] +-- end) end + +variable {P} +theorem seq_colim_over_glue /- r -/ (x : seq_colim_over g (ι f (f a))) + : transport (seq_colim_over g) (glue f a) x = shift_down _ (over_f_equiv g a x) := +ap10 (elim_type_glue _ _ _ a) x + +theorem seq_colim_over_glue_inv (x : seq_colim_over g (ι f a)) + : transport (seq_colim_over g) (glue f a)⁻¹ x = to_inv (over_f_equiv g a) (shift_up _ x) := +ap10 (elim_type_glue_inv _ _ _ a) x + +definition glue_over (p : P (f a)) : pathover (seq_colim_over g) (ιo g p) (glue f a) (ι' _ 1 p) := +pathover_of_tr_eq !seq_colim_over_glue + +-- we can define a function from the colimit of total spaces to the total space of the colimit. + +/- TO DO: define glue' in the same way as glue' -/ +definition glue' (p : P a) : ⟨ι f (f a), ιo g (g p)⟩ = ⟨ι f a, ιo g p⟩ := +sigma_eq (glue f a) (glue_over g (g p) ⬝op glue (seq_diagram_of_over g a) p) + +definition glue_star (k : ℕ) (x : P (rep f k (f a))) : + ⟨ι f (f a), ι (seq_diagram_of_over g (f a)) x⟩ = + ⟨ι f a, ι (seq_diagram_of_over g a) (to_fun (rep_f_equiv f P a k) x)⟩ + :> sigma (seq_colim_over g) := +begin + apply dpair_eq_dpair (glue f a), + apply pathover_of_tr_eq, + refine seq_colim_over_glue g (ι (seq_diagram_of_over g (f a)) x) +end + +definition sigma_colim_of_colim_sigma [unfold 5] (a : seq_colim (seq_diagram_sigma g)) : + Σ(x : seq_colim f), seq_colim_over g x := +begin +induction a with n v n v, +{ induction v with a p, exact ⟨ι f a, ιo g p⟩}, +{ induction v with a p, exact glue' g p } +end + +definition colim_sigma_triangle [unfold 5] (a : seq_colim (seq_diagram_sigma g)) : + (sigma_colim_of_colim_sigma g a).1 = seq_colim_functor (λn, sigma.pr1) (λn, homotopy.rfl) a := +begin +induction a with n v n v, +{ induction v with a p, reflexivity }, +{ induction v with a p, apply eq_pathover, apply hdeg_square, + refine ap_compose sigma.pr1 _ _ ⬝ ap02 _ !elim_glue ⬝ _ ⬝ !elim_glue⁻¹, + exact !sigma_eq_pr1 ⬝ !idp_con⁻¹ } +end + +-- we now want to show that this function is an equivalence. + +/- + Kristina's proof of the induction principle of colim-sigma for sigma-colim. + It's a double induction, so we have 4 cases: point-point, point-path, path-point and path-path. + The main idea of the proof is that for the path-path case you need to fill a square, but we can + define the point-path case as a filler for this square. +-/ + +open sigma + +/- + dictionary: + Kristina | Lean + VARIABLE NAMES (A, P, k, n, e, w are the same) + x : A_n | a : A n + a : A_n → A_{n+1} | f : A n → A (n+1) + y : P(n, x) | x : P a (maybe other variables) + f : P(n, x) → P(n+1, a_n x) | g : P a → P (f a) + DEFINITION NAMES + κ | glue + U | rep_f_equiv : P (n+1+k, rep f k (f x)) ≃ P (n+k+1, rep f (k+1) x) + δ | rep_f_equiv_natural + F | over_f_equiv g a ⬝e (shift_equiv (λk, P (rep f k a)) (seq_diagram_of_over g a))⁻¹ᵉ + g_* | g_star + g | sigma_colim_rec_point +-/ + +definition glue_star_eq (k : ℕ) (x : P (rep f k (f a))) : + glue_star g k x = + dpair_eq_dpair (glue f a) (pathover_tr (glue f a) (ι (seq_diagram_of_over g (f a)) x)) ⬝ + ap (dpair (ι f a)) (seq_colim_over_glue g (ι (seq_diagram_of_over g (f a)) x)) := +ap (sigma_eq _) !pathover_of_tr_eq_eq_concato ⬝ !sigma_eq_con ⬝ whisker_left _ !ap_dpair⁻¹ + +definition g_star_step {E : (Σ(x : seq_colim f), seq_colim_over g x) → Type} + (e : Πn (a : A n) (x : P a), E ⟨ι f a, ιo g x⟩) {k : ℕ} + (IH : Π{n} {a : A n} (x : P (rep f k a)), E ⟨ι f a, ι (seq_diagram_of_over g a) x⟩) : + Σ(gs : Π⦃n : ℕ⦄ {a : A n} (x : P (rep f (k+1) a)), E ⟨ι f a, ι (seq_diagram_of_over g a) x⟩), + Π⦃n : ℕ⦄ {a : A n} (x : P (rep f k (f a))), + pathover E (IH x) (glue_star g k x) (gs (transporto P (rep_f f k a) x)) := +begin + fconstructor, + { intro n a, + refine equiv_rect (rep_f_equiv f P a k) _ _, + intro z, refine transport E _ (IH z), + exact glue_star g k z }, + { intro n a x, exact !pathover_tr ⬝op !equiv_rect_comp⁻¹ } +end + +definition g_star /- g_* -/ {E : (Σ(x : seq_colim f), seq_colim_over g x) → Type} + (e : Πn (a : A n) (x : P a), E ⟨ι f a, ιo g x⟩) {k : ℕ} : + Π {n : ℕ} {a : A n} (x : P (rep f k a)), E ⟨ι f a, ι (seq_diagram_of_over g a) x⟩ := +begin + induction k with k IH: intro n a x, + { exact e n a x }, + { apply (g_star_step g e @IH).1 } +end + +definition g_star_path_left {E : (Σ(x : seq_colim f), seq_colim_over g x) → Type} + (e : Π⦃n⦄ ⦃a : A n⦄ (x : P a), E ⟨ι f a, ιo g x⟩) + (w : Π⦃n⦄ ⦃a : A n⦄ (x : P a), pathover E (e (g x)) (glue' g x) (e x)) + {k : ℕ} {n : ℕ} {a : A n} (x : P (rep f k (f a))) : + pathover E (g_star g e x) (glue_star g k x) + (g_star g e (transporto P (rep_f f k a) x)) := +by apply (g_star_step g e (@(g_star g e) k)).2 + +/- this is the bottom of the square we have to fill in the end -/ +definition bottom_square {E : (Σ(x : seq_colim f), seq_colim_over g x) → Type} + (e : Π⦃n⦄ ⦃a : A n⦄ (x : P a), E ⟨ι f a, ιo g x⟩) + (w : Π⦃n⦄ ⦃a : A n⦄ (x : P a), pathover E (e (g x)) (glue' g x) (e x)) + (k : ℕ) {n : ℕ} {a : A n} (x : P (rep f k (f a))) := +move_top_of_right (natural_square + (λ b, dpair_eq_dpair (glue f a) (pathover_tr (glue f a) b) ⬝ + ap (dpair (ι f a)) (seq_colim_over_glue g b)) + (glue (seq_diagram_of_over g (f a)) x) ⬝hp + ap_compose (dpair (ι f a)) (to_fun (seq_colim_over_equiv g a)) + (glue (seq_diagram_of_over g (f a)) x) ⬝hp + (ap02 (dpair (ι f a)) (seq_colim_over_equiv_glue g a x)⁻¹)⁻¹ ⬝hp + ap_con (dpair (ι f a)) + (ap (λx, shift_down (seq_diagram_of_over g a) (ι (shift_diag (seq_diagram_of_over g a)) x)) + (rep_f_equiv_natural g x)) + (glue (seq_diagram_of_over g a) (to_fun (rep_f_equiv f P a k) x))) + +/- this is the composition + filler -/ +definition g_star_path_right_step {E : (Σ(x : seq_colim f), seq_colim_over g x) → Type} + (e : Π⦃n⦄ ⦃a : A n⦄ (x : P a), E ⟨ι f a, ιo g x⟩) + (w : Π⦃n⦄ ⦃a : A n⦄ (x : P a), pathover E (e (g x)) (glue' g x) (e x)) + (k : ℕ) {n : ℕ} {a : A n} (x : P (rep f k (f a))) + (IH : Π(n : ℕ) (a : A n) (x : P (rep f k a)), + pathover E (g_star g e (seq_diagram_of_over g a x)) + (ap (dpair (ι f a)) (glue (seq_diagram_of_over g a) x)) + (g_star g e x)) := +squareover_fill_r + (bottom_square g e w k x) + (change_path (glue_star_eq g (succ k) (g x)) (g_star_path_left g e w (g x)) ⬝o + pathover_ap E (dpair (ι f a)) + (pathover_ap (λ (b : seq_colim (seq_diagram_of_over g a)), E ⟨ι f a, b⟩) + (ι (seq_diagram_of_over g a)) (apd (g_star g e) (rep_f_equiv_natural g x)))) + (change_path (glue_star_eq g k x) (g_star_path_left g e w x)) + (IH (n+1) (f a) x) + +/- this is just the composition -/ +definition g_star_path_right_step1 {E : (Σ(x : seq_colim f), seq_colim_over g x) → Type} + (e : Π⦃n⦄ ⦃a : A n⦄ (x : P a), E ⟨ι f a, ιo g x⟩) + (w : Π⦃n⦄ ⦃a : A n⦄ (x : P a), pathover E (e (g x)) (glue' g x) (e x)) + (k : ℕ) {n : ℕ} {a : A n} (x : P (rep f k (f a))) + (IH : Π(n : ℕ) (a : A n) (x : P (rep f k a)), + pathover E (g_star g e (seq_diagram_of_over g a x)) + (ap (dpair (ι f a)) (glue (seq_diagram_of_over g a) x)) + (g_star g e x)) := +(g_star_path_right_step g e w k x IH).1 + +definition g_star_path_right {E : (Σ(x : seq_colim f), seq_colim_over g x) → Type} + (e : Π⦃n⦄ ⦃a : A n⦄ (x : P a), E ⟨ι f a, ιo g x⟩) + (w : Π⦃n⦄ ⦃a : A n⦄ (x : P a), pathover E (e (g x)) (glue' g x) (e x)) + (k : ℕ) {n : ℕ} {a : A n} (x : P (rep f k a)) : + pathover E (g_star g e (seq_diagram_of_over g a x)) + (ap (dpair (ι f a)) (glue (seq_diagram_of_over g a) x)) + (g_star g e x) := +begin + revert n a x, induction k with k IH: intro n a x, + { exact abstract begin refine pathover_cancel_left !pathover_tr⁻¹ᵒ (change_path _ (w x)), + apply sigma_eq_concato_eq end end }, + { revert x, refine equiv_rect (rep_f_equiv f P a k) _ _, intro x, + exact g_star_path_right_step1 g e w k x IH } +end + +definition sigma_colim_rec_point [unfold 10] /- g -/ {E : (Σ(x : seq_colim f), seq_colim_over g x) → Type} + (e : Π⦃n⦄ ⦃a : A n⦄ (x : P a), E ⟨ι f a, ιo g x⟩) + (w : Π⦃n⦄ ⦃a : A n⦄ (x : P a), pathover E (e (g x)) (glue' g x) (e x)) + {n : ℕ} {a : A n} (x : seq_colim_over g (ι f a)) : E ⟨ι f a, x⟩ := +begin + induction x with k x k x, + { exact g_star g e x }, + { apply pathover_of_pathover_ap E (dpair (ι f a)), + exact g_star_path_right g e w k x } +end + +definition sigma_colim_rec {E : (Σ(x : seq_colim f), seq_colim_over g x) → Type} + (e : Π⦃n⦄ ⦃a : A n⦄ (x : P a), E ⟨ι f a, ιo g x⟩) + (w : Π⦃n⦄ ⦃a : A n⦄ (x : P a), pathover E (e (g x)) (glue' g x) (e x)) + (v : Σ(x : seq_colim f), seq_colim_over g x) : E v := +begin + induction v with x y, + induction x with n a n a, + { exact sigma_colim_rec_point g e w y }, + { apply pi_pathover_left', intro x, + refine change_path (whisker_left _ !ap_inv ⬝ !con_inv_cancel_right) + (_ ⬝o pathover_ap E (dpair _) (apd (sigma_colim_rec_point g e w) !seq_colim_over_glue⁻¹)), + /- we can simplify the squareover we need to fill a bit if we apply this rule here -/ + -- refine change_path (ap (sigma_eq (glue f a)) !pathover_of_tr_eq_eq_concato ⬝ !sigma_eq_con ⬝ whisker_left _ !ap_dpair⁻¹) _, + induction x with k x k x, + { exact change_path !glue_star_eq (g_star_path_left g e w x) }, + -- { exact g_star_path_left g e w x }, + { apply pathover_pathover, esimp, + refine _ ⬝hop (ap (pathover_ap E _) (apd_compose2 (sigma_colim_rec_point g e w) _ _) ⬝ + pathover_ap_pathover_of_pathover_ap E (dpair (ι f a)) (seq_colim_over_equiv g a) _)⁻¹, + apply squareover_change_path_right', + refine _ ⬝hop !pathover_ap_change_path⁻¹ ⬝ ap (pathover_ap E _) + (apd02 _ !seq_colim_over_equiv_glue⁻¹), + apply squareover_change_path_right, + refine _ ⬝hop (ap (pathover_ap E _) (!apd_con ⬝ (!apd_ap ◾o idp)) ⬝ !pathover_ap_cono)⁻¹, + apply squareover_change_path_right', + apply move_right_of_top_over, + refine _ ⬝hop (ap (pathover_ap E _) !rec_glue ⬝ to_right_inv !pathover_compose _)⁻¹, + refine ap (pathover_ap E _) !rec_glue ⬝ to_right_inv !pathover_compose _ ⬝pho _, + refine _ ⬝hop !equiv_rect_comp⁻¹, + 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} + +definition colim_sigma_of_sigma_colim_constructor [unfold 7] (p : seq_colim_over g (ι f a)) + : seq_colim (seq_diagram_sigma g) := +begin + induction p with k p k p, + { exact ι _ ⟨rep f k a, p⟩}, + { apply glue} +end + +definition colim_sigma_of_sigma_colim_path1 /- μ -/ {k : ℕ} (p : P (rep f k (f a))) : + ι (seq_diagram_sigma g) ⟨rep f k (f a), p⟩ = + ι (seq_diagram_sigma g) ⟨rep f (succ k) a, transporto P (rep_f f k a) p⟩ := +begin + apply apd0111 (λn a p, ι' (seq_diagram_sigma g) n ⟨a, p⟩) (succ_add n k) (rep_f f k a), + apply pathover_tro +end + +definition colim_sigma_of_sigma_colim_path2 {k : ℕ} (p : P (rep f k (f a))) : +square (colim_sigma_of_sigma_colim_path1 g (g p)) (colim_sigma_of_sigma_colim_path1 g p) + (ap (colim_sigma_of_sigma_colim_constructor g) (glue (seq_diagram_of_over g (f a)) p)) + (ap (λx, colim_sigma_of_sigma_colim_constructor g (shift_down (seq_diagram_of_over g a) + (seq_colim_functor (λk, transporto P (rep_f f k a)) (λk p, rep_f_equiv_natural g p) x))) + (glue (seq_diagram_of_over g (f a)) p)) := +begin + refine !elim_glue ⬝ph _, + refine _ ⬝hp (ap_compose' (colim_sigma_of_sigma_colim_constructor g) _ _)⁻¹, + refine _ ⬝hp ap02 _ !seq_colim_over_equiv_glue⁻¹, + refine _ ⬝hp !ap_con⁻¹, + refine _ ⬝hp !ap_compose' ◾ !elim_glue⁻¹, + refine _ ⬝pv whisker_rt _ (natural_square0111 P (pathover_tro (rep_f f k a) p) g + (λn a p, glue (seq_diagram_sigma g) ⟨a, p⟩)), + refine _ ⬝ whisker_left _ (ap02 _ !inv_inv⁻¹ ⬝ !ap_inv), + symmetry, apply apd0111_precompose +end + +definition colim_sigma_of_sigma_colim [unfold 5] (v : Σ(x : seq_colim f), seq_colim_over g x) + : seq_colim (seq_diagram_sigma g) := +begin + induction v with x p, + induction x with n a n a, + { exact colim_sigma_of_sigma_colim_constructor g p }, + apply arrow_pathover_constant_right, intro x, esimp at x, + refine _ ⬝ ap (colim_sigma_of_sigma_colim_constructor g) !seq_colim_over_glue⁻¹, + induction x with k p k p, + { exact colim_sigma_of_sigma_colim_path1 g p }, + apply eq_pathover, apply colim_sigma_of_sigma_colim_path2 +end + +/- TODO: prove and merge these theorems -/ +definition colim_sigma_of_sigma_colim_glue' [unfold 5] (p : P a) + : ap (colim_sigma_of_sigma_colim g) (glue' g p) = glue (seq_diagram_sigma g) ⟨a, p⟩ := +begin + refine !ap_dpair_eq_dpair ⬝ _, + refine !apd011_eq_apo11_apd ⬝ _, + refine ap (λx, apo11_constant_right x _) !rec_glue ⬝ _, + refine !apo11_arrow_pathover_constant_right ⬝ _, esimp, + refine whisker_right _ !idp_con ⬝ _, + rewrite [▸*, tr_eq_of_pathover_concato_eq, ap_con, ↑glue_over, + to_right_inv !pathover_equiv_tr_eq, ap_inv, inv_con_cancel_left], + apply elim_glue +end + +theorem colim_sigma_of_sigma_colim_of_colim_sigma (a : seq_colim (seq_diagram_sigma g)) : + colim_sigma_of_sigma_colim g (sigma_colim_of_colim_sigma g a) = a := +begin +induction a with n v n v, +{ induction v with a p, reflexivity }, +{ induction v with a p, esimp, apply eq_pathover_id_right, apply hdeg_square, + refine ap_compose (colim_sigma_of_sigma_colim g) _ _ ⬝ _, + refine ap02 _ !elim_glue ⬝ _, exact colim_sigma_of_sigma_colim_glue' g p } +end + +theorem sigma_colim_of_colim_sigma_of_sigma_colim (v : Σ(x : seq_colim f), seq_colim_over g x) + : sigma_colim_of_colim_sigma g (colim_sigma_of_sigma_colim g v) = v := +begin + revert v, refine sigma_colim_rec _ _ _, + { intro n a x, reflexivity }, + { intro n a x, apply eq_pathover_id_right, apply hdeg_square, + refine ap_compose (sigma_colim_of_colim_sigma g) _ _ ⬝ _, + refine ap02 _ (colim_sigma_of_sigma_colim_glue' g x) ⬝ _, + apply elim_glue } +end + +variable (P) +definition sigma_seq_colim_over_equiv [constructor] + : (Σ(x : seq_colim f), seq_colim_over g x) ≃ seq_colim (seq_diagram_sigma g) := +equiv.MK (colim_sigma_of_sigma_colim g) + (sigma_colim_of_colim_sigma g) + (colim_sigma_of_sigma_colim_of_colim_sigma g) + (sigma_colim_of_colim_sigma_of_sigma_colim g) + +end over + +definition seq_colim_id_equiv_seq_colim_id0 (x y : A 0) : + seq_colim (id_seq_diagram f 0 x y) ≃ seq_colim (id0_seq_diagram f x y) := +seq_colim_equiv + (λn, !lrep_eq_lrep_irrel (nat.zero_add n)) + (λn p, !lrep_eq_lrep_irrel_natural) + +definition kshift_equiv_inv_incl_kshift_diag {n k : ℕ} (x : A (n + k)) : + kshift_equiv_inv f n (ι' (kshift_diag f n) k x) = ι f x := +begin + revert A f k x, induction n with n IH: intro A f k x, + { exact apd011 (ι' f) !nat.zero_add⁻¹ !pathover_tr⁻¹ᵒ }, + { exact !IH ⬝ apd011 (ι' f) !succ_add⁻¹ !pathover_tr⁻¹ᵒ } +end + +definition incl_kshift_diag {n k : ℕ} (x : A (n + k)) : + ι' (kshift_diag f n) k x = kshift_equiv f n (ι f x) := +eq_inv_of_eq (kshift_equiv_inv_incl_kshift_diag f x) + +definition incl_kshift_diag0 {n : ℕ} (x : A n) : + ι' (kshift_diag f n) 0 x = kshift_equiv f n (ι f x) := +incl_kshift_diag f x + +definition seq_colim_eq_equiv0' (a₀ a₁ : A 0) : ι f a₀ = ι f a₁ ≃ seq_colim (id_seq_diagram f 0 a₀ a₁) := +begin + refine total_space_method2 (ι f a₀) (seq_colim_over (id0_seq_diagram_over f a₀)) _ _ (ι f a₁) ⬝e _, + { apply @(is_trunc_equiv_closed_rev _ + (sigma_seq_colim_over_equiv _ _)), apply is_contr_seq_colim }, + { exact ιo _ idp }, + /- + In the next equivalence we have to show that + seq_colim_over (id0_seq_diagram_over f a₀) (ι f a₁) ≃ seq_colim (id_seq_diagram f 0 a₀ a₁). + This looks trivial, because both of them reduce to + seq_colim (f^{0 ≤ 0+k}(a₀) = f^{0 ≤ 0+k}(a₁), ap_f). + However, not all proofs of these inequalities are definitionally equal. 3 of them are proven by + zero_le : 0 ≤ n, + but one of them (the RHS of seq_colim_over (id0_seq_diagram_over f a₀) (ι f a₁)) uses + le_add_right : n ≤ n+k + Alternatively, we could redefine le_add_right so that for n=0, it reduces to `zero_le (0+k)`. + -/ + { refine seq_colim_equiv (λn, eq_equiv_eq_closed !lrep_irrel idp) _, + intro n p, refine whisker_right _ (!lrep_irrel2⁻² ⬝ !ap_inv⁻¹) ⬝ !ap_con⁻¹ } +end + +definition seq_colim_eq_equiv0 (x y : A 0) : ι f x = ι f y ≃ seq_colim (id0_seq_diagram f x y) := +seq_colim_eq_equiv0' f x y ⬝e seq_colim_id_equiv_seq_colim_id0 f x y + +definition seq_colim_eq_equiv {n : ℕ} (x y : A n) : + ι f x = ι f y ≃ seq_colim (id_seq_diagram f n x y) := +eq_equiv_fn_eq_of_equiv (kshift_equiv f n) (ι f x) (ι f y) ⬝e +eq_equiv_eq_closed (incl_kshift_diag0 f x)⁻¹ (incl_kshift_diag0 f y)⁻¹ ⬝e +seq_colim_eq_equiv0' (kshift_diag f n) x y ⬝e +@seq_colim_equiv _ _ _ (λk, ap (@f _)) + (λm, eq_equiv_eq_closed !lrep_kshift_diag !lrep_kshift_diag) + (λm p, whisker_right _ (whisker_right _ !ap_inv⁻¹ ⬝ !ap_con⁻¹) ⬝ !ap_con⁻¹) ⬝e +seq_colim_equiv + (λm, !lrep_eq_lrep_irrel (ap (add n) (nat.zero_add m))) + begin + intro m q, + refine _ ⬝ lrep_eq_lrep_irrel_natural f (le_add_right n m) (ap (add n) (nat.zero_add m)) q, + exact ap (λx, lrep_eq_lrep_irrel f _ _ _ _ x _) !is_prop.elim + end + +open algebra +theorem is_trunc_seq_colim [instance] (k : ℕ₋₂) [H : Πn, is_trunc k (A n)] : + is_trunc k (seq_colim f) := +begin + revert A f H, induction k with k IH: intro A f H, + { apply is_contr_seq_colim }, + { apply is_trunc_succ_intro, intro x y, + induction x using seq_colim.rec_prop with n a, + induction y using seq_colim.rec_prop with m a', + apply is_trunc_equiv_closed, + exact eq_equiv_eq_closed (lrep_glue _ (le_max_left n m) _) (lrep_glue _ (le_max_right n m) _), + apply is_trunc_equiv_closed_rev, + apply seq_colim_eq_equiv, + apply IH, intro l, apply is_trunc_eq } +end + +definition seq_colim_trunc_of_trunc_seq_colim [unfold 4] (k : ℕ₋₂) (x : trunc k (seq_colim f)) : + seq_colim (trunc_diagram k f) := +begin induction x with x, exact seq_colim_functor (λn, tr) (λn y, idp) x end + +definition trunc_seq_colim_of_seq_colim_trunc [unfold 4] (k : ℕ₋₂) + (x : seq_colim (trunc_diagram k f)) : trunc k (seq_colim f) := +begin + induction x with n x n x, + { induction x with a, exact tr (ι f a) }, + { induction x with a, exact ap tr (glue f a) } +end + +definition trunc_seq_colim_equiv [constructor] (k : ℕ₋₂) : + trunc k (seq_colim f) ≃ seq_colim (trunc_diagram k f) := +equiv.MK (seq_colim_trunc_of_trunc_seq_colim f k) (trunc_seq_colim_of_seq_colim_trunc f k) + abstract begin + intro x, induction x with n x n x, + { induction x with a, reflexivity }, + { induction x with a, apply eq_pathover_id_right, apply hdeg_square, + refine ap_compose (seq_colim_trunc_of_trunc_seq_colim f k) _ _ ⬝ ap02 _ !elim_glue ⬝ _, + refine !ap_compose'⁻¹ ⬝ !elim_glue ⬝ _, exact !idp_con } + end end + abstract begin + intro x, induction x with x, induction x with n a n a, + { reflexivity }, + { apply eq_pathover, apply hdeg_square, + refine ap_compose (trunc_seq_colim_of_seq_colim_trunc f k) _ _ ⬝ ap02 _ !elim_glue ⬝ _, + refine !ap_compose'⁻¹ ⬝ !elim_glue } + end end + +/- the colimit of a sequence of fibers is the fiber of the functorial action of the colimit -/ +definition domain_seq_colim_functor {A A' : ℕ → Type} {f : seq_diagram A} + {f' : seq_diagram A'} (τ : Πn, A' n → A n) + (p : Π⦃n⦄, τ (n+1) ∘ @f' n ~ @f n ∘ @τ n) : + (Σ(x : seq_colim f), seq_colim_over (seq_diagram_over_fiber τ p) x) ≃ seq_colim f' := +begin + transitivity seq_colim (seq_diagram_sigma (seq_diagram_over_fiber τ p)), + exact sigma_seq_colim_over_equiv _ (seq_diagram_over_fiber τ p), + exact seq_colim_equiv (λn, sigma_fiber_equiv (τ n)) (λn x, idp) +end + +definition fiber_seq_colim_functor {A A' : ℕ → Type} {f : seq_diagram A} + {f' : seq_diagram A'} (τ : Πn, A' n → A n) + (p : Π⦃n⦄, τ (n+1) ∘ @f' n ~ @f n ∘ @τ n) {n : ℕ} (a : A n) : + fiber (seq_colim_functor τ p) (ι f a) ≃ seq_colim (seq_diagram_fiber τ p a) := +begin + refine _ ⬝e fiber_pr1 (seq_colim_over (seq_diagram_over_fiber τ p)) (ι f a), + apply fiber_equiv_of_triangle (domain_seq_colim_functor τ p)⁻¹ᵉ, + refine _ ⬝hty λx, (colim_sigma_triangle _ _)⁻¹, + apply homotopy_inv_of_homotopy_pre (seq_colim_equiv _ _) (seq_colim_functor _ _) (seq_colim_functor _ _), + refine (λx, !seq_colim_functor_compose⁻¹) ⬝hty _, + refine seq_colim_functor_homotopy _ _, + intro n x, exact point_eq x.2, + intro n x, induction x with x y, induction y with y q, induction q, + apply square_of_eq, refine !idp_con⁻¹ +end + +definition fiber_seq_colim_functor0 {A A' : ℕ → Type} {f : seq_diagram A} + {f' : seq_diagram A'} (τ : Πn, A' n → A n) + (p : Π⦃n⦄, τ (n+1) ∘ @f' n ~ @f n ∘ @τ n) (a : A 0) : + fiber (seq_colim_functor τ p) (ι f a) ≃ seq_colim (seq_diagram_fiber0 τ p a) := +sorry + + +/- the sequential colimit of standard finite types is ℕ -/ +open fin +definition nat_of_seq_colim_fin [unfold 1] (x : seq_colim seq_diagram_fin) : ℕ := +begin + induction x with n x n x, + { exact x }, + { reflexivity } +end + +definition seq_colim_fin_of_nat (n : ℕ) : seq_colim seq_diagram_fin := +ι' _ (n+1) (fin.mk n (self_lt_succ n)) + +definition lrep_seq_diagram_fin {n : ℕ} (x : fin n) : + lrep seq_diagram_fin (is_lt x) (fin.mk x (self_lt_succ x)) = x := +begin + induction x with k H, esimp, induction H with n H p, + reflexivity, + exact ap (@lift_succ2 _) p +end + +definition lrep_seq_diagram_fin_lift_succ {n : ℕ} (x : fin n) : + lrep_seq_diagram_fin (lift_succ2 x) = ap (@lift_succ2 _) (lrep_seq_diagram_fin x) := +begin + induction x with k H, reflexivity +end + +definition seq_colim_fin_equiv [constructor] : seq_colim seq_diagram_fin ≃ ℕ := +equiv.MK nat_of_seq_colim_fin seq_colim_fin_of_nat + abstract begin + intro n, reflexivity + end end + abstract begin + intro x, induction x with n x n x, + { esimp, refine (lrep_glue _ (is_lt x) _)⁻¹ ⬝ ap (ι _) (lrep_seq_diagram_fin x), }, + { apply eq_pathover_id_right, + refine ap_compose seq_colim_fin_of_nat _ _ ⬝ ap02 _ !elim_glue ⬝ph _, + esimp, refine (square_of_eq !con_idp)⁻¹ʰ ⬝h _, + refine _ ⬝pv natural_square_tr (@glue _ (seq_diagram_fin) n) (lrep_seq_diagram_fin x), + refine ap02 _ !lrep_seq_diagram_fin_lift_succ ⬝ !ap_compose⁻¹ } + end end + +/- the sequential colimit of embeddings is an embedding -/ + +definition seq_colim_eq_equiv0'_inv_refl (a₀ : A 0) : + (seq_colim_eq_equiv0' f a₀ a₀)⁻¹ᵉ (ι' (id_seq_diagram f 0 a₀ a₀) 0 proof (refl a₀) qed) = refl (ι f a₀) := +begin + apply inv_eq_of_eq, + reflexivity, +end + +definition is_embedding_ι (H : Πn, is_embedding (@f n)) : is_embedding (ι' f 0) := +begin + intro x y, fapply is_equiv_of_equiv_of_homotopy, + { symmetry, refine seq_colim_eq_equiv0' f x y ⬝e _, + apply equiv_of_is_equiseq, intro n, apply H }, + { intro p, induction p, apply seq_colim_eq_equiv0'_inv_refl } +end + +end seq_colim diff --git a/colimit/sequence.hlean b/colimit/sequence.hlean new file mode 100644 index 0000000..98229a7 --- /dev/null +++ b/colimit/sequence.hlean @@ -0,0 +1,263 @@ +/- +Copyright (c) 2015 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Floris van Doorn, Egbert Rijke +-/ + +import ..move_to_lib types.fin types.trunc + +open nat eq equiv sigma sigma.ops is_equiv is_trunc trunc prod fiber + +namespace seq_colim + + definition seq_diagram [reducible] (A : ℕ → Type) : Type := Π⦃n⦄, A n → A (succ n) + + structure Seq_diagram : Type := + (carrier : ℕ → Type) + (struct : seq_diagram carrier) + + definition is_equiseq [reducible] {A : ℕ → Type} (f : seq_diagram A) : Type := + forall (n : ℕ), is_equiv (@f n) + + structure Equi_seq : Type := + (carrier : ℕ → Type) + (maps : seq_diagram carrier) + (prop : is_equiseq maps) + + protected abbreviation Mk [constructor] := Seq_diagram.mk + attribute Seq_diagram.carrier [coercion] + attribute Seq_diagram.struct [coercion] + + variables {A A' : ℕ → Type} (f : seq_diagram A) (f' : seq_diagram A') + include f + + definition lrep {n m : ℕ} (H : n ≤ m) (a : A n) : A m := + begin + induction H with m H y, + { exact a }, + { exact f y } + end + + definition lrep_irrel_pathover {n m m' : ℕ} (H₁ : n ≤ m) (H₂ : n ≤ m') (p : m = m') (a : A n) : + lrep f H₁ a =[p] lrep f H₂ a := + apo (λm H, lrep f H a) !is_prop.elimo + + definition lrep_irrel {n m : ℕ} (H₁ H₂ : n ≤ m) (a : A n) : lrep f H₁ a = lrep f H₂ a := + ap (λH, lrep f H a) !is_prop.elim + + definition lrep_eq_transport {n m : ℕ} (H : n ≤ m) (p : n = m) (a : A n) : lrep f H a = transport A p a := + begin induction p, exact lrep_irrel f H (nat.le_refl n) a end + + definition lrep_irrel2 {n m : ℕ} (H₁ H₂ : n ≤ m) (a : A n) : + lrep_irrel f (le.step H₁) (le.step H₂) a = ap (@f m) (lrep_irrel f H₁ H₂ a) := + begin + have H₁ = H₂, from !is_prop.elim, induction this, + refine ap02 _ !is_prop_elim_self ⬝ _ ⬝ ap02 _(ap02 _ !is_prop_elim_self⁻¹), + reflexivity + end + + definition lrep_eq_lrep_irrel {n m m' : ℕ} (H₁ : n ≤ m) (H₂ : n ≤ m') (a₁ a₂ : A n) (p : m = m') : + (lrep f H₁ a₁ = lrep f H₁ a₂) ≃ (lrep f H₂ a₁ = lrep f H₂ a₂) := + equiv_apd011 (λm H, lrep f H a₁ = lrep f H a₂) (is_prop.elimo p H₁ H₂) + + definition lrep_eq_lrep_irrel_natural {n m m' : ℕ} {H₁ : n ≤ m} (H₂ : n ≤ m') {a₁ a₂ : A n} + (p : m = m') (q : lrep f H₁ a₁ = lrep f H₁ a₂) : + lrep_eq_lrep_irrel f (le.step H₁) (le.step H₂) a₁ a₂ (ap succ p) (ap (@f m) q) = + ap (@f m') (lrep_eq_lrep_irrel f H₁ H₂ a₁ a₂ p q) := + begin + esimp [lrep_eq_lrep_irrel], + symmetry, + refine fn_tro_eq_tro_fn2 _ (λa₁ a₂, ap (@f _)) q ⬝ _, + refine ap (λx, x ▸o _) (@is_prop.elim _ _ _ _), + apply is_trunc_pathover + end + + definition is_equiv_lrep [constructor] [Hf : is_equiseq f] {n m : ℕ} (H : n ≤ m) : + is_equiv (lrep f H) := + begin + induction H with m H Hlrepf, + { apply is_equiv_id }, + { exact is_equiv_compose (@f _) (lrep f H) }, + end + + local attribute is_equiv_lrep [instance] + definition lrep_back [reducible] [Hf : is_equiseq f] {n m : ℕ} (H : n ≤ m) : A m → A n := + (lrep f H)⁻¹ᶠ + + section generalized_lrep + variable {n : ℕ} + + -- definition lrep_pathover_lrep0 [reducible] (k : ℕ) (a : A 0) : lrep f k a =[nat.zero_add k] lrep0 f k a := + -- begin induction k with k p, constructor, exact pathover_ap A succ (apo f p) end + + /- lreplace le_of_succ_le with this -/ + + definition lrep_f {n m : ℕ} (H : succ n ≤ m) (a : A n) : + lrep f H (f a) = lrep f (le_step_left H) a := + begin + induction H with m H p, + { reflexivity }, + { exact ap (@f m) p } + end + + definition lrep_lrep {n m k : ℕ} (H1 : n ≤ m) (H2 : m ≤ k) (a : A n) : + lrep f H2 (lrep f H1 a) = lrep f (nat.le_trans H1 H2) a := + begin + induction H2 with k H2 p, + { reflexivity }, + { exact ap (@f k) p } + end + + -- -- this should be a squareover + -- definition lrep_lrep_succ (k l : ℕ) (a : A n) : + -- lrep_lrep f k (succ l) a = change_path (idontwanttoprovethis n l k) + -- (lrep_f f k (lrep f l a) ⬝o + -- lrep_lrep f (succ k) l a ⬝o + -- pathover_ap _ (λz, n + z) (apd (λz, lrep f z a) (succ_add l k)⁻¹ᵖ)) := + -- begin + -- induction k with k IH, + -- { constructor}, + -- { exact sorry} + -- end + + definition f_lrep {n m : ℕ} (H : n ≤ m) (a : A n) : f (lrep f H a) = lrep f (le.step H) a := idp + + definition rep (m : ℕ) (a : A n) : A (n + m) := + lrep f (le_add_right n m) a + + definition rep0 (m : ℕ) (a : A 0) : A m := + lrep f (zero_le m) a + + -- definition old_rep (m : ℕ) (a : A n) : A (n + m) := + -- by induction m with m y; exact a; exact f y + + -- definition rep_eq_old_rep (m : ℕ) (a : A n) : rep f m a = old_rep f m a := + -- by induction m with m p; reflexivity; exact ap (@f _) p + + definition rep_f (k : ℕ) (a : A n) : + pathover A (rep f k (f a)) (succ_add n k) (rep f (succ k) a) := + begin + induction k with k IH, + { constructor }, + { unfold [succ_add], apply pathover_ap, exact apo f IH} + end + + definition rep_rep (k l : ℕ) (a : A n) : + pathover A (rep f k (rep f l a)) (nat.add_assoc n l k) (rep f (l + k) a) := + begin + induction k with k IH, + { constructor}, + { apply pathover_ap, exact apo f IH} + end + + end generalized_lrep + + section shift + + definition shift_diag [unfold_full] : seq_diagram (λn, A (succ n)) := + λn a, f a + + definition kshift_diag [unfold_full] (k : ℕ) : seq_diagram (λn, A (k + n)) := + λn a, f a + + definition kshift_diag' [unfold_full] (k : ℕ) : seq_diagram (λn, A (n + k)) := + λn a, transport A (succ_add n k)⁻¹ (f a) + + definition lrep_kshift_diag {n m k : ℕ} (H : m ≤ k) (a : A (n + m)) : + lrep (kshift_diag f n) H a = lrep f (nat.add_le_add_left2 H n) a := + by induction H with k H p; reflexivity; exact ap (@f _) p + + end shift + + section constructions + + omit f + + definition constant_seq (X : Type) : seq_diagram (λ n, X) := + λ n x, x + + definition seq_diagram_arrow_left [unfold_full] (X : Type) : seq_diagram (λn, X → A n) := + λn g x, f (g x) + + definition seq_diagram_prod [unfold_full] : seq_diagram (λn, A n × A' n) := + λn, prod_functor (@f n) (@f' n) + + open fin + definition seq_diagram_fin [unfold_full] : seq_diagram fin := + lift_succ2 + + definition id0_seq [unfold_full] (a₁ a₂ : A 0) : ℕ → Type := + λ k, rep0 f k a₁ = lrep f (zero_le k) a₂ + + definition id0_seq_diagram [unfold_full] (a₁ a₂ : A 0) : seq_diagram (id0_seq f a₁ a₂) := + λ (k : ℕ) (p : rep0 f k a₁ = rep0 f k a₂), ap (@f k) p + + definition id_seq [unfold_full] (n : ℕ) (a₁ a₂ : A n) : ℕ → Type := + λ k, rep f k a₁ = rep f k a₂ + + definition id_seq_diagram [unfold_full] (n : ℕ) (a₁ a₂ : A n) : seq_diagram (id_seq f n a₁ a₂) := + λ (k : ℕ) (p : rep f k a₁ = rep f k a₂), ap (@f (n + k)) p + + definition trunc_diagram [unfold_full] (k : ℕ₋₂) (f : seq_diagram A) : + seq_diagram (λn, trunc k (A n)) := + λn, trunc_functor k (@f n) + + end constructions + + section over + + variable {A} + variable (P : Π⦃n⦄, A n → Type) + + definition seq_diagram_over : Type := Π⦃n⦄ {a : A n}, P a → P (f a) + + definition weakened_sequence [unfold_full] : seq_diagram_over f (λn a, A' n) := + λn a a', f' a' + + definition id0_seq_diagram_over [unfold_full] (a₀ : A 0) : + seq_diagram_over f (λn a, lrep f (zero_le n) a₀ = a) := + λn a p, ap (@f n) p + + variable (g : seq_diagram_over f P) + variables {f P} + + definition seq_diagram_of_over [unfold_full] {n : ℕ} (a : A n) : + seq_diagram (λk, P (rep f k a)) := + λk p, g p + + definition seq_diagram_sigma [unfold 6] : seq_diagram (λn, Σ(x : A n), P x) := + λn v, ⟨f v.1, g v.2⟩ + + variables {n : ℕ} (f P) + + theorem rep_f_equiv [constructor] (a : A n) (k : ℕ) : + P (lrep f (le_add_right (succ n) k) (f a)) ≃ P (lrep f (le_add_right n (succ k)) a) := + equiv_apd011 P (rep_f f k a) + + theorem rep_rep_equiv [constructor] (a : A n) (k l : ℕ) : + P (rep f (l + k) a) ≃ P (rep f k (rep f l a)) := + (equiv_apd011 P (rep_rep f k l a))⁻¹ᵉ + + end over + + omit f + -- do we need to generalize this to the case where the bottom sequence consists of equivalences? + definition seq_diagram_pi {X : Type} {A : X → ℕ → Type} (g : Π⦃x n⦄, A x n → A x (succ n)) : + seq_diagram (λn, Πx, A x n) := + λn f x, g (f x) + + variables {f f'} + definition seq_diagram_over_fiber (g : Π⦃n⦄, A n → A' n) + (p : Π⦃n⦄ (a : A n), g (f a) = f' (g a)) : seq_diagram_over f' (λn, fiber (@g n)) := + λk a, fiber_functor (@f k) (@f' k) (@p k) idp + + definition seq_diagram_fiber (g : Π⦃n⦄, A n → A' n) (p : Π⦃n⦄ (a : A n), g (f a) = f' (g a)) + {n : ℕ} (a : A' n) : seq_diagram (λk, fiber (@g (n + k)) (rep f' k a)) := + seq_diagram_of_over (seq_diagram_over_fiber g p) a + + definition seq_diagram_fiber0 (g : Π⦃n⦄, A n → A' n) (p : Π⦃n⦄ (a : A n), g (f a) = f' (g a)) + (a : A' 0) : seq_diagram (λk, fiber (@g k) (rep0 f' k a)) := + λk, fiber_functor (@f k) (@f' k) (@p k) idp + + +end seq_colim diff --git a/move_to_lib.hlean b/move_to_lib.hlean index d5a8299..67baf7c 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -8,9 +8,12 @@ open eq nat int susp pointed sigma is_equiv equiv fiber algebra trunc pi group attribute pType.sigma_char sigma_pi_equiv_pi_sigma sigma.coind_unc [constructor] attribute ap1_gen [unfold 8 9 10] attribute ap010 [unfold 7] +attribute tro_invo_tro [unfold 9] -- TODO: move -- TODO: homotopy_of_eq and apd10 should be the same -- TODO: there is also apd10_eq_of_homotopy in both pi and eq(?) + + namespace algebra variables {A : Type} [add_ab_inf_group A] @@ -21,6 +24,10 @@ end algebra namespace eq +definition homotopy.symm_symm {A : Type} {P : A → Type} {f g : Πx, P x} (H : f ~ g) : + H⁻¹ʰᵗʸ⁻¹ʰᵗʸ = H := +begin apply eq_of_homotopy, intro x, apply inv_inv end + definition apd10_prepostcompose_nondep {A B C D : Type} (h : C → D) {g g' : B → C} (p : g = g') (f : A → B) (a : A) : apd10 (ap (λg a, h (g (f a))) p) a = ap h (apd10 p (f a)) := begin induction p, reflexivity end @@ -123,6 +130,162 @@ namespace eq homotopy_group_isomorphism_of_pequiv n f ⬝g ghomotopy_group_ptrunc_of_le H B +definition equiv_pathover2 {A : Type} {a a' : A} (p : a = a') + {B : A → Type} {C : A → Type} (f : B a ≃ C a) (g : B a' ≃ C a') + (r : to_fun f =[p] to_fun g) : f =[p] g := +begin + fapply pathover_of_fn_pathover_fn, + { intro a, apply equiv.sigma_char }, + { apply sigma_pathover _ _ _ r, apply is_prop.elimo } +end + +definition equiv_pathover_inv {A : Type} {a a' : A} (p : a = a') + {B : A → Type} {C : A → Type} (f : B a ≃ C a) (g : B a' ≃ C a') + (r : to_inv f =[p] to_inv g) : f =[p] g := +begin + /- this proof is a bit weird, but it works -/ + apply equiv_pathover2, + change f⁻¹ᶠ⁻¹ᶠ =[p] g⁻¹ᶠ⁻¹ᶠ, + apply apo (λ(a: A) (h : C a ≃ B a), h⁻¹ᶠ), + apply equiv_pathover2, + exact r +end + +definition transport_lemma {A : Type} {C : A → Type} {g₁ : A → A} + {x y : A} (p : x = y) (f : Π⦃x⦄, C x → C (g₁ x)) (z : C x) : + transport C (ap g₁ p)⁻¹ (f (transport C p z)) = f z := +by induction p; reflexivity + +definition transport_lemma2 {A : Type} {C : A → Type} {g₁ : A → A} + {x y : A} (p : x = y) (f : Π⦃x⦄, C x → C (g₁ x)) (z : C x) : + transport C (ap g₁ p) (f z) = f (transport C p z) := +by induction p; reflexivity + +definition eq_of_pathover_apo {A C : Type} {B : A → Type} {a a' : A} {b : B a} {b' : B a'} + {p : a = a'} (g : Πa, B a → C) (q : b =[p] b') : + eq_of_pathover (apo g q) = apd011 g p q := +by induction q; reflexivity + + definition apd02 [unfold 8] {A : Type} {B : A → Type} (f : Πa, B a) {a a' : A} {p q : a = a'} + (r : p = q) : change_path r (apd f p) = apd f q := + by induction r; reflexivity + + definition pathover_ap_cono {A A' : Type} {a₁ a₂ a₃ : A} + {p₁ : a₁ = a₂} {p₂ : a₂ = a₃} (B' : A' → Type) (f : A → A') + {b₁ : B' (f a₁)} {b₂ : B' (f a₂)} {b₃ : B' (f a₃)} + (q₁ : b₁ =[p₁] b₂) (q₂ : b₂ =[p₂] b₃) : + pathover_ap B' f (q₁ ⬝o q₂) = + change_path !ap_con⁻¹ (pathover_ap B' f q₁ ⬝o pathover_ap B' f q₂) := + by induction q₁; induction q₂; reflexivity + + definition concato_eq_eq {A : Type} {B : A → Type} {a₁ a₂ : A} {p₁ : a₁ = a₂} + {b₁ : B a₁} {b₂ b₂' : B a₂} (r : b₁ =[p₁] b₂) (q : b₂ = b₂') : + r ⬝op q = r ⬝o pathover_idp_of_eq q := + by induction q; reflexivity + +definition ap_apd0111 {A₁ A₂ A₃ : Type} {B : A₁ → Type} {C : Π⦃a⦄, B a → Type} {a a₂ : A₁} + {b : B a} {b₂ : B a₂} {c : C b} {c₂ : C b₂} + (g : A₂ → A₃) (f : Πa b, C b → A₂) (Ha : a = a₂) (Hb : b =[Ha] b₂) + (Hc : c =[apd011 C Ha Hb] c₂) : + ap g (apd0111 f Ha Hb Hc) = apd0111 (λa b c, (g (f a b c))) Ha Hb Hc := +by induction Hb; induction Hc using idp_rec_on; reflexivity + +section squareover + + variables {A A' : Type} {B : A → Type} + {a a' a'' a₀₀ a₂₀ a₄₀ a₀₂ a₂₂ a₂₄ a₀₄ a₄₂ a₄₄ : A} + /-a₀₀-/ {p₁₀ : a₀₀ = a₂₀} /-a₂₀-/ {p₃₀ : a₂₀ = a₄₀} /-a₄₀-/ + {p₀₁ : a₀₀ = a₀₂} /-s₁₁-/ {p₂₁ : a₂₀ = a₂₂} /-s₃₁-/ {p₄₁ : a₄₀ = a₄₂} + /-a₀₂-/ {p₁₂ : a₀₂ = a₂₂} /-a₂₂-/ {p₃₂ : a₂₂ = a₄₂} /-a₄₂-/ + {p₀₃ : a₀₂ = a₀₄} /-s₁₃-/ {p₂₃ : a₂₂ = a₂₄} /-s₃₃-/ {p₄₃ : a₄₂ = a₄₄} + /-a₀₄-/ {p₁₄ : a₀₄ = a₂₄} /-a₂₄-/ {p₃₄ : a₂₄ = a₄₄} /-a₄₄-/ + {s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁} {s₃₁ : square p₃₀ p₃₂ p₂₁ p₄₁} + {s₁₃ : square p₁₂ p₁₄ p₀₃ p₂₃} {s₃₃ : square p₃₂ p₃₄ p₂₃ p₄₃} + + {b : B a} + {b₀₀ : B a₀₀} {b₂₀ : B a₂₀} {b₄₀ : B a₄₀} + {b₀₂ : B a₀₂} {b₂₂ : B a₂₂} {b₄₂ : B a₄₂} + {b₀₄ : B a₀₄} {b₂₄ : B a₂₄} {b₄₄ : B a₄₄} + /-b₀₀-/ {q₁₀ : b₀₀ =[p₁₀] b₂₀} /-b₂₀-/ {q₃₀ : b₂₀ =[p₃₀] b₄₀} /-b₄₀-/ + /-b₀₂-/ {q₁₂ : b₀₂ =[p₁₂] b₂₂} /-b₂₂-/ {q₃₂ : b₂₂ =[p₃₂] b₄₂} /-b₄₂-/ + /-b₀₄-/ {q₁₄ : b₀₄ =[p₁₄] b₂₄} /-b₂₄-/ {q₃₄ : b₂₄ =[p₃₄] b₄₄} /-b₄₄-/ + {q₀₁ : b₀₀ =[p₀₁] b₀₂} /-t₁₁-/ {q₂₁ : b₂₀ =[p₂₁] b₂₂} /-t₃₁-/ {q₄₁ : b₄₀ =[p₄₁] b₄₂} + {q₀₃ : b₀₂ =[p₀₃] b₀₄} /-t₁₃-/ {q₂₃ : b₂₂ =[p₂₃] b₂₄} /-t₃₃-/ {q₄₃ : b₄₂ =[p₄₃] b₄₄} + + definition move_right_of_top_over {p : a₀₀ = a} {p' : a = a₂₀} + {s : square p p₁₂ p₀₁ (p' ⬝ p₂₁)} {q : b₀₀ =[p] b} {q' : b =[p'] b₂₀} + (t : squareover B (move_top_of_right s) (q ⬝o q') q₁₂ q₀₁ q₂₁) : + squareover B s q q₁₂ q₀₁ (q' ⬝o q₂₁) := + begin induction q', induction q, induction q₂₁, exact t end + + /- TODO: replace the version in the library by this -/ + definition hconcato_pathover' {p : a₂₀ = a₂₂} {sp : p = p₂₁} {s : square p₁₀ p₁₂ p₀₁ p} + {q : b₂₀ =[p] b₂₂} (t₁₁ : squareover B (s ⬝hp sp) q₁₀ q₁₂ q₀₁ q₂₁) + (r : change_path sp q = q₂₁) : squareover B s q₁₀ q₁₂ q₀₁ q := + by induction sp; induction r; exact t₁₁ + + variables (s₁₁ q₀₁ q₁₀ q₂₁ q₁₂) + definition squareover_fill_t : Σ (q : b₀₀ =[p₁₀] b₂₀), squareover B s₁₁ q q₁₂ q₀₁ q₂₁ := + begin + induction s₁₁, induction q₀₁ using idp_rec_on, induction q₂₁ using idp_rec_on, + induction q₁₂ using idp_rec_on, exact ⟨idpo, idso⟩ + end + + definition squareover_fill_b : Σ (q : b₀₂ =[p₁₂] b₂₂), squareover B s₁₁ q₁₀ q q₀₁ q₂₁ := + begin + induction s₁₁, induction q₀₁ using idp_rec_on, induction q₂₁ using idp_rec_on, + induction q₁₀ using idp_rec_on, exact ⟨idpo, idso⟩ + end + + definition squareover_fill_l : Σ (q : b₀₀ =[p₀₁] b₀₂), squareover B s₁₁ q₁₀ q₁₂ q q₂₁ := + begin + induction s₁₁, induction q₁₀ using idp_rec_on, induction q₂₁ using idp_rec_on, + induction q₁₂ using idp_rec_on, exact ⟨idpo, idso⟩ + end + + definition squareover_fill_r : Σ (q : b₂₀ =[p₂₁] b₂₂) , squareover B s₁₁ q₁₀ q₁₂ q₀₁ q := + begin + induction s₁₁, induction q₀₁ using idp_rec_on, induction q₁₀ using idp_rec_on, + induction q₁₂ using idp_rec_on, exact ⟨idpo, idso⟩ + end + + +end squareover + +/- move this to types.eq, and replace the proof there -/ + section + parameters {A : Type} (a₀ : A) (code : A → Type) (H : is_contr (Σa, code a)) + (c₀ : code a₀) + include H c₀ + protected definition encode2 {a : A} (q : a₀ = a) : code a := + transport code q c₀ + + protected definition decode2' {a : A} (c : code a) : a₀ = a := + have ⟨a₀, c₀⟩ = ⟨a, c⟩ :> Σa, code a, from !is_prop.elim, + this..1 + + protected definition decode2 {a : A} (c : code a) : a₀ = a := + (decode2' c₀)⁻¹ ⬝ decode2' c + + open sigma.ops + definition total_space_method2 (a : A) : (a₀ = a) ≃ code a := + begin + fapply equiv.MK, + { exact encode2 }, + { exact decode2 }, + { intro c, unfold [encode2, decode2, decode2'], + rewrite [is_prop_elim_self, ▸*, idp_con], + apply tr_eq_of_pathover, apply eq_pr2 }, + { intro q, induction q, esimp, apply con.left_inv, }, + end + end + +definition total_space_method2_refl {A : Type} (a₀ : A) (code : A → Type) (H : is_contr (Σa, code a)) + (c₀ : code a₀) : total_space_method2 a₀ code H c₀ a₀ idp = c₀ := +begin + reflexivity +end + section hsquare variables {A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type} {f₁₀ : A₀₀ → A₂₀} {f₃₀ : A₂₀ → A₄₀} @@ -209,6 +372,21 @@ namespace nat exact q ⬝htyh p end +definition iterate_equiv2 {A : Type} {C : A → Type} (f : A → A) (h : Πa, C a ≃ C (f a)) + (k : ℕ) (a : A) : C a ≃ C (f^[k] a) := +begin induction k with k IH, reflexivity, exact IH ⬝e h (f^[k] a) end + + + + /- replace proof of le_of_succ_le by this -/ + definition le_step_left {n m : ℕ} (H : succ n ≤ m) : n ≤ m := + by induction H with H m H'; exact le_succ n; exact le.step H' + + /- TODO: make proof of le_succ_of_le simpler -/ + + definition nat.add_le_add_left2 {n m : ℕ} (H : n ≤ m) (k : ℕ) : k + n ≤ k + m := + by induction H with m H H₂; reflexivity; exact le.step H₂ + end nat @@ -511,6 +689,29 @@ namespace sigma change_path (ap_sigma_pr1 f g p)⁻¹ (pathover_ap C f (apd g p)) := by induction p; reflexivity +definition ap_sigma_functor_sigma_eq {A A' : Type} {B : A → Type} {B' : A' → Type} + {a a' : A} {b : B a} {b' : B a'} (f : A → A') (g : Πa, B a → B' (f a)) (p : a = a') (q : b =[p] b') : + ap (sigma_functor f g) (sigma_eq p q) = sigma_eq (ap f p) (pathover_ap B' f (apo g q)) := +by induction q; reflexivity + +definition ap_sigma_functor_id_sigma_eq {A : Type} {B B' : A → Type} + {a a' : A} {b : B a} {b' : B a'} (g : Πa, B a → B' a) (p : a = a') (q : b =[p] b') : + ap (sigma_functor id g) (sigma_eq p q) = sigma_eq p (apo g q) := +by induction q; reflexivity + +definition sigma_eq_pr2_constant {A B : Type} {a a' : A} {b b' : B} (p : a = a') + (q : b =[p] b') : ap pr2 (sigma_eq p q) = (eq_of_pathover q) := +by induction q; reflexivity + +definition sigma_eq_pr2_constant2 {A B : Type} {a a' : A} {b b' : B} (p : a = a') + (q : b = b') : ap pr2 (sigma_eq p (pathover_of_eq p q)) = q := +by induction p; induction q; reflexivity + +definition sigma_eq_concato_eq {A : Type} {B : A → Type} {a a' : A} {b : B a} {b₁ b₂ : B a'} + (p : a = a') (q : b =[p] b₁) (q' : b₁ = b₂) : sigma_eq p (q ⬝op q') = sigma_eq p q ⬝ ap (dpair a') q' := +by induction q'; reflexivity + + -- open sigma.ops -- definition eq.rec_sigma {A : Type} {B : A → Type} {a₀ : A} {b₀ : B a₀} -- {P : Π(a : A) (b : B a), ⟨a₀, b₀⟩ = ⟨a, b⟩ → Type} (H : P a₀ b₀ idp) {a : A} {b : B a} @@ -592,8 +793,48 @@ namespace fiber definition is_contr_pfiber_pid (A : Type*) : is_contr (pfiber (pid A)) := is_contr.mk pt begin intro x, induction x with a p, esimp at p, cases p, reflexivity end +definition fiber_functor [constructor] {A A' B B' : Type} {f : A → B} {f' : A' → B'} {b : B} {b' : B'} + (g : A → A') (h : B → B') (H : hsquare g h f f') (p : h b = b') (x : fiber f b) : fiber f' b' := +fiber.mk (g (point x)) (H (point x) ⬝ ap h (point_eq x) ⬝ p) + +definition pfiber_functor [constructor] {A A' B B' : Type*} {f : A →* B} {f' : A' →* B'} + (g : A →* A') (h : B →* B') (H : psquare g h f f') : pfiber f →* pfiber f' := +pmap.mk (fiber_functor g h H (respect_pt h)) + begin + fapply fiber_eq, + exact respect_pt g, + exact !con.assoc ⬝ to_homotopy_pt H + end + +-- TODO: use this in pfiber_pequiv_of_phomotopy +definition fiber_equiv_of_homotopy {A B : Type} {f g : A → B} (h : f ~ g) (b : B) + : fiber f b ≃ fiber g b := +begin + refine (fiber.sigma_char f b ⬝e _ ⬝e (fiber.sigma_char g b)⁻¹ᵉ), + apply sigma_equiv_sigma_right, intros a, + apply equiv_eq_closed_left, apply h +end + +definition fiber_equiv_of_square {A B C D : Type} {b : B} {d : D} {f : A → B} {g : C → D} (h : A ≃ C) + (k : B ≃ D) (s : k ∘ f ~ g ∘ h) (p : k b = d) : fiber f b ≃ fiber g d := + calc fiber f b ≃ fiber (k ∘ f) (k b) : fiber.equiv_postcompose + ... ≃ fiber (k ∘ f) d : transport_fiber_equiv (k ∘ f) p + ... ≃ fiber (g ∘ h) d : fiber_equiv_of_homotopy s d + ... ≃ fiber g d : fiber.equiv_precompose + +definition fiber_equiv_of_triangle {A B C : Type} {b : B} {f : A → B} {g : C → B} (h : A ≃ C) + (s : f ~ g ∘ h) : fiber f b ≃ fiber g b := +fiber_equiv_of_square h erfl s idp + end fiber +namespace fin + +definition lift_succ2 [constructor] ⦃n : ℕ⦄ (x : fin n) : fin (nat.succ n) := +fin.mk x (le.step (is_lt x)) + +end fin + namespace function variables {A B : Type} {f f' : A → B} open is_conn sigma.ops