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

some stuff about exact couples

Browse source
This commit is contained in:
Egbert Rijke 2017-05-11 17:25:02 -04:00
parent 922baa9975
commit eaf7290def
1 changed files with 9 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
algebra/exact_couple.hlean
View file

@ -131,12 +131,20 @@ definition SES_of_exact_couple_at_i : SES (ab_kernel i) A (ab_image i) :=
fapply ab_group_first_iso_thm i, fapply ab_group_first_iso_thm i,
end end
definition kj_zero (a : A) : k (j a) = 1 :=
begin
exact sorry
end
definition j_factor : A →g (ab_kernel d) := definition j_factor : A →g (ab_kernel d) :=
begin begin
fapply ab_hom_lift j, fapply ab_hom_lift j,
intro a, intro a,
unfold kernel_subgroup, unfold kernel_subgroup,
exact sorry --refine ap (group_fun j) _, exact calc
d (j a) = j (k (j a)) : rfl
... = j 1 : by exact ap j (kj_zero a)
... = 1 : to_respect_one,
end end