From 79dea677e8deca640b66750e228a674b8ac5f403 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 12 Oct 2016 20:07:18 -0400 Subject: [PATCH] colimit, start on encode-decode proof --- colim.hlean | 127 ++++++++++++++++++++++++++++++++++++++-- homotopy/spectrum.hlean | 21 +++++-- homotopy/splice.hlean | 6 +- move_to_lib.hlean | 100 +++++++++++++++++++++---------- 4 files changed, 210 insertions(+), 44 deletions(-) diff --git a/colim.hlean b/colim.hlean index 2bb77f3..ee761ee 100644 --- a/colim.hlean +++ b/colim.hlean @@ -16,12 +16,8 @@ namespace seq_colim : X n →* pseq_colim f := pmap.mk (inclusion f) (inclusion_pt f n) - -- TODO: we need to prove this - definition pseq_colim_loop {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) : - Ω (pseq_colim f) ≃* pseq_colim (λn, Ω→(f n)) := - sorry - definition seq_diagram [reducible] (A : ℕ → Type) : Type := Π⦃n⦄, A n → A (succ n) + definition pseq_diagram [reducible] (A : ℕ → Type*) : Type := Π⦃n⦄, A n →* A (succ n) structure Seq_diagram : Type := (carrier : ℕ → Type) @@ -192,8 +188,13 @@ namespace seq_colim seq_diagram (λn, Πx, A x n) := λn f x, g (f x) + namespace seq_colim.ops abbreviation ι [constructor] := @inclusion + abbreviation pι [constructor] {A} (f) {n} := @pinclusion A f n + abbreviation pι' [constructor] [parsing_only] := @pinclusion abbreviation ι' [constructor] [parsing_only] {A} (f n) := @inclusion A f n + end seq_colim.ops + open seq_colim.ops definition rep0_glue (k : ℕ) (a : A 0) : ι f (rep0 f k a) = ι f a := begin @@ -345,6 +346,122 @@ namespace seq_colim { esimp, apply respect_pt } end + definition prep0 [constructor] {A : ℕ → Type*} (f : pseq_diagram A) (k : ℕ) : A 0 →* A k := + pmap.mk (rep0 (λn x, f 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 x) n pt = rep0 (λn x, f 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, +ap_con, ap_inv, +con.assoc] + + 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 + (λ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 + + section + parameters {X : ℕ → Type} (g : seq_diagram X) (x : X 0) + + definition rep_eq_diag ⦃n : ℕ⦄ (y : X n) : seq_diagram (λk, rep g k (rep0 g n x) = rep g k y) := + proof λk, ap (@g (n + k)) qed + + definition code_incl ⦃n : ℕ⦄ (y : X n) : Type := + seq_colim (rep_eq_diag y) + + definition code [unfold 4] : seq_colim g → Type := + seq_colim.elim_type g code_incl + begin + intro n y, + refine _ ⬝e !shift_equiv⁻¹ᵉ, + fapply seq_colim_equiv, + { intro k, exact code_glue_equiv g k (rep0 g n x) y }, + { intro k p, exact code_glue_equiv_ap g p } + end + + definition encode [unfold 5] (y : seq_colim g) (p : ι g x = y) : code y := + transport code p (ι' _ 0 idp) + + definition decode [unfold 4] (y : seq_colim g) (c : code y) : ι g x = y := + begin + induction y, + { esimp at c, exact sorry}, + { exact sorry } + end + + definition decode_encode (y : seq_colim g) (p : ι g x = y) : decode y (encode y p) = p := + sorry + + definition encode_decode (y : seq_colim g) (c : code y) : encode y (decode y c) = c := + sorry + + definition seq_colim_eq_equiv_code [constructor] (y : seq_colim g) : (ι g x = y) ≃ code y := + equiv.MK (encode y) (decode y) (encode_decode y) (decode_encode y) + + definition seq_colim_eq {n : ℕ} (y : X n) : (ι g x = ι g y) ≃ seq_colim (rep_eq_diag y) := + proof seq_colim_eq_equiv_code (ι g y) qed + + end + + definition rep0_eq_diag {X : ℕ → Type} (f : seq_diagram X) (x y : X 0) + : seq_diagram (λk, rep0 f k x = rep0 f k y) := + proof λk, ap (@f (k)) qed + + definition seq_colim_eq0 {X : ℕ → Type} (f : seq_diagram X) (x y : X 0) : + (ι f x = ι f y) ≃ seq_colim (rep0_eq_diag f x y) := + begin + refine !seq_colim_eq ⬝e _, + fapply seq_colim_equiv, + { intro n, exact sorry}, + { intro n p, exact sorry } + 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_eq0 ⬝e _, + fapply seq_colim_equiv, + { intro n, exact loop_equiv_eq_closed (respect_pt (prep0 f n)) }, + { intro n p, apply prep0_succ_lemma }}, + { 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)) : diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean index cdc1ea1..88be0b1 100644 --- a/homotopy/spectrum.hlean +++ b/homotopy/spectrum.hlean @@ -123,6 +123,7 @@ namespace spectrum ------------------------------ -- These make sense for any succ_str. + structure smap {N : succ_str} (E F : gen_prespectrum N) := (to_fun : Π(n:N), E n →* F n) (glue_square : Π(n:N), glue F n ∘* to_fun n ~* Ω→ (to_fun (S n)) ∘* glue E n) @@ -243,13 +244,16 @@ namespace spectrum definition sfiber {N : succ_str} {X Y : gen_spectrum N} (f : X →ₛ Y) : gen_spectrum N := spectrum.MK (λn, pfiber (f n)) - (λn, pfiber_loop_space (f (S n)) ∘*ᵉ pfiber_equiv_of_square (sglue_square f n)) + (λn, pfiber_loop_space (f (S n)) ∘*ᵉ pfiber_equiv_of_square _ _ (sglue_square f n)) - /- the map from the fiber to the domain. The fact that the square commutes requires work -/ + /- the map from the fiber to the domain -/ definition spoint {N : succ_str} {X Y : gen_spectrum N} (f : X →ₛ Y) : sfiber f →ₛ X := smap.mk (λn, ppoint (f n)) begin - intro n, exact sorry + intro n, + refine _ ⬝* !passoc, + refine _ ⬝* pwhisker_right _ !ap1_ppoint_phomotopy⁻¹*, + rexact (pfiber_equiv_of_square_ppoint (equiv_glue X n) (equiv_glue Y n) (sglue_square f n))⁻¹* end definition π_glue (X : spectrum) (n : ℤ) : π[2] (X (2 - succ n)) ≃* π[3] (X (2 - n)) := @@ -386,6 +390,15 @@ namespace spectrum definition spectrify_type {N : succ_str} (X : gen_prespectrum N) (n : N) : Type* := pseq_colim (spectrify_type_fun X n) + /- + Let Y = spectify X. Then + Ω Y (n+1) ≡ Ω colim_k Ω^k X ((n + 1) + k) + ... = colim_k Ω^{k+1} X ((n + 1) + k) + ... = colim_k Ω^{k+1} X (n + (k + 1)) + ... = colim_k Ω^k X(n + k) + ... ≡ Y n + -/ + definition spectrify_pequiv {N : succ_str} (X : gen_prespectrum N) (n : N) : spectrify_type X n ≃* Ω (spectrify_type X (S n)) := begin @@ -396,7 +409,7 @@ namespace spectrum fapply pseq_colim_pequiv, { intro n, apply loopn_pequiv_loopn, apply pequiv_ap X, apply succ_str.add_succ }, { intro k, apply to_homotopy, - refine !passoc⁻¹* ⬝* _, refine pwhisker_right _ (loopn_succ_in_inv_apn (succ k) _) ⬝* _, + refine !passoc⁻¹* ⬝* _, refine pwhisker_right _ (loopn_succ_in_inv_natural (succ k) _) ⬝* _, refine !passoc ⬝* _ ⬝* !passoc⁻¹*, apply pwhisker_left, refine !apn_pcompose⁻¹* ⬝* _ ⬝* !apn_pcompose, apply apn_phomotopy, exact !glue_ptransport⁻¹* } diff --git a/homotopy/splice.hlean b/homotopy/splice.hlean index 67d4210..53cb2f4 100644 --- a/homotopy/splice.hlean +++ b/homotopy/splice.hlean @@ -20,9 +20,9 @@ such that the evident squares commute, we can obtain a single sequence However, in this formalization, we will only do this for k = 3, because we get more definitional equalities in this specific case than in the general case. The reason is that we need to check -whether a term `x : fin (succ k)` represents `n`. If we do this in general using -if x = n then ... else ... -we don't get definitionally that x = n and the successor of x is 0, which means that when defining +whether a term `x : fin (succ k)` represents `k`. If we do this in general using +if x = k then ... else ... +we don't get definitionally that x = k and the successor of x is 0, which means that when defining maps G_{n,m} -> G_{n+1,m+k-1} we need to transport along those paths, which is annoying. So far, the splicing seems to be only needed for k = 3, so it seems to be sufficient. diff --git a/move_to_lib.hlean b/move_to_lib.hlean index 3c37415..4243431 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -7,7 +7,8 @@ open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc attribute equiv.symm equiv.trans is_equiv.is_equiv_ap fiber.equiv_postcompose fiber.equiv_precompose pequiv.to_pmap pequiv._trans_of_to_pmap ghomotopy_group_succ_in - isomorphism_of_eq pmap_bool_equiv sphere_equiv_bool psphere_pequiv_pbool [constructor] + isomorphism_of_eq pmap_bool_equiv sphere_equiv_bool psphere_pequiv_pbool fiber_eq_equiv + [constructor] attribute is_equiv.eq_of_fn_eq_fn' [unfold 3] attribute isomorphism._trans_of_to_hom [unfold 3] attribute homomorphism.struct [unfold 3] @@ -90,11 +91,21 @@ namespace pi -- move to types.arrow { apply pmap_eq_idp} end - end pi open pi namespace eq + -- types.eq + definition loop_equiv_eq_closed [constructor] {A : Type} {a a' : A} (p : a = a') + : (a = a) ≃ (a' = a') := + eq_equiv_eq_closed p p + + -- init.path + definition tr_ap {A B : Type} {x y : A} (P : B → Type) (f : A → B) (p : x = y) (z : P (f x)) : + transport P (ap f p) z = transport (P ∘ f) p z := + (tr_compose P f p z)⁻¹ + + definition pathover_eq_Fl' {A B : Type} {f : A → B} {a₁ a₂ : A} {b : B} (p : a₁ = a₂) (q : f a₂ = b) : (ap f p) ⬝ q =[p] q := by induction p; induction q; exact idpo @@ -298,16 +309,6 @@ namespace pointed {a₁ a₂ : A} (p : a₁ = a₂) : pequiv_of_eq (ap C p) ∘* f a₁ ~* f a₂ ∘* pequiv_of_eq (ap B p) := pcast_commute f p - -- TODO: make the name apn_succ_phomotopy_in consistent with this - definition loopn_succ_in_inv_apn {A B : Type*} (n : ℕ) (f : A →* B) : - Ω→[n + 1] f ∘* (loopn_succ_in A n)⁻¹ᵉ* ~* (loopn_succ_in B n)⁻¹ᵉ* ∘* Ω→[n] (Ω→ f):= - begin - apply pinv_right_phomotopy_of_phomotopy, - refine _ ⬝* !passoc⁻¹*, - apply phomotopy_pinv_left_of_phomotopy, - apply apn_succ_phomotopy_in - end - definition papply [constructor] {A : Type*} (B : Type*) (a : A) : ppmap A B →* B := pmap.mk (λ(f : A →* B), f a) idp @@ -337,30 +338,52 @@ namespace pointed ppmap A B →* Ω[n] B := papply _ p ∘* papn_pt n A B - definition loopn_succ_in_natural {A B : Type*} {n : ℕ} (f : A →* B) : + definition loopn_succ_in_natural {A B : Type*} (n : ℕ) (f : A →* B) : loopn_succ_in B n ∘* Ω→[n+1] f ~* Ω→[n] (Ω→ f) ∘* loopn_succ_in A n := !apn_succ_phomotopy_in - definition loopn_succ_in_inv_natural {A B : Type*} {n : ℕ} (f : A →* B) : - (loopn_succ_in B n)⁻¹ᵉ* ∘* Ω→[n] (Ω→ f) ~* Ω→[n+1] f ∘* (loopn_succ_in A n)⁻¹ᵉ* := - sorry + definition loopn_succ_in_inv_natural {A B : Type*} (n : ℕ) (f : A →* B) : + Ω→[n + 1] f ∘* (loopn_succ_in A n)⁻¹ᵉ* ~* (loopn_succ_in B n)⁻¹ᵉ* ∘* Ω→[n] (Ω→ f):= + begin + apply pinv_right_phomotopy_of_phomotopy, + refine _ ⬝* !passoc⁻¹*, + apply phomotopy_pinv_left_of_phomotopy, + apply apn_succ_phomotopy_in + end end pointed open pointed namespace fiber + definition pfiber.sigma_char [constructor] {A B : Type*} (f : A →* B) + : pfiber f ≃* pointed.MK (Σa, f a = pt) ⟨pt, respect_pt f⟩ := + pequiv_of_equiv (fiber.sigma_char f pt) idp + + definition ppoint_sigma_char [constructor] {A B : Type*} (f : A →* B) + : ppoint f ~* pmap.mk pr1 idp ∘* pfiber.sigma_char f := + !phomotopy.refl + definition pfiber_loop_space {A B : Type*} (f : A →* B) : pfiber (Ω→ f) ≃* Ω (pfiber f) := pequiv_of_equiv - (calc pfiber (Ω→ f) ≃ Σ(p : Point A = Point A), ap1 f p = rfl : (fiber.sigma_char (ap1 f) (Point (Ω B))) - ... ≃ Σ(p : Point A = Point A), (respect_pt f) = ap f p ⬝ (respect_pt f) : (sigma_equiv_sigma_right (λp, - calc (ap1 f p = rfl) ≃ !respect_pt⁻¹ ⬝ (ap f p ⬝ !respect_pt) = rfl : equiv_eq_closed_left _ (con.assoc _ _ _) - ... ≃ ap f p ⬝ (respect_pt f) = (respect_pt f) : eq_equiv_inv_con_eq_idp - ... ≃ (respect_pt f) = ap f p ⬝ (respect_pt f) : eq_equiv_eq_symm)) - ... ≃ fiber.mk (Point A) (respect_pt f) = fiber.mk pt (respect_pt f) : fiber_eq_equiv - ... ≃ Ω (pfiber f) : erfl) - (begin cases f with f p, cases A with A a, cases B with B b, esimp at p, esimp at f, induction p, reflexivity end) + (calc pfiber (Ω→ f) ≃ Σ(p : Point A = Point A), ap1 f p = rfl + : (fiber.sigma_char (ap1 f) (Point (Ω B))) + ... ≃ Σ(p : Point A = Point A), (respect_pt f) = ap f p ⬝ (respect_pt f) + : (sigma_equiv_sigma_right (λp, + calc (ap1 f p = rfl) ≃ !respect_pt⁻¹ ⬝ (ap f p ⬝ !respect_pt) = rfl + : equiv_eq_closed_left _ (con.assoc _ _ _) + ... ≃ ap f p ⬝ (respect_pt f) = (respect_pt f) + : eq_equiv_inv_con_eq_idp + ... ≃ (respect_pt f) = ap f p ⬝ (respect_pt f) + : eq_equiv_eq_symm)) + ... ≃ fiber.mk (Point A) (respect_pt f) = fiber.mk pt (respect_pt f) + : fiber_eq_equiv + ... ≃ Ω (pfiber f) + : erfl) + (begin cases f with f p, cases A with A a, cases B with B b, esimp at p, esimp at f, + induction p, reflexivity end) - definition pfiber_equiv_of_phomotopy {A B : Type*} {f g : A →* B} (h : f ~* g) : pfiber f ≃* pfiber g := + definition pfiber_equiv_of_phomotopy {A B : Type*} {f g : A →* B} (h : f ~* g) + : pfiber f ≃* pfiber g := begin fapply pequiv_of_equiv, { refine (fiber.sigma_char f pt ⬝e _ ⬝e (fiber.sigma_char g pt)⁻¹ᵉ), @@ -371,12 +394,14 @@ namespace fiber rewrite idp_con, apply inv_con_eq_of_eq_con, symmetry, exact (to_homotopy_pt h) } end - definition transport_fiber_equiv [constructor] {A B : Type} (f : A → B) {b1 b2 : B} (p : b1 = b2) : fiber f b1 ≃ fiber f b2 := + definition transport_fiber_equiv [constructor] {A B : Type} (f : A → B) {b1 b2 : B} (p : b1 = b2) + : fiber f b1 ≃ fiber f b2 := calc fiber f b1 ≃ Σa, f a = b1 : fiber.sigma_char ... ≃ Σa, f a = b2 : sigma_equiv_sigma_right (λa, equiv_eq_closed_right (f a) p) ... ≃ fiber f b2 : fiber.sigma_char - definition pequiv_postcompose {A B B' : Type*} (f : A →* B) (g : B ≃* B') : pfiber (g ∘* f) ≃* pfiber f := + definition pequiv_postcompose {A B B' : Type*} (f : A →* B) (g : B ≃* B') + : pfiber (g ∘* f) ≃* pfiber f := begin fapply pequiv_of_equiv, esimp, refine transport_fiber_equiv (g ∘* f) (respect_pt g)⁻¹ ⬝e fiber.equiv_postcompose f g (Point B), @@ -384,7 +409,8 @@ namespace fiber rewrite [con.assoc, con.right_inv, con_idp, -ap_compose'], apply ap_con_eq_con end - definition pequiv_precompose {A A' B : Type*} (f : A →* B) (g : A' ≃* A) : pfiber (f ∘* g) ≃* pfiber f := + definition pequiv_precompose {A A' B : Type*} (f : A →* B) (g : A' ≃* A) + : pfiber (f ∘* g) ≃* pfiber f := begin fapply pequiv_of_equiv, esimp, refine fiber.equiv_precompose f g (Point B), @@ -393,12 +419,23 @@ namespace fiber { apply pathover_eq_Fl' } end - definition pfiber_equiv_of_square {A B C D : Type*} {f : A →* B} {g : C →* D} {h : A ≃* C} {k : B ≃* D} (s : k ∘* f ~* g ∘* h) - : pfiber f ≃* pfiber g := + definition pfiber_equiv_of_square {A B C D : Type*} {f : A →* B} {g : C →* D} (h : A ≃* C) + (k : B ≃* D) (s : k ∘* f ~* g ∘* h) : pfiber f ≃* pfiber g := calc pfiber f ≃* pfiber (k ∘* f) : pequiv_postcompose ... ≃* pfiber (g ∘* h) : pfiber_equiv_of_phomotopy s ... ≃* pfiber g : pequiv_precompose + definition ap1_ppoint_phomotopy {A B : Type*} (f : A →* B) + : Ω→ (ppoint f) ∘* pfiber_loop_space f ~* ppoint (Ω→ f) := + begin + exact sorry + end + + definition pfiber_equiv_of_square_ppoint {A B C D : Type*} {f : A →* B} {g : C →* D} + (h : A ≃* C) (k : B ≃* D) (s : k ∘* f ~* g ∘* h) + : ppoint g ∘* pfiber_equiv_of_square h k s ~* h ∘* ppoint f := + sorry + end fiber namespace eq --algebra.homotopy_group @@ -689,7 +726,7 @@ namespace new_sphere { revert A, induction n with n IH: intro A, { reflexivity }, { intro f, refine ap !loopn_succ_in⁻¹ᵉ* (IH (Ω A) _ ⬝ !apn_pcompose _) ⬝ _, - exact !loopn_succ_in_inv_natural _ }} + exact !loopn_succ_in_inv_natural⁻¹* _ }} end end new_sphere @@ -709,4 +746,3 @@ namespace sphere -- end end sphere -