From d23466396d20ec6ad3f0b40fbf559d430c4a9133 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Sat, 1 Jul 2017 20:00:40 +0100 Subject: [PATCH] fix some errors --- algebra/exact_couple.hlean | 24 ++++++++---------------- homotopy/spectrum.hlean | 28 ++++++++++++++-------------- 2 files changed, 22 insertions(+), 30 deletions(-) diff --git a/algebra/exact_couple.hlean b/algebra/exact_couple.hlean index 2623363..20e0b1d 100644 --- a/algebra/exact_couple.hlean +++ b/algebra/exact_couple.hlean @@ -141,9 +141,6 @@ definition derived_couple_A : AbGroup := definition derived_couple_B : AbGroup := homology (differential EC) (differential_is_differential EC) -print homology - - definition derived_couple_i : derived_couple_A →g derived_couple_A := (image_lift (exact_couple.i EC)) ∘g (image_incl (exact_couple.i EC)) @@ -196,8 +193,8 @@ open eq definition left_square_derived_ses_aux : j_factor ∘g ab_image_incl k ~ (SES.f (SES_of_differential d H)) ∘g (image_homomorphism k j) := begin intro x, - induction x with a p, induction p with f, induction f with b p, induction p, - fapply subtype_eq, + induction x with a p, induction p with f, induction f with b p, induction p, + fapply subtype_eq, reflexivity, end @@ -207,10 +204,7 @@ definition left_square_derived_ses : j_factor ∘g (ab_kernel_incl i) ~ (SES.f ( exact (ap j_factor (subgroup_iso_exact_at_A_triangle x)) ⬝ (left_square_derived_ses_aux (subgroup_iso_exact_at_A x)), end -print quotient_extend_unique_SES -check quotient_extend_unique_SES (SES_of_exact_couple_at_i) (SES_of_differential d H) (subgroup_homom_ker_to_im) (j_factor) (left_square_derived_ses) - -definition derived_couple_j_unique : +definition derived_couple_j_unique : is_contr (Σ hC, group_fun (hC ∘g SES.g SES_of_exact_couple_at_i) ~ group_fun (SES.g (SES_of_differential d H) ∘g j_factor)) := quotient_extend_unique_SES (SES_of_exact_couple_at_i) (SES_of_differential d H) (subgroup_homom_ker_to_im) (j_factor) (left_square_derived_ses) @@ -229,7 +223,7 @@ definition derived_couple_j_htpy : group_fun (derived_couple_j ∘g SES.g SES_of definition SES_im_i_trivial : SES trivial_ab_group derived_couple_A derived_couple_A := begin fapply SES_of_isomorphism_right, - fapply isomorphism.refl, + fapply isomorphism.refl, end definition subgroup_iso_exact_kerj_imi : ab_kernel j ≃g ab_image i := @@ -252,7 +246,7 @@ definition k_restrict : ab_kernel d →g derived_couple_A := definition k_restrict_square_left : k_restrict ∘g (SES.f (SES_of_differential d H)) ~ λ x, 1 := begin intro x, - induction x with b' p, + induction x with b' p, induction p with q, induction q with b p, induction p, @@ -260,7 +254,7 @@ definition k_restrict_square_left : k_restrict ∘g (SES.f (SES_of_differential induction EC, induction exact_jk, fapply im_in_ker, - end + end definition derived_couple_k_unique : is_contr (Σ hC, group_fun (hC ∘g SES.g (SES_of_differential d H)) ~ group_fun @@ -273,8 +267,6 @@ definition derived_couple_k : derived_couple_B →g derived_couple_A := exact pr1 (center' (derived_couple_k_unique)), end -print conter_internal.center - definition derived_couple_k_htpy : group_fun (derived_couple_k ∘g SES.g (SES_of_differential d H)) ~ group_fun (SES.g (SES_im_i_trivial) ∘g k_restrict) := begin @@ -286,8 +278,8 @@ definition derived_couple_exact_ij : is_exact_ag derived_couple_i derived_couple fapply is_exact.mk, intro a, induction a with a' t, - induction t with q, induction q with a p, induction p, - repeat exact sorry, + induction t with q, induction q with a p, induction p, + repeat exact sorry, end end derived_couple diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean index 3f019a2..67049e7 100644 --- a/homotopy/spectrum.hlean +++ b/homotopy/spectrum.hlean @@ -155,7 +155,7 @@ namespace spectrum definition sid [constructor] [refl] {N : succ_str} (E : gen_prespectrum N) : E →ₛ E := smap.mk (λ n, pid (E n)) (λ n, psquare_of_phtpy_bot (ap1_pid) (psquare_of_pid_top_bot (phomotopy.rfl))) - print sid + --print sid -- smap.mk (λn, pid (E n)) -- (λn, calc glue E n ∘* pid (E n) ~* glue E n : pcompose_pid -- ... ~* pid (Ω(E (S n))) ∘* glue E n : pid_pcompose @@ -163,9 +163,9 @@ namespace spectrum definition scompose [trans] {N : succ_str} {X Y Z : gen_prespectrum N} (g : Y →ₛ Z) (f : X →ₛ Y) : X →ₛ Z := - smap.mk (λn, g n ∘* f n) - (λ n, psquare_of_phtpy_bot - (ap1_pcompose (g (S n)) (f (S n))) + smap.mk (λn, g n ∘* f n) + (λ n, psquare_of_phtpy_bot + (ap1_pcompose (g (S n)) (f (S n))) (psquare_hcompose (glue_square f n) (glue_square g n))) /- @@ -201,10 +201,10 @@ namespace spectrum structure shomotopy {N : succ_str} {E F : gen_prespectrum N} (f g : E →ₛ F) := (to_phomotopy : Πn, f n ~* g n) - (glue_homotopy : Πn, ptube_v - (to_phomotopy n) - (ap1_phomotopy (to_phomotopy (S n))) - (glue_square f n) + (glue_homotopy : Πn, ptube_v + (to_phomotopy n) + (ap1_phomotopy (to_phomotopy (S n))) + (glue_square f n) (glue_square g n)) /- (glue_homotopy : Πn, phsquare @@ -220,7 +220,7 @@ namespace spectrum shomotopy.mk (λn, (shomotopy.to_phomotopy q n) ⬝* (shomotopy.to_phomotopy p n)) begin - intro n, + intro n, unfold [ptube_v], rewrite (pwhisker_left_trans _), rewrite ap1_phomotopy_trans, rewrite (pwhisker_right_trans _), @@ -229,7 +229,7 @@ namespace spectrum definition shomotopy_inverse {N : succ_str} {E F : gen_prespectrum N} {f g : E →ₛ F} (p : f ~ₛ g) : g ~ₛ f := shomotopy.mk (λn, (shomotopy.to_phomotopy p n)⁻¹*) begin - intro n, + intro n, unfold [ptube_v], rewrite (pwhisker_left_symm _ _), rewrite [-ap1_phomotopy_symm], rewrite (pwhisker_right_symm _ _), @@ -255,7 +255,7 @@ namespace spectrum structure is_sequiv {N : succ_str} {E F : gen_prespectrum N} (f : E →ₛ F) : Type := (to_linv : F →ₛ E) - (is_retr : to_linv ∘ₛf ~ₛ sid E) + (is_retr : to_linv ∘ₛf ~ₛ sid E) (to_rinv : F →ₛ E) (is_sec : f ∘ₛ to_rinv ~ₛ sid F) @@ -269,7 +269,7 @@ namespace spectrum definition is_sequiv_of_smap_pequiv {N : succ_str} {E F : gen_prespectrum N} (f : E →ₛ F) (H : is_sequiv_smap f) (n : N) : E n ≃* F n := begin - fapply pequiv_of_pmap, + fapply pequiv_of_pmap, exact f n, fapply H, end @@ -285,7 +285,7 @@ namespace spectrum exact glue_square f n, end - local postfix `⁻¹ˢ` : (max + 1) := is_sequiv_of_smap_inv + local postfix `⁻¹ˢ` : (max + 1) := is_sequiv_of_smap_inv definition is_sequiv_of_smap_isretr {N : succ_str} {E F : gen_prespectrum N} (f : E →ₛ F) (H : is_sequiv_smap f) : is_sequiv_of_smap_inv f H ∘ₛ f ~ₛ sid E := begin @@ -537,7 +537,7 @@ namespace spectrum begin intro f, fapply smap.mk, - intro n, exact (equiv_glue E n)⁻¹ᵉ* ∘* Ω→ (f (S n)), + intro n, exact (equiv_glue E n)⁻¹ᵉ* ∘* Ω→ (f (S n)), intro n, fapply psquare_of_phomotopy, refine (passoc (glue (gen_spectrum.to_prespectrum E) n) (pequiv.to_pmap (equiv_glue (gen_spectrum.to_prespectrum E) n)⁻¹ᵉ*) (Ω→ (to_fun f (S n))))⁻¹* ⬝* _,