michael/Spectral
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

left square

Browse source
This commit is contained in:
Steve Awodey 2017-05-18 17:54:13 -04:00
parent c28c078f1c
commit 7ee38d255c
1 changed files with 11 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
algebra/exact_couple.hlean
View file

@ -121,6 +121,7 @@ section derived_couple
local abbreviation k := exact_couple.k EC local abbreviation k := exact_couple.k EC
local abbreviation d := differential EC local abbreviation d := differential EC
local abbreviation H := differential_is_differential EC local abbreviation H := differential_is_differential EC
-- local abbreviation u := exact_couple.i (SES_of_differential d H)
definition derived_couple_A : AbGroup := definition derived_couple_A : AbGroup :=
ab_subgroup (image_subgroup i) ab_subgroup (image_subgroup i)
@ -172,7 +173,16 @@ definition subgroup_iso_exact_at_A_triangle : ab_kernel_incl i ~ ab_image_incl k
induction EC, induction exact_ki, exact im_in_ker b, induction EC, induction exact_ki, exact im_in_ker b,
end end
definition definition subgroup_homom_ker_to_im : ab_kernel i →g ab_image d :=
(image_homomorphism k j) ∘g subgroup_iso_exact_at_A
open eq
definition left_square_derived_ses : j_factor ∘g (ab_kernel_incl i) ~ (SES.f (SES_of_differential d H)) ∘g subgroup_homom_ker_to_im :=
begin
intro x,
fapply subtype_eq,
refine sorry --(ap (j_factor) subgroup_iso_exact_at_A_triangle) ⬝ _,
end
definition derived_couple_j : derived_couple_A EC →g derived_couple_B EC := definition derived_couple_j : derived_couple_A EC →g derived_couple_B EC :=
begin begin
exact sorry, exact sorry,