fix some errors
This commit is contained in:
Floris van Doorn
parent
9d562c1e5d
commit
d23466396d
2 changed files with 22 additions and 30 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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))))⁻¹* ⬝* _,
|
||||
|
|
|
|||
Loading…
Reference in a new issue