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

work on SES

Browse source
This commit is contained in:
Egbert Rijke 2017-01-26 16:55:59 -05:00
parent c09f568992
commit af70424d60
1 changed files with 26 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
algebra/exact_couple.hlean
View file

@ -15,6 +15,32 @@ structure is_exact {A B C : AbGroup} (f : A →g B) (g : B →g C) :=
( im_in_ker : Π(a:A), g (f a) = 1)
( ker_in_im : Π(b:B), (g b = 1) → ∃(a:A), f a = b)
structure SES (A B C : AbGroup) :=
( f : A →g B)
( g : B →g C)
( Hf : is_embedding f)
( Hg : is_surjective g)
( ex : is_exact f g)
structure hom_SES {A B C A' B' C' : AbGroup} (ses : SES A B C) (ses' : SES A' B' C') :=
( hA : A →g A')
( hB : B →g B')
( hC : C →g C')
( htpy1 : hB ∘g (SES.f ses) ~ (SES.f ses') ∘g hA)
( htpy2 : hC ∘g (SES.g ses) ~ (SES.g ses') ∘g hB)
definition quotient_SES {A B C : AbGroup} (ses : SES A B C) : C ≃g quotient_ab_group (image_subgroup (SES.f ses)) :=
begin
fapply ab_group_first_iso_thm B C (SES.g ses),
end
definition right_extend_SES {A B C A' B' C' : AbGroup}
(ses : SES A B C) (ses' : SES A' B' C')
(hA : A →g A') (hB : B →g B') (htpy1 : hB ∘g (SES.f ses) ~ (SES.f ses') ∘g hA) : C →g C' :=
begin
end
definition is_differential {B : AbGroup} (d : B →g B) := Π(b:B), d (d b) = 1
definition image_subgroup_of_diff {B : AbGroup} (d : B →g B) (H : is_differential d) : subgroup_rel (ab_kernel d) :=